程序修复点和Coq中的函数有什么区别？

Question

他们似乎服务于类似的目的.到目前为止我注意到的一个区别是,虽然Program Fixpoint会接受一个复合测量{measure (length l1 + length l2) },但Function似乎拒绝这个并且只会允许{measure length l1}.

是否Program Fixpoint比Function它们更强大,或者它们更适合不同的用例？

Answer 1

这可能不是完整的列表，但这是我迄今为止发现的：

• 正如您已经提到的，Program Fixpoint允许该措施考虑多个论点。
• Function创建一个foo_equation引理，可用于重写foo对其 RHS 的调用。对于避免像Coq simpl for Program Fixpoint这样的问题非常有用。
• 在某些（简单？）情况下，Function可以定义一个foo_ind引理来沿着 的递归调用结构执行归纳foo。同样，这对于证明一些事情非常有用，foo而无需在证明中有效地重复终止论证。
• Program Fixpoint可以被欺骗以支持嵌套递归，请参阅/sf/answers/3280161671/。这也是为什么Program Fixpoint可以定义阿克曼函数而Function不能定义的原因。