Re: [isabelle] Infinitely recursive lambda expression or not?
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
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.
Le Fri, 27 Dec 2013 00:07:23 +0100, Yannick Duchêne (Hibou57)
<yannick_duchene at yahoo.fr> a écrit:
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 an
equality which in turn allows a substitution, and so, recursively. Ex:
(* Based on the original proposition which was: "f = (λa. a ∨ f
a) ⟹ (f a = a)" *)
lemma "f = (λa. a ∨ f a) ⟹ f = (λa. a ∨ (λa. a ∨ f a) a)" by simp
lemma "f = (λa. a ∨ f a) ⟹ f = (λa. a ∨ (λa. a ∨ (λa. a ∨ f a) a)
a)" by simp
(* And so on… *)
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.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and