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