coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Russell O'Connor" <roconnor AT Math.Berkeley.EDU>
- To: Jean-Yves Vion-Dury <jean-yves.vion-dury AT inrialpes.fr>
- Cc: Coq Club <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] Expressiveness of Fixpoints
- Date: Tue, 14 Oct 2003 16:34:56 -0700 (PDT)
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
[To:
jean-yves.vion-dury AT inrialpes.fr,
coq-club AT pauillac.inria.fr]
On Tue, 14 Oct 2003, Jean-Yves Vion-Dury 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) ?
Someone can correct me if I'm wrong, but a good example of a recursive
function that (hopefully) terminates but cannot be represented using
Fixpoints in Coq is an algorithm that ``normalizes Coq terms that use only
Fixpoint (and does not use CoFixpoint of course)''.
I hope that was understandable.
- --
Russell O'Connor <http://math.berkeley.edu/~roconnor/>
Work to ensure that Iraq is run by Iraqis.
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.2.1 (SunOS)
iQCVAwUBP4yIJE0+aO5oRkNZAQITqAP/cMFvrI9BYyD6xiNdOgc4u8yij/FFowfs
uY4pwTbJqD6IMldSGB4MAWI8SxdYWaL0vupbuR85JUwu8S1GaspMtWhPRL92epl2
9ZybIpny34KtvZDy1EPBTHkYOiiwvO2srMp5rOYcknlHJ6JFKVZ0UCtITjRqcMLO
Hb/IzFwTVh8=
=53T1
-----END PGP SIGNATURE-----
- [Coq-Club] Expressiveness of Fixpoints, Jean-Yves Vion-Dury
- Re: [Coq-Club] Expressiveness of Fixpoints, Eduardo Gimenez
- Re: [Coq-Club] Expressiveness of Fixpoints, Russell O'Connor
Archive powered by MhonArc 2.6.16.