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



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



On 12/14/2013 4:29 AM, John Wickerson wrote:
Hi Yannick,

The counterexample involves having f as the constant "True" function, and then picking "a" to be False. The assumption in your lemma can be rewritten as

∀x. (f(x) = x ∨ f(x))

and this certainly holds when f is the constant "True" function, since both sides of the =-operator are True. But the conclusion of your lemma doesn't hold since f(False) is not False.

Does that help?

john





On 14 Dec 2013, at 10:15, Yannick Duchêne (Hibou57)<yannick_duchene at yahoo.fr>  wrote:

My ashamed apologizes if this looks as weird as I'm afraid it may looks, however, this question really tickles me.

I came to something like this after some simplifications, so I wanted to test it with a lemma:

    lemma "f = (λa. a ∨ f a) ⟹ (f a = a)"

Isabelle tells me it found a counter example with “a = False” and “f a = True” . It does not seems to see there is an infinite recursion, or else I don't understand how it can believe “f a” may differs from “a” (how so?).

To me, it can only be “a”, an infinite never ending sequence of disjunctions of the same term may be nothing else if it's ever something, than this term.

I guess this case looks weird, but I would like to know, first if Isabelle sees it as an infinitely recursive lambda expression or not, then if if it do, if there exists some trusted axioms which are able to deal with this?


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