Update: The latest version of the lambda calculator has line editing and a command history. It’s more convenient than the version linked in the blog and is tagged 0.1.0.
The world’s smallest programming language is probably the Lambda Calculus. The Lambda Calculus was invented by Alonzo Church in the 1930’s as a means of exploring computability in maths. As such, it is an analogue to the more famous Turing Machine. Alan Turing, himself, proved that the Lambda Calculus is Turing Complete, which is to say, it is as powerful as a Turing Machine and any other programming model. The Lambda Calculus is not really practical as a means of programming, but its ideas have directly influenced many programming languages, starting with LISP. Closures in modern languages are sometimes referred to as lambdas and the reason is the Lambda Calculus.
A Lambda Calculator
In order to aid this blog, I thought it might be useful to be able to run some of the examples, so I have created a simple REPL interpreter here. The version used in this blog is tagged blog-1474. It’s a Swift package, so make sure you have the Swift build system installed, clone the repository and then type
swift run. Exit the session by typing ctrl d.
When the interpreter expects input from the user, it prints
> . It prefixes its own output with
: . When you type a line of text in, it does one of two things:
- If the line contains anything other than white space, it attempts to parse it as a lambda expression and make the result its current expression.
- If the line is devoid of anything but white space, it attempts to do one β-reduction (pronounced “beta reduction”) on the current expression. More on what one of those is later.
After doing one of the above, the interpreter prints the current expression (or tells you if you have made a mistake). Here is an example of a run of the program.
jeremyp@eleanor LambdaCalculus % swift run [3/3] Linking lambdacalc > (\x.x x)(\x.x)y : (λx.x x) (λx.x) y > : (λx.x) (λx.x) y > : (λx.x) y > : y
The Lambda Calculus
The Lambda Calculus is very simple. It has two keywords: “λ” (lambda) and “.” (full stop or period). For convenience, in my lambda calculator, you can use
\ in place of λ if you don’t have a Greek keyboard.
It also uses parentheses for grouping expressions and there’s one binary operator called “application” which doesn’t have a special symbol: if you see two expressions next to each other, application is implied.
Everything else except white space is a variable. In the current incarnation of my lambda calculator, white space is used to separate variables and the end of the line signifies the end of the lambda expression. Other than that, the syntax is as follows:
|Variable||Any sequence of characters except the keywords, parentheses and white space.||A variable|
|Abstraction||λx.M where x is a variable and M is a lambda expression||An abstraction is the Lambda Calculus equivalent to a function or a closure. The variable x is said to be bound in M.|
|Application||M N where M and N are both lambda expressions||This represents an application of an abstraction to a lambda expression. It’s like a function call, but what it actually means will be discussed later. Application is the only operator in Lambda Calculus.|
|Parentheses||(M) where M is a lambda expression||Used to override the normal order of precedence.|
Here are a few example lambda expressions
|An abstraction in which the body is a sequence of applications|
|An application of the above abstraction to the variable z.|
|An application of an abstraction to another abstraction|
Application is left associative, with is to say
x y z is equivalent to
(x y) z.
By convention, the body of an abstraction (the expression) is considered to extend as far right as possible. In practice, that means until you reach an unmatched right parenthesis or the end of the line. For example
λx.a b c is the same as
λx.(a b c)
These rules are designed mainly to stop us from drowning in parentheses.
One further point: the version of the Lambda calculator tagged for this post defines a variable as a sequence of letters and numbers and the
' character with
' not allowed to appear at the start and the Greek letter λ not allowed. So
123xyz' is a variable and so is
123λxyz is not, nor is
'123abc. A lot of articles on the Lambda Calculus assume a variable is a single letter. So in an article, you might see
(λx.xy)z. In my Lambda Calculator, you’d have to write it as
(λx.x y)z to ensure that
xy is read as an application of two variables rather than a single variable named
So far, all we have done is describe what lambda expressions look like. To be a programming language, it must have some means of expressing computation. This is the subject of the next post.