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

Le Wed, 18 Dec 2013 23:55:03 +0100, Gottfried Barrow <gottfried.barrow at> 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:

    theory Test
    imports Main

(* 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.” [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.