coq - Coq中的程序定点和功能之间有什么区别？

Question

它们似乎具有相似的目的。到目前为止，我注意到的一个区别是，虽然Program Fixpoint将接受像{measure (length l1 + length l2) }这样的复合量度，但Function似乎拒绝了这一点，并且只允许{measure length l1}。
Program Fixpoint是否比Function严格更强大，或者它们更适合于不同的用例？

Answer 1

这可能不是完整的列表，但这是我到目前为止发现的:

正如您已经提到的，Program Fixpoint允许度量查看多个参数。

Function创建一个foo_equation引理，该引理可用于用其​​RHS重写对foo的调用。避免Coq simpl for Program Fixpoint之类的问题非常有用。

在某些(简单？)情况下，Function可以定义foo_ind引理，以按照foo的递归调用的结构执行归纳。同样，在不有效重复证明中的终止参数的情况下证明有关foo的内容非常有用。

可以欺骗

Program Fixpoint以支持嵌套递归，请参见https://stackoverflow.com/a/46859452/946226。这也是为什么Program Fixpoint无法执行时Function可以define the Ackermann功能的原因。