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



On Sat, 14 Dec 2013 11:29:47 +0100, John Wickerson <johnwickerson at cantab.net> wrote:

Hi Yannick,

Hello John, and thanks for your interest in the question.

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?

I don't know so far, will see if I understand. At least you seem to confirm Isabelle really understand it as a recursive function application (I had a doubt on this for a moment).

Why is f(False) not False ? If it's built with False only and only disjunctions, where could True comes from?

Or else may be my interpretation is wrong: I see it as an infinite sequence like “x ∨ x ∨ x ∨ x ∨ x ∨ …”.

For the longer story, what I was attempting with this lemma, is to get a rule for elimination of this particular kind of infinite recursion. A more general case could be (in my interpretation which may be erroneous, I don't know so far): let “+” be an operator, let the proposition “a + b = a” be previously proved to holds, then an infinite sequence like “a + b + b + b + b + …” may be substituted to “a”; that was the meaning I expected.

May be there is a way to prove it with something like a list induction and proving the function recursion is like the list recursion on an infinite list. May be with a list I could say “what ever the length of a + b + b + b + b + … it will always be a when a + b = a” so the infinite length list produce the same if it's interpreted as producing anything (already hardly provable I believe). Just that it's not a list, it's a recursive function instead. Then I wondered if there exist an axiom for this in any kind of theory (either that of Isabelle or from foreign theories) or else if it would be safe to create one, and I'm afraid of creating an axiom which I'm not able to prove (so a pure axiom, not a theorem).

--
Yannick Duchêne




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.