The Coq mailing list

[Eduardo Gimenez <Eduardo.Gimenez AT trusted-logic.fr>]

On Tuesday 14 October 2003 10:25, you wrote:
> Dear Coq'ers,
>
> I wonder if the Fixpoint construction allows the capture of any
> terminating recursive scheme ? In other word, can we say that any
> "valid" (i.e. terminating) recursive computation can be modeled in Coq
> (I do not consider CoFixpoint and CoInduction) ?

No, it only captures a class of recursive definitions usually known as 
"structurally smaller definitions". Actually, determining whether a given 
recursive function terminates is an undecidable problem, so there is no 
hope that a Fixpoint could capture the whole class of terminating functions.

> Any hint from coq theoricists welcome. ( concretely, I have to capture a
> working recursive scheme, and I have to deal with coq's syntactic
> constraints, and...this more general question came to my mind)

You can rather use the so-called well-founded induction, based on the 
accessibility predicate (acc). This is much stronger than the syntactical 
principle used by Fixpoint, but it's up to you to *prove* that your function 
terminates. 

You may take a look to an example of well-founded induction in my (rahter 
old) tutorial on recursive types, available at Coq's web site.

Cheers,
Eduardo.