This is a foray into untyped lambda calculus using Python. The code is entirely impractical, definitely wouldn't recommend using any of this in a real-world program.
We will assign names to certain expressions and use them to build more complex expressions. However, we'll imagine that these are not functions that can call themselves, but just shorthands that expand to the expression they denote, assuming automatic renaming (α-conversion) to avoid name collisions.
We start with some basic Boolean logic. True and false are represented as functions that take two arguments and select the first or second argument respectively.
TRUE = lambda x: lambda y: x FALSE = lambda x: lambda y: y
These definitions give us a simple conditional
if-else construct, which we can make more explicit with another shorthand definition.
IFELSE = lambda p: lambda x: lambda y: p(x)(y)
To translate these Booleans to the built-in Python Booleans, we just need to apply them to
BOOL = lambda b: b(True)(False)
Defining basic operations of Boolean algebra is easy if we think in terms of our first abstractions. For
NOT we simply reverse the order of the arguments, so that
AND the first argument selects the second if it is
TRUE and itself if it is
OR it's exactly the other way round.
NOT = lambda p: p(FALSE)(TRUE) AND = lambda p: lambda q: p(q)(p) OR = lambda p: lambda q: p(p)(q)
To implement the equality predicate for Boolean values, we can build on these basic Boolean operations.
EQB = lambda p: lambda q: OR (AND(p)(q)) (AND (NOT(p)) (NOT(q)))
Let's give it a try.
BOOL(NOT(TRUE)) # False BOOL(AND(NOT(FALSE))(NOT(FALSE))) # True BOOL(OR(NOT(FALSE))(FALSE)) # True BOOL(EQB(NOT(FALSE))(TRUE)) # True
We continue with Curch pairs and immutable lists. A pair is just a function that takes a function as argument and applies it to two expressions. I use the Lisp names for the basic operations. Remember that
TRUE selects its first argument,
FALSE its second argument.
CONS = lambda x: lambda y: lambda f: f(x)(y) CAR = lambda l: l(TRUE) CDR = lambda l: l(FALSE)
Starting from Church pairs there are different ways to represent lists, let's use the shortest.
NIL = FALSE ISNIL = lambda l: l(lambda h: lambda t: lambda b: FALSE)(TRUE)
ISNIL applies it to two arguments, the second of which is
ISNIL(NIL) obviously works. Otherwise we eventually end up with
(lambda h: lambda t: lambda b: FALSE) (CAR(l)) (CDR(l)) (TRUE), which is always
Here are some examples involving list operations.
BOOL(ISNIL(NIL)) # True BOOL(ISNIL(CONS(TRUE)(NIL))) # False BOOL(CAR(CONS(TRUE)(NIL))) # True BOOL(ISNIL(CDR(CONS(TRUE)(NIL)))) # True
We use Church numerals to represent natural numbers. Each Church numeral is a function that accepts a function and an expression. We start with
ZERO, which just returns the expression, and obtain the successor by wrapping a numeral into another function. So n-fold composition gives us the natural number n.
ZERO = lambda f: lambda x: x SUCC = lambda n: lambda f: lambda x: f(n(f)(x))
To check for zero, we use the fact that
ZERO is equivalent to
FALSE, so it just selects the second argument, which hence must be
TRUE. Otherwise we pass a function to the numeral that evaluates to
FALSE, independent of the argument, so
ISZERO evaluates to
FALSE for all successors of
ISZERO = lambda n: n(lambda x: FALSE)(TRUE)
It's hard to read Church numerals, so it will be convenient to have a function that translates them to the built-in Python numbers.
ARABIC = lambda n: n(lambda x: x + 1)(0)
Let's type a few examples again.
BOOL(ISZERO(ZERO)) # True ARABIC(SUCC(ZERO)) # 1 ARABIC(SUCC(SUCC(ZERO))) # 2 ...
We got some basic Boolean logic, we have lists and numbers with nil and zero checks, let's put it together to do something interesting with recursion. How about a length function for lists? It should take a list as its argument and return a Church numeral representing the length of the list.
In the beginning I said that our definitions are not able to call themselves (in practice they are, but let's pretend). Luckily, after reading chapter 9 of The Little Schemer, I know a neat trick to build recursive functions in lambda calculus: the applicative-order Y combinator.
Y = lambda le: (lambda f: f(f)) (lambda f: le(lambda x: f(f)(x)))
I won't try to explain it here, because a single sentence wouldn't be enough, but I think the The Little Schemer does a good job at that.
Now we define the function that will fill
le. It takes a function
length as argument and produces a function that takes a list and evaluates to
ZERO if the list is
NIL or the successor of
length applied to
CDR(l). The function
length will be supplied by the Y combinator in terms of
LENGTH itself. The definition is quite long, so I adopt a more Lispy indentation style.
LENGTH = (lambda length: (lambda l: (IFELSE (ISNIL (l)) (ZERO) (SUCC (length (CDR (l)))))))
Let's try this on the empty list
NIL by evaluating
ARABIC(Y(LENGTH)(NIL)) to get 0.
RecursionError: maximum recursion depth exceeded
Oh no, a recursion error on the empty list! This doesn't look good. Is there a mistake in one of our definitions? No, not really. The problem is that Python evaluates function arguments eagerly, so already the first time
IFELSE is evaluated, we run into infinite recursion in its third argument.
What can we do? We are cheating. We convert our Church Boolean to a Python Boolean and use the built-in if-else construct, which only executes one of its branches.
LENGTH = (lambda length: (lambda l: (ZERO) if BOOL(ISNIL(l)) else (SUCC(length(CDR(l))))))
Now it works.
ARABIC(Y(LENGTH)(NIL)) # 0 ARABIC(Y(LENGTH)(CONS(TRUE)(NIL))) # 1 ARABIC(Y(LENGTH)(CONS(TRUE)(CONS(TRUE)(NIL)))) # 2 ...
Friedman, D. P., & Felleisen, M. (1996). The Little Schemer. MIT Press.