# 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. Thus`succ`

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

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