The Coq mailing list

[Jean-Yves Vion-Dury <jean-yves.vion-dury AT inrialpes.fr>]

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) ?

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)

Jean-Yves

--

Jean-Yves Vion-Dury   Research Scientist	Xerox Research Centre Europe
INRIA (sabbatical) 655 avenue de l'Europe, 38334 Montbonnot (FRANCE) Jean-Yves.Vion-Dury AT inrialpes.fr	from France:   0 4 76 61 53 83 from abroad: +33 4 76 61 53 83
you may have a look at the Circus Transformation Language?	www.alphaAve.com