-
Notifications
You must be signed in to change notification settings - Fork 5
Introduction to Lambda Calculus
Welcome! This article tries to be an introduction to Lambda Calculus. Lambda Calculus is a functional, esoteric language based directly upon The Untyped Lambda Calculus, with a convenient syntax system. This introduction will explain what The Lambda Calculus is, how its syntax works, and how it can be used to create programs - including some simple examples.
Imagine you were trying to design a language. You want it to be as simple as possible, while still Turing Complete. You start with a fairly standard untyped language, and begin to remove all the features you do not need. Eventually you realise that you have managed to remove everything, except for anonymous functions, and what you are left with is still turing complete!
What you have just created, is The Lambda Calculus. It is a system consisting of only anonymous functions, which is still able to compute anything that a "normal" language can (as will be seen in some examples later). Of course the challenge, and enjoyment, lies in figuring out how.
Here are the things you can do in Lambda Calculus:
Functions in lambda calculus always take exactly one input, and return one ouput. You define them like this:
\ input . body
input is the name of the single input variable, and body will be some lambda calculus term to be evaluated and returned.
It is very common to create a function which immediately returns another function, for example \ a . \ b . a. For convenience, in Lambda Calculus you can contract these kinds of functions into a single declaration, like this: \ a b . a. These contracted declarations can have as many inputs as needed, but keep in mind that they are actually a series of single input functions.
To call a function with a value, merely leave a space between the function and its argument. For example:
func arg
Multiple arguments can be chained in this way, like func arg1 arg2 arg2 and so on, and function application is left associative, meaning that the same thing could be written with brackets like this: ((func arg1) arg2) arg3.
While not quite pure Lambda Calculus, named terms are used in Lambda Calculus language in order to reference specific definitions either internally, or from Javascript scripts which compile it. Defining named terms can only be done at the top level (ie. no defined terms inside other defined terms), and looks something like this:
name = term
Depending on the Purity settings of the compiler, the names defined can be used in different places.
-
PureLC: defined terms cannot be used anywhere, and are just for the Javascript to access. -
Let: defined terms can be used in the definitions of any later terms. -
LetRec: defined terms can be used in the definitions of any later terms and can be used in their own definitions (recursion).
Finally, you may define a term across multiple lines if you wish, as long as all subsequent lines start with some indent. So:
example = func
arg1
arg2
is valid, but
example = func
arg1
arg2
is not.
Another feature added for convenience to Lambda Calculus language, is the use of literal numbers (eg. 8, 99). The meaning of these numbers will depend on the encoding (explained below) of numbers, but essentially a number is just a shorthand way to write the equivalent encoded lambda term. For example, if the number encoding is set to Church, then:
inc = add 1
is exactly equivalent to:
inc = add \ f x . f x
Now that you know how to write code in Lambda Calculus, you are probably wondering how it is possible to actually do anything, considering that we only have functions to work with? The secret lies in encodings.
An encoding is some construct of functions, which we can arbitrarily choose to treat as a specific data type.
As a classic example, consider the following encoding - Church Booleans:
True = \ t f . t
False = \ t f . f
Very simply, both booleans accept two values, and they are differentiated by True returning the first value, and False returning the second value. Both boolean types take the same number of inputs, so we can use them both in the same places, and use their differences in behaviour to affect things.
Note that we could just as easily swap the definitions of True and False (which happens to be called Scott Booleans), or even use some entirely different encoding. What is important is that we remember what encodings we are using, because all our other functions we build will be based around them.
There are encodings for Booleans, Integers, Lists, Strings and on and on. And of course, you are also welcome (and encouraged!) to try and invent your own encodings, which work with a variety of functions.
Once you have sorted out all the encodings you are going to use, it then comes time to construct the functions which will use those encodings, and actually perform the computation that you want.
It can be very helpful, when designing functions, to properly keep track of the type signatures. The type signature of a function is the types which are expected as inputs, as well as the type of the output. For example, a function add might have the following type signature (using Haskell style type notation):
add :: Number -> Number -> Number
That is to say, add will accept two arguments which should be Numbers, and then the result will also be a Number. Keeping proper track of this makes it much easier to spot mistakes, and to find places where an input might not match properly with what the function expects. I would highly recommend writing down your functions type signatures using comments write above the function definitions.
Sometimes it is easier to understand by looking at code. Below I will write out an example project, in pieces with commentary on what is happening. I will also post the full code below if you would rather skip straight to there.
The plan is to implement the functions all and any, both with the type signature List Boolean -> Boolean. That is, all will accept a list of booleans, and return True if all elements are True. any will be similar, however return True if any elements are True.
Note that for this code, I will assume no numEncoding (we don't need it), and LetRec purity, for convenience.
# Church Booleans
True = \ t f . t
False = \ t f . f
This is just the boolean encoding from earlier.
# and :: Boolean -> Boolean -> Boolean
and = \ a b . a b False
# or :: Boolean -> Boolean -> Boolean
or = \ a b . a True b
Here we have two functions and their type signatures. They both accept two Boolean inputs and return another Boolean. and will return False if its first argument is False, otherwise will simply return the second argument. or is implemented similarly.
# Pairs
Pair = \ left right . \ chooser . chooser left right
This is the Pair data type. It is essentially a Tuple of two elements. In our encoding, this means that we accept two values, and then we accept a chooser function which will return either left or right (notice that our booleans are perfect for this).
Another thing to notice here, is the contracted argument list was specifically broken into two parts, \ left right . and \ chooser .. This does not change the behaviour at all, it is just to make it clearer that our 'constructor' for Pair takes two arguments, and the result is a function which accepts chooser.
# first :: Pair a b -> a
first = \ p . p True
# second :: Pair a b -> b
second = \ p . p False
Here we define accessors for our Pair, by using booleans as the chooser function for whatever pair gets inputted.
# Lists
Nil = Pair False ()
Cons = \ x xs . Pair True (Pair x xs)
Our final encoding type is for lists. Conceptually it is fairly simply, we have an initial Pair, which has a Boolean as the left value. This boolean tells us if the list is empty or not (notice that Nil uses False, and Cons uses True). Then the second element of our pair, is another pair which contains the current value, and the rest of the list. Since Nil (an empty list) does not have any more list following, we simply use () which means an undefined value. This is acceptable, as long as we never try to access it in our functions.
# is-not-empty :: List a -> Boolean
is-not-empty = \ xs . first xs
# head :: List a -> a
head = \ xs . first (second xs)
# tail :: List a -> List a
tail = \ xs . second (second xs)
Some functions which work on lists. is-not-empty will be an important tool, to make sure that we do not try to get the tail of an empty list, for example.
# all :: List Boolean -> Boolean
all = \ xs . is-not-empty xs
( and (head xs) (all (tail xs) ) ) # If not empty
( True ) # If empty
# any :: List Boolean -> Boolean
any = \ xs . is-not-empty xs
( or (head xs) (any (tail xs) ) ) # If not empty
( False ) # If empty
Finally we have the two final functions we wanted. Both are quite similar, and first check if our input list is empty, and if not then does a recursive call for the rest of the list.
And voile! We have managed to create some basic logical functions, using nothing but anonymous functions! Of course, this was a fairly simple example, but I hope it could provide some insight into how larger projects could also be approached. Before I leave the full code below, I would strongly encourage checking out some other articles on the documentation wiki.
Good luck solving in Lambda Calculus!
This code is the same as above, but all together in one code block, for easier reading/copying
# Church Booleans
True = \ t f . t
False = \ t f . f
# and :: Boolean -> Boolean -> Boolean
and = \ a b . a b False
# or :: Boolean -> Boolean -> Boolean
or = \ a b . a True b
# Pairs
Pair = \ left right . \ chooser . chooser left right
# first :: Pair a b -> a
first = \ p . p True
# second :: Pair a b -> b
second = \ p . p False
# Lists
Nil = Pair False ()
Cons = \ x xs . Pair True (Pair x xs)
# is-not-empty :: List a -> Boolean
is-not-empty = \ xs . first xs
# head :: List a -> a
head = \ xs . first (second xs)
# tail :: List a -> List a
tail = \ xs . second (second xs)
# all :: List Boolean -> Boolean
all = \ xs . is-not-empty xs
( and (head xs) (all (tail xs) ) ) # If not empty
( True ) # If empty
# any :: List Boolean -> Boolean
any = \ xs . is-not-empty xs
( or (head xs) (any (tail xs) ) ) # If not empty
( False ) # If empty