Chapter 2: Data Abstraction

Since lambda calculus is a programming language, the machinery to encode data structures is necessary.

Another core idea about lambda calculus is that everything is function. Don't be surprised, just continue and see.

Booleans and If Function

Let's start with simplest ones - booleans. true is defined as a function that selects its first parameter and false selects its second one.

$$T=\lambda xy.x\\ F=\lambda xy.y$$

Owing to the selection design of booleans, it is natural to implement if function like this:

$$\text{if}=\lambda cxy.cxy$$

You may verify following expressions:

$$\text{if }Tab=a\\ \text{if }Fab=b$$

But as you apply $\eta$ reduction to if function, you will find out it is entirely redundant, since booleans are already selector themselves.

$$\text{if }cxy=(\lambda cxy.cxy)cxy=cxy$$

Logic Functions

Making good use of selection semantics contributes to the establishment of fundamental logic functions.

$$\text{not}=\lambda x.xFT\\ \text{and}=\lambda xy.xyF\\ \text{or}=\lambda xy.xTy$$

You may combine basic logic functions above and perform certain reductions to obtain more, or directly construct one according to your innermost intuition.

$$\text{xor}=\lambda xy.x(yFT)(yTF)=\lambda xy.x(\text{not } y)y=\lambda xy.(x\text{ not }I)y$$

Ordered Pairs

Mathematicians love ordered pairs. They may be the infrastructure of all data structures. For example, tuples are often defined as recursive ordered pairs. Ordered pairs in lambda calculus are defined as follows:

$$\text{cons}=\pi=\lambda ab.\lambda z.zab\\ \text{car}=\pi_1=\lambda p.pT\\ \text{cdr}=\pi_2=\lambda p.pF$$

$\pi$ constructs an ordered pair, $\pi_1$ and $\pi_2$ retrieve the first and second element of the ordered pair respectively.

Note: symbol $\pi$ is homophonic with "pair" and alphabetic names originated from Lisp.

Unlike previous functions, I didn't uncurry all parameters because the element selector $z$ seldom comes together with the pair elements. With delayed accessors, it creates a semantics as if the elements are "stored" in the function returned by $\pi$.

$$p:=\pi ab\\ \pi_1p=a\\ \pi_2p=b$$

Triples

As long as oredered pairs are ready, other abstract data types could be implemented. For example, a triple may be defined as:

$$\tau=\lambda abc.\pi a(\pi bc)\\ \tau_1=\pi_1\\ \tau_2=\lambda t.\pi_1(\pi_2t)\\ \tau_3=\lambda t.\pi_2(\pi_2t)\\$$

Note: symbol $\tau$ is homophonic with "triple"

Tuples of arbitrary length could be implemented in the same approach.

Linear Lists

Tuples are not enough, an extensible linear list is expected. So there is.

$$\text{push-front}=\lambda la.\pi al\\ \text{pop-front}=\pi_2\\ \text{get-front}=\pi_1$$

Unlike tuples, the second element of last pair of a list should not store a regular value but a special object that indicates the end of the list. It must be intrinsic and unable to be implemented via lambda calculus to avoid potential conflicts with other regular logics. Let's call the indicator $\text{nil}$. The predicate to test if an object is $\text{nil}$ is $\text{is-nil}$.

$$\text{is-nil }\text{nil}=T\\ \text{is-nil }\textit{otherwise}=F$$

Then a prepending singly linked list is done!

$$l:=\text{nil}\\ l:=\text{push-front }l3\\ l:=\text{push-front }l2\\ l:=\text{push-front }l1$$

Now $l$ is $(1, (2, (3, \text{nil})))$, or just $(1, 2, 3)$ for short.

Recursive definition of lists provokes recursive algorithm. But recursion will not be discussed until Chapter 5. At the same time you will see the functionality of $\text{nil}$.

Linear data structures are merely pieces of cake if you keep exploring.

Trees

What about trees?

Remember triples? It's high time to reuse it to build a binary tree.

$$\text{cons-node}=\tau\\ \text{node-data}=\tau_1\\ \text{left-child}=\tau_2\\ \text{right-child}=\tau_3$$

Did I define anything new? Yes and no. Yes semantically, no underlyingly. That's why we call them abstract data types. Abstraction rocks!

Data Abstraction

In fact, by defining appropriate accessor functions, any abstract data type is available from ordered pairs. Differences are no more than how pairs are organized and how pairs are manipulated. Underlying representation of pairs remains unchanged.

See Structure and Interpretation of Computer Programs for more about data abstraction.