agda - 有根据的递归安全吗？

Question

在关于不终止的问题中，带有模糊终止的条款的答案建议求助于<-wellFounded.

我查看了<-wellFounded之前的定义，让我印象深刻的是--safe在OPTIONS. 没有这个选项就可以工作吗？也就是说，是在使用--safe一些优化，还是在解决一些基本问题？所以在这种情况下，我们只是将终止问题委托给标记为“安全”的函数？

Answer 1

这是完全安全的。--safe使模块遵循比默认更严格的标准。这并不意味着某事不安全，而是意味着某事是安全的。从任何模块使用有根据的递归，无论安全与否，都不会引入非终止。终止相当强烈地融入可访问性的归纳定义中。