*To*: "Yannick Duchêne (Hibou57)" <yannick_duchene at yahoo.fr>*Subject*: Re: [isabelle] Infinitely recursive lambda expression or not?*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Fri, 27 Dec 2013 17:33:49 +0000*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <op.w8rgogrkule2fv@cardamome>*References*: <op.w72usxweule2fv@cardamome> <C743CBFE-029F-4E49-9A56-3695338394B8@cantab.net> <52AC4D87.9030304@gmx.com> <op.w723lrn9ule2fv@cardamome> <52B227C7.6070607@gmx.com> <op.w8p2ilo1ule2fv@cardamome> <op.w8rgogrkule2fv@cardamome>

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.

**Follow-Ups**:**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*Yannick Duchêne (Hibou57)

**References**:**[isabelle] Infinitely recursive lambda expression or not?***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*John Wickerson

**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*Gottfried Barrow

**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*Gottfried Barrow

**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*Yannick Duchêne (Hibou57)

- Previous by Date: Re: [isabelle] Infinitely recursive lambda expression or not?
- Next by Date: Re: [isabelle] Infinitely recursive lambda expression or not?
- Previous by Thread: Re: [isabelle] Infinitely recursive lambda expression or not?
- Next by Thread: Re: [isabelle] Infinitely recursive lambda expression or not?
- Cl-isabelle-users December 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list