A toy parser for recreational λ-calculus

I moved to SnowOnion Lee’s dorm during the winter break, where I saw the books he had on his shelves. I admire his abundance in reading, though he might not agree the plentiness. I decided to read more, not exclusively computer science books. That said, I still chose to start from computer science books. I have heard about λ-calculus as a computational model for long, but never got a chance to have an even recreational look at it. Today’s entry simply records the creating of the parser.

What is and why λ-calculus?

Well, despite of its section title, I’m not going to cover λ-calculus here. I read the Wikipedia article and Achim Jung’s introductory notes to get the basic idea of λ-calculus. You can, too, if you want. Here’s a newbie’s a posteriori understanding of this formalism:

Functions (composed from a finite set of function of some choice) are used to express computation, and usually can be written in some form. The objects a function operates can be vastly different, e.g., numbers, tuples, lists of numbers, string, etc. A usual approach is to encode everything as a natural number or a string to simplify the modelling, as is done in Turing’s model.

From a mathematical point of view, things we use daily are sets. Functions are special sets (special relations, which are special subsets of the Cartesian product of two sets), and operate sets. It might seem tempting to formalise the setting with sets.

However, we want to freely manipulate functions, which involves applying the function to the function itself. Without some restrictions, this is mathematically impossible (because such a function cannot be represented by a set, because a set cannot own itself, nor can it own a set that owns itself, and so on).

To avoid the problem (and since the restrictions are not easy to formulate), we write everything as formal symbols (strings) and define equivalence relations on these formal symbols (using α-conversion, β-reduction and η-conversion).

What is and why de Bruijn index?

The usual writing system is human-friendly, but managing names of variables can be a pain.

Nicolaas Govert de Bruijn invented the notation of de Bruijn index, which eliminates the need for names of bound variables, completely relieving us from α-conversion.

The idea is to have a stack in the head. Each time an abstraction is entered, we push a new bound variable onto the stack. The bound variables are represented by positive integers, which indicates the distance of the recalled variable from the top of the stack. Unbounded variables can be represented by an index-out-of-bound value.

My grammar and my parser

I further simplified the CFG for lambda terms to ease the implementation. A lambda term is a list of application terms optionally followed by an abstraction term, but is not empty. An abstraction term is ‘λ’ followed by a lambda term. An application term is either a variable, a constant (represented by some identifier) or a grouped lambda term, i.e., a lambda term with parentheses around it. Formally this means$\begin{aligned}&\Lambda\to{A^*\lambda\Lambda\mid A^{+}}\\&A\to{\mathrm{var}\mid\mathrm{const}\mid(\Lambda)}.\end{aligned}$Furthermore, we allow no unbound variables. Usually this check is done by SDT after parsing, however, my code actually does sanity checks and produces the final lambda term representation in one pass.

Lexically, lambda and . are considered ‘λ’ tokens, integers are variables, identifiers are constants, and parentheses are parentheses.

The grammar is so simple that even manually writing the parser is a piece of cake. I published the code on GitHub (the link takes you to the specific commit c104397, not always the latest master branch). I actually bothered to implement everything from scratch. (Nit-pickers’ corner: not from the very scratch.)

The file code/utils.hpp has a memory pool coupled with reference counting smart pointer for specific types, code/terms.hpp defines the structural representation of lambda terms as well as a handy CRTP template that eases employment of visitor pattern, code/parser.hpp implements the parser, and finally code/toys/parse-print.cpp does some gluing to form a demonstration.

So much for today. I might implement computation if I find time.