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 ^{1}**

**.**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.

^{1}https://en.wikipedia.org/wiki/Lambda_calculus