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 True and False.
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 TRUE selects FALSE and FALSE selects TRUE.
In AND the first argument selects the second if it is TRUE and itself if it is FALSE.
In 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)
If l is NIL (or FALSE), ISNIL applies it to two arguments, the second of which is TRUE, so 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 FALSE.
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 ZERO.
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.
This page was moved from my old website.