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



It is simply that if f is the constant-True function, then f = (λa. False ∨ f False).

I think that you are imagining some sort of execution model for HOL. But HOL doesn’t have an operational semantics. 

Larry Paulson


On 14 Dec 2013, at 13:26, Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr> 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.





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