Implementing SUB1 function in Lambda Calculus using Python via the "Wisdom Tooth Trick"!

sub1.py

# This is the implementation of SUB1 in Lambda Calculus (LC)
# using the "Wisdom Tooth" trick! Apparently for some time,
# even Alonzo Church didn't believe SUB1 is a feasible operation
# in LC until one day his student Kleene came up with this idea.
# It's called "Wisdom Tooth" because he came up with it while he
# was at dentist :)
#
# It simply starts counting up from ZERO and at each step, remebers
# the previous value and when reaches the target, returns the previous
# value as the SUB1 result:
#
#   zero       := λf.λx.x
#   succ       := λn.λf.λx.f(n(f)(x))
#   make_pair  := λa.λb.λs.s(a)(b)
#   fst        := λa.λb.a
#   snd        := λa.λb.b
#   transform  := λp.make_pair(p(snd))(succ(p(snd)))
#   transforms := λn.λp.n(transform)(p)
#   zz         := make_pair(zero)(zero)
#   pred       := λn.transforms(n)(zz)(fst)
#
# Note that "succ" is the same as ADD1 and "pred" is the
# same as SUB1. As you know, there is NO assignment in
# Lambda Calculus, so all of those definitions must be
# inlined via LC's substitution rule, but if I do that
# this code is gonna become gross and extremely unreadable!
# So I'm gonna keep it this way for comprehensibility reasons.
#
# The following is the Python implementation of this:

ZERO    = lambda f: lambda x: x
SUCC    = lambda n: lambda f: lambda x: f( n(f)(x) )
MK_PAIR = lambda a: lambda b: lambda s: s(a)(b)
FST     = lambda a: lambda b: a
SND     = lambda a: lambda b: b
TRANS   = lambda p: MK_PAIR(p(SND))(SUCC(p(SND)))
TRANSS  = lambda n: lambda p: n(TRANS)(p)
ZZ      = MK_PAIR(ZERO)(ZERO)
SUB1    = lambda n: TRANSS(n)(ZZ)(FST)

SIX     = SUCC(SUCC(SUCC(SUCC(SUCC(SUCC(ZERO))))))

print(
  SUB1(
    SIX
  )(
    lambda x: x + 1
  )(
    0
  )
) #=> 5