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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe