[Haskell-cafe] Lambda Calculus question on equivalence

[Francesco Mazzoli]

At Fri, 03 May 2013 00:44:09 +0200,
Timon Gehr wrote:
> 
> 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.

+ and * should be interpreted as term definitions, that can be replaced with the
actual body, whatever that might be.  I’m not sure about the ‘sugar’ you are
talking about... but again these details don’t really matter.

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

That’s a good point, but I was talking about typed terms.  I guess the
discussion does change if you go into the untyped lambda calculus but then you
are opening a big can of worms regarding to termination (see below).

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

‘normal form’ does, which is what I was referring to.

> > otherwise you can’t normalise and compare.
> >...
> 
> The terms in question are already normalised.

‘(L A)’ and ‘(L B)’ are clearly not normalised (if L is a function).  If the
calculus is not terminating you need to explain what’s your strategy when
comparing things that are not in a normal form already.

Francesco