On 05/02/2013 11:37 PM, Edward Z. Yang wrote:
Excerpts from Timon Gehr's message of Thu May 02 14:16:45 -0700 2013:
Those are 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).
The trick is to define the second one as x * 2 (and assume the fixpoint
operates on the first argument). Now they are not equal.
Edward
Neither equal nor extensionally equivalent.
mult = λm.λn.λf. n (m f)
mult 2 = λn.λf. n (2 f)
mult 2 = λn.λf. n (λx. f (f x))
flip mult 2 = λm.λf. 2 (m f)
flip mult 2 = λm.λf.λx. m f (m f x)
(λn.λf. n (λx. f (f x)) const = λf. const (λx. f (f x))
= λf.λa.λx. f (f x)
This is clearly not the same as:
(λm.λf.λx. m f (m f x)) const = λf.λx. f
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
