*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Infinitely recursive lambda expression or not?*From*: Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr>*Date*: Fri, 27 Dec 2013 18:10:54 +0100*Organization*: Ada @ Home*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>*User-agent*: Opera Mail/12.16 (Linux)

Le Wed, 18 Dec 2013 23:55:03 +0100, Gottfried Barrow<gottfried.barrow at gmx.com> a écrit:On 12/14/2013 7:26 AM, Yannick Duchêne (Hibou57) wrote:I wanted to check if had an issue with binding (indeed, I did had issues with implicit operations in some cases), so tried this: lemma "f = (λa. False ∨ f False) ⟹ (f False = False)" It still says it find a counter example, with “f False = True”. Precisely, what I don't understand, is why it suppose this may be True. “a” is not used, and the only constant used in f is False. I must be missing something important, or else it's just Auto Quickcheck which is not made for this kind of infinite expression.You might have worked this out already, but I attach and include a THY which has comments. You're treating "=" as programming language assignment, but it's not. You're also speaking of non-terminating, recursive functions, but they don't exist in HOL, so I've read, I think.I did not really interpreted this as an assignment, rather as anequality which in turn allows a substitution, and so, recursively. Ex:theory Test imports Main begin(* Based on the original proposition which was: "f = (λa. a ∨ fa) ⟹ (f a = a)" *)lemma "f = (λa. a ∨ f a) ⟹ f = (λa. a ∨ (λa. a ∨ f a) a)" by simplemma "f = (λa. a ∨ f a) ⟹ f = (λa. a ∨ (λa. a ∨ (λa. a ∨ f a) a)a)" by simp(* And so on… *) end That's why I saw an infinite recursion. I will have a look later in your extensive sample.

-- “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

**Follow-Ups**:**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*Lawrence Paulson

**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)

- 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