For those not yet initiated in λ-calculus, the first questions are usually the four Ws: What, Who, When, and Why. Created by Alonzo Church in the 1930s (a decade that had other notable inventions like Monopoly, nylon, frozen foods, polarizing glass and the Zippo lighter), λ-calculus is defined as a formal system for expressing computation based on function abstraction and application using variable binding and substitution1. That is a fancy way of saying that the purpose of λ-calculus is to define a common framework of understanding on which research of computation as a concept can be done.
Why learn it or, in this case, explain it to the reader? Understanding λ-calculus provides a deeper understanding of what computation (and computer science) is, and foments an increased appreciation of high-level programming languages.
Where does λ-calculus fit?
Recall that λ-calculus focuses on the concept of computation. It provides a baseline to answer the question of what does it mean to compute. Λ-calculus is not formal language research (though we are sure someone with a lot of creativity has found a way to leverage it) or esoteric language research (the syntax of λ-calculus might be initially off putting, but it was not built with that purpose). If we were to place λ-calculus in a poorly scaled longcat in relation to other programming languages, it would look something like this:
THE FUNDAMENTALS OF Λ-CALCULUS
The fundamentals of λ-calculus are straightforward:
- Functions are single input (allowing the study of functions in simpler theoretical models)
- Functions are anonymous
In order to ‘create’ a multi-input function, currying is needed. Currying is the technique to convert a multi-input function into a series of single-input functions.
Consider the below example in pseudo-code, comparing Python to λ-calculus:
# Python definition def sq_sum(x, y): return ((x^2)+(y^2)) # Python execution retval = sq_sum(2,5) # λ-calculus definition x -> (y -> x^2 + y^2) # λ-calculus execution (x -> (y -> x^2 + y^2) (5)) (2)
The other fundamental concepts to know about λ-calculus are the term syntax and reduction operations. Term syntax are pretty straightforward to understand:
Reduction operations come in three flavors:
- α-conversion: changing bound variables (aka renaming variables)
- β-reduction: applying functions to their arguments (aka executing a function)
- η-reduction (eta reduction, not n-reduction): captures extensionality (local completeness, aka. two functions are the same)
THE BASICS OF Λ-CALCULUS
Now that we understand the fundamentals, we can dive into the basics of λ-calculus: Church Numerals (numbers), arithmetic, and boolean algebra.
Church Numerals are higher order functions. That is, a Church numeral n (for example, 9) is a function that takes a function f as argument and returns the n-th (in our example, 9th) composition of f.
We can define traditional numbers using Church Numerals like so:
0 := λf.λx.x 1 := λf.λx.f x 2 := λf.λx.f (f x) 3 := λf.λx.f (f (f x))
In our example of 9, it would look like:
9 := λf.λx.f (f (f (f (f (f (f (f (f x))))))))
Now we can write numbers that were first introduced in 700 AD using λ-calculus.
The trusted arithmetic operators we are all familiar with, like addition, subtraction, multiplication, etc. can be defined as functions using lambda calculus:
SUCC := λn.λf.λx.f (n f x) PLUS := λm.λn.λf.λx.m f (n f x) MULT := λm.λn.λf.m (n f) POW := λb.λe.e b PRED := λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u) SUB := λm.λn.n PRED m
At this point we can celebrate, because we can perform arithmetic operations that were first seen in 18,000 BC using λ-calculus.
Booleans, the data types that allow us to represent true/false values and conditional operators (e.g. AND/OR/NOT/IFTHENELSE) can also be defined using λ-calculus:
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 IFTHENELSE := λp.λa.λb.p a b
And more importantly, we can also do other predicate operations (operations that result in a Boolean value) like checking if an input is zero, less than or equal, etc.:
ISZERO := λn.n (λx.FALSE) TRUE LEQ := λm.λn.ISZERO (SUB m n) PRED := λn.n (λg.λk.ISZERO (g 1) k (PLUS (g k) 1)) (λv.0) 0
WHAT TO DO WITH ALL THIS KNOWLEDGE?
At Cynnovative we like to challenge ourselves with every new piece of knowledge we obtain. For a recent presentation of this λ-calculus material, we asked attendees to build a program (function definitions and β-reduction) in λ-calculus that:
- Counts from 0 to 100,
- Prints out the message “Hello, World” in binary,
- Builds a linked list of 1,000,000 elements, and
- Sends a GET request to https://cynnovative.com and verifies the SSL certificate validity, printing out its expiration date.
No constraints: everyone could get as creative as they wanted. In a future post, we will go over some of the answers and analyze how they work.