程序固定点和Coq中的函数有什么区别？

2018-06-13 23:44:01

他们似乎有相似的目的。迄今为止我注意到的一个区别是，虽然Program Fixpoint点将接受像{measure (length l1 + length l2) }这样的复合度量，但Function似乎拒绝了这一点，并且只允许{measure length l1} 。

Program Fixpoint比Function严格得多，还是更适合不同的用例？

这可能不是一个完整的清单，但这是我迄今发现的：

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

Function创建一个foo_equation引理，可以用它的RHS重写对foo调用。非常有用，可以避免Coq简化Program Fixpoint等问题。

在一些（简单的？）情况下， Function可以定义一个foo_ind引理来沿着foo的递归调用的结构进行归纳。同样，证明关于foo事情非常有用，而不必在证明中有效地重复终止论证。

Program Fixpoint可以欺骗成支持嵌套递归，请参阅https://stackoverflow.com/a/46859452/946226。这也是为什么Program Fixpoint可以在Function不能时定义Ackermann函数的原因。

链接地址: http://www.djcxy.com/p/39839.html