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 non‑terminating.

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:

     theory Test
     imports Main
     begin

(* 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… *)

     end

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.