2 May
2013
2 May
'13
9:37 p.m.
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