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



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


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

> To tell it another way, my erroneous interpretation was to believe it was the same as a definition of “f”, while both an explicit “definition” and a “fun/function” definition fails with such an expression:
> 
>    definition f where "f = (λa. a ∨ f a)" (* Isabelle complains “Extra variables on rhs: "f"”. *)
> 
>    fun f where "f a = (a ∨ f a)" (* Isabelle complains “Could not find lexicographic termination order”. *)
> 
> For the second case, no way to try with “function”, as that's absolutely non‑terminating.
> 
> So this was like an attempt to define something impossible to Isabelle, and also after some comments here, something HOL can't deal with. Finally, in the absence of any real definition, Quickcheck was free to substitute “f” to whatever it wanted. This should summarize the case.





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