Geek Answers Handbook

What is the difference between a fixpoint program and a function in Coq?

They seem to fulfill similar goals. The only difference I've noticed so far is that although the Program Fixpoint will take a composite measure like {measure (length l1 + length l2) } , Function seems to reject this and will only allow {measure length l1} .

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

+7
coq
source share
1 answer

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

  • As you already mentioned, Program Fixpoint allows you to measure more than one argument.
  • Function creates the lemma foo_equation , which can be used to rewrite calls to foo with its RHS. It is very helpful to avoid issues like Coq for Fixpoint .
  • In some (simple?) Cases, Function can define the lemma foo_ind for induction on the structure of recursive calls foo . Again, it is very useful to prove things about foo without effectively repeating the termination argument in the proof.
  • Program Fixpoint can be Program Fixpoint into supporting nested recursion, see fooobar.com/questions/846726 / .... That is why Program Fixpoint can define an Ackermann function if Function cannot.
+3
source share

More articles:


All Articles