Lambda Calculus: an Elm CLI

Introduction

The lambda calculus, sometimes described as the world’s smallest programming language, was devised by Alonzo Church in 1932–33 as new foundation for logic. A term (think “phrase”) in the lambda calculus is made up of just three grammatical entities: variables, abstractions, and applications. Variables are things like x, y, z, ... . An abstraction (λx.E), where E is a lambda term, defines a function of x. For example, (λx.2x + 1) is the function that doubles whatever x is, then adds 1. The expression (λx.2x + 1) (3) is an application. Its meaning is given by the rule of substitution: in the body of the abstraction, namely the expression 2x + 1, replace every occurrence of x by 3, obtaining 7.

To summarize: we have variables, abstractions, used to define functions, and applications, used to apply functions to data. Application is carried out by the rule of substitution.

In the pure lambda calculus, we have only variables, abstractions, and applications. An expression like 2x + 1 is therefore not part of the pure lambda calculus. It is made up of the integers 1 and 2 and the operations of addition and multiplication. Nonetheless, it is possible to encode the integers in the lambda calculus and with these encodings to define addition, multiplication, and all the rest of arithmetic. Even more is true: anything that can be computed can be expressed in the lambda calculus. This is the Church-Turing thesis. Another way of stating the Church-Turing thesis is that the operation of a universal Turing machine may be encoded in the lambda calculus and, conversely, that one can write a program for a Turing machine that carries out arbitrary computations in the lambda calculus.

A Lambda Calculator

As a tool to use in my quest to understand the lambda calculus, I wrote a small program in Elm to “run” the lambda calculus. Easier than writing for a Turing machine. Here is a sample session:

$ lambda
Welcome! type :help for help
> (\x.x) (\y.y)
λy.y

Here the text \x.x is the way we write λx.x at the keyboard. We apply this lambda expression to the lambda expression λy.y when we say (\x.x) (y.y). The rule of substitution says “in the body of λx.x, namely x, replace all occurrences of x by λy.y. If we do that, we get λy.y. The lambda term λx.x is the identity function: apply it to anything, and it returns what you give it.

As with any good calculator, we can store things for later use:

> :let id = \x.x
added id as λx.x
> id id
λx.x

Our lambda calculator comes with a “standard library,” as displayed below. The Boolean values of true and false are encoded as λx.λy.x and λx.λy.y, respectively. Encodings of the natural numbers zero, one, two, and three are also given. Working by hand or with the lambda calculator, one finds that succ zero = one, succ one = two, etc. Thussucc is the successor function: the function that adds one to any natural number.

# Standard Libary
# Booleans
true      \x.\y.x
false     \x.\y.y
and       \p.\q.p q p
or        \p.\q.p p q
not       \p.p (false) true

# Church numerals
zero      \s.\z.z
one       \s.\z.s z
two       \s.\z.s s z
three     \s.\z.s s s z
isZero    \n.n (\x.zero) true
succ      \n.\f.\x.f(n f x)

Let’s check out the standard library by doing some Boolean algebra computations

> and true true
λx.λy.x
> and true false
λx.λy.y
> and false false
λx.λy.y

Implementing the Calculator in Elm

To implement the calculator in Elm, we begin with a definition that captures the notion of a lambda term:

type Expr
    = Var String
    | Lambda String Expr
    | Apply Expr Expr

Some examples where we parse a string representation of a lambda term to a value of type Expr:

> :parse x
Ok (Var "x")
> :parse \x.x
Ok (Lambda "x" (Var "x"))
> :parse (\x.x) \y.y
Ok (Apply (Lambda "x" (Var "x")) (Lambda "y" (Var "y")))

The relevant code can be found at jxxcarlson/elm-lambda: a package and an app that runs on the command line. There is also the GitHub repo.

Brief summary of the various modules:

Lambda.Expression: the type Expr and the function beta : Expr -> Expr that does beta reduction, aka computation.

Lambda.Parser: parse strings to Exprs.

Lambda.Defs: the machinery for setting up a dictionary mapping names to string representations of lambda terms so that we can say and true false instead of

(\p.\q.p q p) (\x.\y.x) (\x.\y.y)

Lambda.Eval: the function eval: Dict String String -> String -> String that is used to run the calculator in the app folder.

References

Lambda Calculi, in Internet Encyclopedia of Philosophy

Lambda Calculus (Wikipedia)

Church, Alonzo. 1932. “A Set of Postulates for the Foundation of Logic (Part I).” Annals of Mathematics, 33(2):346–366.

Church, Alonzo. 1933. “A Set of Postulates for the Foundation of Logic (Part II).” Annals of Mathematics, 34(4):839–864.

Addenda

Output options

I’ve added some additional output options. The default is :pretty. Switch between options using :named, :pretty, and :raw:

> and true false
false

> :pretty
> and true false
λx.λy.y

> :raw
> and true false
\x.\y.y

> :named
> and true false
false

Recall that when you type in a lambda expression with no :command, the expression is beta-reduced.

:beta command

The :beta command checks for beta-equivalence of two terms:

> :beta (succ zero) one
true

It does alpha-conversion, aka renaming variables:

> :beta (\x.x) (\a.a)
true

And it has some guards against divergent expressions. Let omega = λx.x x and let Omega = (λx.x x)(λx.x x). Then we have

> Omega
TOO MANY SUBSTITUTIONS (size2 > 100000). Term may be divergent
> :beta Omega Omega
LHS may be divergent