Introduction to Lambda Calculus

Lambda calculus, what a wonderful study of logic and maths! It allows us to represent all kinds of data using just functions. And with God's help I have created an interpretive programming language for the express purpose of simplifying lambda calculus expressions.

First, a brief history of Defunct. I found out about lambda calculus last year, and made a simple interpreter called LambdaSalt ("land assault", get it?), which was the precursor to Defunct. LambdaSalt was written in C#, but now Defunct is proudly written in Python. The open source code is available on GitHub here, and can be installed on Windows.

A simple Defunct script, where <expr> is an expression:


def myFunc (<expr>)

do (print myFunc)

Save it as a file (myscript.txt) and use Windows Command Prompt to run defunct.exe with it. [More help]


defunct "myscript.txt"

Notwithstanding in thy days I will not do it for David thy father's sake: but I will rend it out of the hand of thy son. 1 Kings 11:12, KJV

God keeps his promises.

The most fundamental idea of lambda calculus is that everything is a function. Numbers? Made of functions. Booleans, true and false? Functions. Comparisons like greater than, equal to, or less than? Also functions. These aren't your typical programming lanugage 'functions' like in C# or Java, no, these functions are more like data structures than procedures. So what is a function in lambda calculus?

Functions

A function takes an expression of functions as a parameter (its one and only argument), and always returns (is reduced to) another expression of functions. The argument has a name, which can be referenced multiple times within the body of the function. These references are called variables.

A function is declared like so:

Lambda Calculus	Defunct
`λ<varname>.<expr>`	`[<varname>.<expr>]`


where <expr> := <varname>

             or <function>

             or '(' <expr> ')'

             or <expr> [ <expr> [ <expr> ... ] ]

Hover over the coloured code to see tooltips.

Here are some examples:

Lambda Calculus	Defunct
`λx.x`	`[x.x]`
`λy.λx.xy λyx.xy`	`[y.[x.x y]] [y x.x y]`
`λwyx.y(wyx)`	`[w y x.y(w y x)]`
`(λx.x)(λx.x) (λx.x)(λy.y)`	`[x.x][x.x] [ x . x ] [ y . y ]`
`λxyz.y`	`[me myself i.myself]`

Each table row is equivalent in meaning between lambda calculus and Defunct.

Note that in lambda calculus all variable names must be one symbol/character, and there are no spaces anywhere. In Defunct, names can be any length, and they end when a Space character or syntax/punctuation character [].() is encountered.

Variable Scope

Variables within an expression or sub-expression can either be free or bound.

Lambda Calculus	Defunct
`λy.(λx.yx)`	`[y.[x.y x]]`

In the expression above, x is a bound variable within the red function, which means it references a function's argument within the expression. It is also bound within the blue function, because the red function (whose argument it is referencing) is within the body of the blue function.

Within the blue function, y is also a bound variable, because it references the argument y.

However, within the red function, y is a free variable, because there is no declaration of a variable y within the red function's scope.

Here's another example:

Lambda Calculus	Defunct
`λa.ab`	`[a.a b]`

In this expression, a is bound and b is free.

Reduction

We can reduce (simplify, evaluate) expressions of functions using these three techniques:

α-conversion (alpha conversion):
Changing variable names to avoid confusion.
β-reduction (beta reduction):
Applying functions (passing in parameters).
η-reduction (eta reduction):
Removing redundant wrapper functions.

Alpha Conversion

Say you have this expression:

Lambda Calculus	Defunct
`(λxy.yx)(λx.xx)`	`[x y.y x][x.x x]`

The first function has variables x and y, while the second function has variable x. But these are two entirely separate functions, with their own bound variables! Therefore, we can change one of the variable names to something different, say z, and the expression will still be identical.

Lambda Calculus	Defunct
`(λxy.yx)(λz.zz)`	`[x y.y x][z.z z]`

Defunct treats all functions as having their own unique variable, so you don't need to do any alpha conversions yourself.

Beta Reduction

A function can be applied to another function, which means the second function is copied into all the places where the first function's variable is being referenced. For example:

Lambda Calculus	Defunct
`(λx.λy.yx)(λz.zz) λy.y(λz.zz)`	`[x.[y.y x]][z.z z] [y.y[z.z z]]`

The x function is being applied to the z function, so all references to x will be replaced with the z function.

Also note that the remaining expression cannot be further simplified. The variable reference y cannot be applied to function z until it has been replaced/substituted with a function.

This example demonstrates that you can apply a function to a variable reference:

Lambda Calculus	Defunct
`λy.(λx.xxx)y λy.yyy`	`[y.[x.x x x]y] [y.y y y]`

Brackets and Series of Expressions

Just like normal maths, technically there are brackets everywhere, we just hide them for easy reading. This is why we need order of operations.

The inner-most pairs of brackets are always evaluated (reduced as much as possible) first, before any outer pairs of brackets.

Series of expressions are evaluated from left to right. This means these expressions are all identical (equivalent):

Lambda Calculus	Defunct
`abc (ab)c (((a)(b))(c))`	`a b c (a b)c (((a)(b))(c))`

And so are these two:

Lambda Calculus	Defunct
`(λa.a)(λb.bb)(λxy.y) ((λa.a)(λb.bb))(λxy.y)`	`[a.a][b.b b][x y.y] ([a.a][b.b b])[x y.y]`

But of these three, none are equivalent:

Lambda Calculus	Defunct
`abcd a(bc)d a(bcd)`	`a b c d a(b c)d a(b c d)`

Defunct stores all expressions as a syntax tree of Pairs (a left-hand-side expression and a right-hand-side expression), which is used to determine the evaluation order.

Eta Reduction

When a function's sole purpose is to pass its variable into another function, it can be reduced to just that inner function.

Lambda Calculus	Defunct
`λx.Mx M`	`[x.M x] M`
`λx.(λy.yy)x λx.xx λy.yy`	`[x.[y.y y]x] [x.x x] [y.y y]`

If the inner function contains a free variable referencing the outer function's variable, the function cannot be eta-reduced.

Lambda Calculus	Defunct
`λx.(λyz.yzx)x λx.(λz.xzx) λxz.xzx ≠λyz.yzx`	`[x.[y z.y z x]x] [x.[z.x z x]] [x z.x z x] ≠[y z.y z x]`

Next up is the brilliant world of logical operators in lambda calculus!