Building with λ-calculus

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 substitution¹. 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

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.

ARITHMETIC

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.

CHURCH BOOLEANS

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.