Coq中的程序定点和功能之间有什么区别？ [英] What's the difference between Program Fixpoint and Function in Coq?

问题描述

它们似乎具有相似的目的。到目前为止，我注意到的一个区别是，虽然 Program Fixpoint 将接受类似 {measure（length l1 + length l2）} / code>，函数似乎拒绝了，只会允许 {卷长l1} 。

They seem to serve similar purposes. The one difference I've noticed so far is that while Program Fixpoint will accept a compound measure like {measure (length l1 + length l2) }, Function seems to reject this and will only allow {measure length l1}.

严格来说，程序定位点比功能强大，或者

Is Program Fixpoint strictly more powerful than Function, or are they better suited for different use cases?

推荐答案

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

This may not be a complete list, but it is what I have found so far:

• 正如您已经提到的， Program Fixpoint 允许该措施查看更多


• Function 创建一个可以使用的 foo_equation 引理。用其RHS重写对 foo 的调用。对于避免诸如程序修订点的Coq简化这样的问题非常有用。


• 简单吗？）情况下， Function 可以定义 foo_ind 引理，以沿着<$ c的递归调用的结构执行归纳$ c> foo 。同样，对于证明 foo 的事情而又没有有效地重复证明中的终止参数非常有用。


• 程序Fixpoint 可以被欺骗来支持嵌套递归，请参见 https://stackoverflow.com/a/46859452/946226 。这也是为什么程序修订点可以定义 Function 不能的Ackermann 函数。

• As you already mentioned, Program Fixpoint allows the measure to look at more than one argument.
• Function creates a foo_equation lemma that can be used to rewrite calls to foo with its RHS. Very useful to avoid problems like Coq simpl for Program Fixpoint.
• In some (simple?) cases, Function can define a foo_ind lemma to perform induction along the structure of recursive calls of foo. Again, very useful to prove things about foo without effectively repeating the termination argument in the proof.
• Program Fixpoint can be tricked into supporting nested recursion, see https://stackoverflow.com/a/46859452/946226. This is also why Program Fixpoint can define the Ackermann function when Function cannot.

这篇关于Coq中的程序定点和功能之间有什么区别？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！