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.