[Haskell-cafe] Lambda Calculus question on equivalence

[Timon Gehr]

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