What's the difference between Program Fixpoint and Function in Coq?

 

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:

  • 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.
    • 链接地址: http://www.djcxy.com/p/39840.html

    上一篇: 如何使用两个堆栈实现队列？

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