在Coq中，程序的Fixpoint和Function有什么区别？

Question

它们似乎具有类似的目的。到目前为止我注意到的唯一区别是，虽然 Program Fixpoint 可以接受类似于 {measure (length l1 + length l2) } 的组合度量，但是 Function 会拒绝这样做，只允许 {measure length l1}。

Program Fixpoint 是否比 Function 更强大，还是它们更适用于不同的用例？

- LogicChains

---

顺便提一下，Coq v8.7 路线图 表示他们的实现将被合并。 - Anton Trunov

这是一个好问题。我建议你去 Coq 的 gitter 寻求详细的答案，因为对此有深入了解的人不会在 Stack Overflow 上阅读。Function 和 Program 的实现由不同的人在不同的情境下完成，因此它们的功能集并非严格是另一个的子集。计划将它们合并在一个新的“Equations”插件中，但这不会在 8.7 版本中发生，即使已经取得了很多进展。话虽如此，如果您关心与未来的 Coq 发布版本兼容性，我认为通常最好使用 Program。 - ejgallego

Answer 1

这可能不是一个完整的列表，但这是我目前找到的:

• 正如您已经提到的，Program Fixpoint 允许度量衡查看多个参数。
• Function 创建一个 foo_equation 引理，可以用来重写对 foo 的调用与其 RHS。非常有用，避免像Coq simpl for Program Fixpoint这样的问题。
• 在一些（简单的？）情况下，Function 可以定义一个 foo_ind 引理，以沿着递归调用 foo 的结构进行归纳。再次，非常有用，可以证明关于 foo 的事情，而不实际重复证明中的终止参数。
• Program Fixpoint 可以被欺骗支持嵌套递归，请参见https://dev59.com/Dqbja4cB1Zd3GeqPbBlN#46859452。这也是为什么当Function不能时，Program Fixpoint可以定义Ackermann函数的原因。

- Joachim Breitner

---

似乎也不可能使用“Function”定义Ackermann函数，但是“Program Fixpoint”可以做到。参考链接。 - Anton Trunov

谢谢，已将其添加到答案中。 - Joachim Breitner