它们似乎具有相似的目的。到目前为止,我注意到的一个区别是,虽然Program Fixpoint
将接受像{measure (length l1 + length l2) }
这样的复合量度,但Function
似乎拒绝了这一点,并且只允许{measure length l1}
。Program Fixpoint
是否比Function
严格更强大,或者它们更适合于不同的用例?
最佳答案
这可能不是完整的列表,但这是我到目前为止发现的:
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功能的原因。 关于coq - Coq中的程序定点和功能之间有什么区别?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/44606245/