Re: [isabelle] Non terminating function proven terminating



Thanks for all the comments: I now understand a bit more the philosophy
behind Isabelle. Given that extraction remains safe (I guess that the simps
equations are the one used to generate the code?), I suppose that this is
just a matter of taste.

--
guillaume


On 22 October 2011 13:58, Makarius <makarius at sketis.net> wrote:
> You quote this like something that is well-known in the constructive
> community.  Can you point to some mailing list threads discussing it, or
> similar?

I don't know if it's really well-known: I was just giving credits to the one
that discovered it. In the meantime Andreas Abel told me that it was actually
older than Pierre's remark:

« No this trick is old, and documented in Barthe et al, MSCS 2004, page 3,
point 3b. »

http://code.google.com/p/agda/issues/detail?id=497
http://journals.cambridge.org/abstract_S0960129503004122



On 22 October 2011 23:53, Alexander Krauss <krauss at in.tum.de> wrote:
> You seem to be using a specific notion of "well-defined", probably coming
> from constructive type theory.

Guilty as charged! Now that I put back my classical glasses, I can understand
that "\lambda (). ()" can also be seen as a well defined solution (it
works + every
other solution has to be extensionally equal).





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.