The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

The question about capturing all terminating recursive functions is a
bit confusing.  All recursive function are ultimately described using
the  Fix construct.  So all the functions that can be described in Coq 
can be described using Fixpoint.  Taken in this broad sense, we get
more than just the structural recursive functions.

However, it is true that well-founded recursive functions (see the
constant well_founded_induction) actually have an extra argument, in
the Prop sort, that is used to control the recursion: so the algorithm
is slightly modified to make it fit through the keyhole of structural
recursion.

But the algorithm is not modified so much.  When you extract a
function from a Coq function defined by well-founded recursion, the
extra argument that was in Prop is dropped and you get back the
algorithm you had in mind.

There are other techniques, mainly introduced by Ana Bove in the
context of Martin-Löf's Type theory, that make it possible to encode a
recursive function, even a partial one, as a function in Coq (again
with an extra proof argument).  Martin-Löf's type theory does not
provide a distinction between sorts Set and Prop, but Christine Paulin 
proposed in a previous message on this forum a scheme to make sure the 
proof is really viewed as a proof, so that it is dropped during the
extraction and you again get the algorithm you initially had in mind.
So these new techniques bring more than just total computable
functions, and they still are encoded using the Fixpoint construct.

One key disadvantage of functions with extra proof arguments is that
they do not compute well inside Coq, so that they are less suitable
for things like proof by reflection, for instance.

To date, we conjecure that any purely functional recursive algorithm
without nested recursion can be encoded as a function in Coq, if we
allow ourselves to add an extra argument in the sort Prop.  But should
we consider it is still the same algorithm?  Probably we should, because
we can design the Coq function so that the extracted function
implements exactly the algorithm we have in mind.

The best supported technique currently available to define a general
recursive function is the definition by well_founded_induction.
Eduardo Giménez' tutorial is a good reference.  Pierre Castéran and I also
provide a few examples of using this method to define algorithms in
the chapter "Récursivité Générale" of the book we plan to publish any
time soon.  You can have access at an old version of this book on the
following web side:

ftp://ftp-sop.inria.fr/lemme/Yves.Bertot/bouquin/coqart.ps.gz

You can find the solutions to a few exercises at the following web-site:

http://www.labri.fr/Perso/~casteran/EXPORTABLE/gen-rec/index.html

We hope to publish this book before the end of the year.

In a more recent version (but not publicly available) we also describe
Ana Bove's method.  It is more elegant but it requires a
much stronger ability to handle dependent types and induction.

I hope this helps,

  Yves

Yves.Bertot AT inria.fr
  Tel: (+33/0)4 92 38 77 39  Fax: (+33/0)4 92 38 50 60
INRIA Sophia-Antipolis 2004, route des lucioles, B.P. 93,
06902 Sophia Antipolis Cedex (France).
http://www.inria.fr/lemme/Yves.Bertot