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



Le Sat, 14 Dec 2013 13:22:31 +0100, Gottfried Barrow <gottfried.barrow at gmx.com> a écrit:

Yannick,

I just make more explicit what John says with regards to the constant function, and also, explicitly, for any free variables in a lemma, there is implicit universal quantification of those free variables, something which Christian Sternagel made explicit enough with explicit examples to conclusively show, for me, the connection between free variables and universal quantification.

There can be lots of implicit action working underneath.

You're stating this:

lemma "!!f. !!a. f = (%a. a | f a) ==> (f a = a)"
oops

So, let "f = (%a. True)", and for the quantified variable "a", let "a = False".

Then

lemma "(%x. True) = (%x. x | (%x. True) x) ==> ((%x. True) False ~= False)"
by(simp)

Regards,
GB

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.


I won't go with an axiom, looks unsafe if I am missing something.


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