What's in a Language?

A programming language is a syntax that tells a computer what instructions to execute.

While many, many languages exist, the choice between them is largely stylistic: almost all languages are Turing-complete, meaning the sets of problems they can solve are equal.

Informally, a language is Turing-complete if it can compute any function whose values are expressible in terms of an algorithm.

Why so Small?

By understanding extremely minimal Turing-complete languages, we can therefore better understand programming in general.

They're pretty impractical to ever actually use, but their simplicity also makes them fun to explore, like Peano arithmetic for computer science.

Branching

Traditionally, a Turing-complete language includes the ability to branch: what we think of as if statements.

If we're interested in making a tiny grammar for a language, though, we can get away with much less: recursion.

This is a small part of a fundamental difference in languages, which exist on a spectrum from imperative, where code tells the computer what to do, to functional, where code tells the computer how to do things.

Iterative Algorithms

function factorial(n)
{
    let product = 1;

    for (let i = 1; i <= n; i++)
    {
        product *= i;
    }

    return product;
}

function factorial(n)
{
    if (n === 0)
    {
        return 1;
    }

    return n * factorial(n - 1);
}

Lambdas

Introduced by Alonzo Church in 1936, lambda calculus is an extremely barebones language for expressing functions.

Let's start with functions, since we need those to do recursion. We write these as λx.E: the λ is a formal symbol that indicates a function, x is its argument, and the return value is E.

For example, λx.x is the identity function.

λx.λy.x takes in x and returns a function that takes in an argument y, discards it, and returns x.

Beta Reduction

The other thing we need to do with functions is plug things into them, which we indicate by (left-associative) juxtaposition.

(λx.E)y means we plug y into the function λx.E.

To actually perform the evaluation, we define an equivalence relation on lambda expressions, with the process of evaluating an expression known as beta reduction.

If E and y are lambda expressions, then (λx.E)y can be beta reduced to E with every x replaced by a y. We write E ≡ F for expressions that can both beta reduce to the same expression.

Diagrams

Lambda diagrams have a beautiful visual representation, introduced by John Tromp and defined recursively.

A lambda like λx.E is represented by a horizontal line over the diagram for E.

A variable like x is represented by a vertical line drawn down from its binding lambda's horizontal line. An expression E used in an evaluation is represented by a vertical line drawn down from its expression's diagram.

An evaluation like EF is represented by connecting the vertical lines for E and F with a horizontal line.

Constants

At this point, we might expect to start introducing formal constants that represent numbers, booleans, and so on, but the magic of lambda calculus is that we can represent all of these with irreducible lambda expressions.

Booleans

By conventions, booleans are two-argument selector functions: true is T := λx.λy.x and false is F := λx.λy.y. We can build up boolean operators from these.

Not: ! := λb.bFT

And: & := λb.λc.bcF

Or: | := λb.λc.bTc

Church Numerals

We represent nonnegative integers by repeated composition: for example, 3 := λf.λx.f(f(f(x))).

These are more complicated to work with, but we can begin with a function that tests if a number is zero: _ := λn.n(λx.F)T.

Successor: > := λn.λf.λx.f(nf(x))

The predecessor operator < is much more complicated, since there isn't a natural way to undo function application. We'll get to it later if there's time.

Arithmetic

Addition: + := λa.λb.λf.λx.(af)(bfx).

Multiplication: * := λa.λb.λf.b(af).

Exponentiation: ^ := λa.λb.ba.

Recursion

Let's try to define the factorial function f:

f := λn._(<n)1(*n(f(<n)))

Unfortunately, this definition is recursive and therefore not a valid lambda expression.

For any expression g,

Yg = (λf.(λx.f(xx))(λx.f(xx)))g

   ≡ (λx.g(xx))(λx.g(xx))

   ≡ g((λx.g(xx))(λx.g(xx)))

   = g(Yg)

   ≡ g(g(Yg))

   ≡ g(g(g(Yg))) ≡ ...

Now Yλf.λn._(<n)1(*n(f(<n))) is the factorial function!

Iterative Methods

Unfortunately, recursion is slow and kind of awful. We can improve it with an iterative design, much closer to a for loop.

The design (λn.n(λg.λa.λb.g(>a)(*ab))(λa.λb.b)11)4 looks bad, but isn't terrible if we explain it in symbols: if we let L := λg.λa.λb.g(>a)(*ab), then

$$\begin{align*} L(g) &= (a, b) \mapsto g(a + 1, ab) \\ L(L(g)) &= (a, b) \mapsto L(g)(a + 1, ab) \\ &= (a, b) \mapsto g(a + 2, (a+1)ab) \end{align*}$$

The loop design iterates L a total of n times, and then sets g = λa.λb.b, which extracts the second argument of the pair. The result is a function

$$(a, b) \mapsto (a + n)(a + n - 1)\cdots(a + 1)ab,$$

and we finally set $a = b = 1$.

To close out, here's a function I designed that computes $a \uparrow^n b$:

Yλf.λn.λa.λb.
(
    _(<n)
    (
        ba
    )
    (
        ( (<b) (λg.λc.λd.gc(f(<n)cd)) ) (λc.λd.d) a a
    )
)

Thank You!