[Haskell-cafe] Lambda Calculus question on equivalence

[Timon Gehr]

On 05/02/2013 11:33 PM, Francesco Mazzoli wrote:
> At Thu, 02 May 2013 23:16:45 +0200,
> Timon Gehr wrote:
>>> Yes, they can.  Take ‘f = λ x : ℕ → x + x’ and ‘g = λ x : ℕ → 2 * x’.
>> Those are not lambda terms.
>
> How are they not lambda terms?
>

I guess if + and * are interpreted as syntax sugar then they are lambda 
terms with free variables. In this case, they are not equivalent.

>> Furthermore, if those terms are rewritten to operate on church numerals,
>> they have the same unique normal form, namely λλλ 3 2 (3 2 1).
>
> You are assume things about the implementation of natural numbers, of *, and +
> (admittedly they were underspecified on my side :).  They could be implemented
> in different way, or I could simply change the second definition to ‘λ x → x *
> 2’, in which case execution would be stuck on the abstract variable.
>

AFAICS this does not show anything either, as the terms λλλ 3 2 (3 2 1) 
and λλ 2 (λ 2 (2 1)) are not extensionally equivalent. (since their 
domain is not restricted to terms corresponding to church numerals. Eg. 
feed them λλ 2.)

> In any case, definitionally different functions can be extensionally equal,
> there is little doubt on that.
>
>>> These terms are not ‘definitionally’ equal (which could be the α-equivalence you cite
>>> but can be extended to fancier checks on the term structure).  However, for all
>>> (well typed)  inputs the result of those two functions are the same: they are
>>> ‘extensionally’ equal [1].  The first part (...(L A) is equivalent to (L B)...)
>>> holds: the same function will always produce the same output given
>>> definitionally equal arguments.
>>> ...
>>
>> (I guess the question is about untyped lambda calculus.)
>
> I don’t think so, since Ian talked about ‘terminating’ λ-calculus, while
> the untyped λ-calculus isn’t...

'terminating' does not occur in the original post.

> otherwise you can’t normalise and compare.
>...

The terms in question are already normalised.