[Haskell-beginners] pred (succ n)

ben 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 mailing list