[Haskell-cafe] Lambda Calculus question on equivalence

[Francesco Mazzoli]

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?

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

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... otherwise you can’t normalise and compare.

Besides that, the typed calculi I cited are interesting because they internalise
some notion of equality, but the observation about function extensionality holds
with or without types.

Francesco