Full implementation of Factorial in Lambda Calculus using Python.

factorial.py

#!/usr/bin/env python

# As you know there is NO Assignment in Lambda Calculus (LC),
# and all those functions must be inlined using LC's
# substitution rule. But if I do that this code will look extremely
# gross and unreadable. So I keep it this way for comprehensibility
# reasons.
#
# This was SO MUCH fun to implement and quite an interesting puzzle
# to solve. This whole thing was completely inspired by Gary Bernhardt's
# screencast on Lambda Calculus at:
#   https://www.twitch.tv/gary_bernhardt/v/90270724!
#
# I recommend you to check it out!

EMP     = (
    lambda x: x
)

ZERO    = (
    lambda f: lambda x: x
)

TRUE    = (
    lambda t: lambda f: t(EMP)
)

FALSE   = (
    lambda t: lambda f: f(EMP)
)

IF      = (
    lambda cond: lambda t: lambda f: cond(t)(f)
)

IS_ZERO = (
    lambda n: n(lambda _: FALSE)(TRUE)
)

## SUCC/ADD1

SUCC    = (
    lambda n: lambda f: lambda x: f( n(f)(x) )
)

## SUB1/PRED

MK_PAIR = (
    lambda a: lambda b: lambda s: s(a)(b)
)

FST     = (
    lambda a: lambda b: a
)

SND     = (
    lambda a: lambda b: b
)

STEP    = (
    lambda p: MK_PAIR(p(SND))(SUCC(p(SND)))
)

STEPS   = (
    lambda n: lambda p: n(STEP)(p)
)

ZZ      = (
    MK_PAIR(ZERO)(ZERO)
)

PRED    = (
    lambda n: STEPS(n)(ZZ)(FST)
)

ADD     = (
    lambda n: lambda m: n(SUCC)(m)
)

MULT    = (
    lambda n: lambda m: (PRED(n))(ADD(m))(m)
)

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

FACT    = (
    lambda f: lambda n: (
      IF(
        IS_ZERO(n)
      )(
        SUCC(ZERO)
      )(
        lambda _: MULT(n)(f(f)(PRED(n)))
      )
    )
)

print(
    FACT(
      FACT
    )(
      SIX
    )(
      lambda x: x + 1
    )(
      0
    )
) #=> 720