Re: [isabelle] Infinitely recursive lambda expression or not?



You could try Isabelle/HOLCF, but I’m not sure how well documented and supported it is.

Larry Paulson


On 27 Dec 2013, at 17:47, Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr> wrote:

> Le Fri, 27 Dec 2013 18:33:49 +0100, Lawrence Paulson <lp15 at cam.ac.uk> a écrit:
> 
>> From a computational point of view, "f a = (a ∨ f a)” must be regarded as undefined, because the recursion is not well-founded. There are logics where you could then prove that f(True)=True and f(False)=undefined.
>> 
>> Larry Paulson
>> 
> 
> Interesting. Just out of curiosity and learn more (really not to use it), what are the names of these logics?
> 
> 
> -- 
> “Syntactic sugar causes cancer of the semi-colons.” [1]
> “Structured Programming supports the law of the excluded muddle.” [1]
> [1]: Epigrams on Programming — Alan J. — P. Yale University
> 
> 





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