Lambda Calculus: an Elm CLI

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.

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:

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:

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.

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

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

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

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

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

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

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

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

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

It does alpha-conversion, aka renaming variables:

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

--

--

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store