[Haskell-beginners] pred (succ n)
benedikt.ahrens at gmx.net
Thu Nov 4 11:21:17 EDT 2010
this question is somewhat similar to the one I've asked some hours ago:
I would like to have a predecessor operator PRED for the untyped lambda
calculus that has the property that
PRED (SUCC n) --> n (I)
for a suitable successor function SUCC.
So far I've tried with
SUCC := S := \nfx.f (n f x)
PRED := P := \nfx.n (\gh.h (g f)) (\u.x) (\u.u)
for which I can prove beta equivalence
P (S n) == n
by induction on n, but not the property (I).
Could anybody give me a pointer?
ps. Please keep me in CC, since I'm not currently subscribed to the list.
More information about the Beginners