Lambda Calculus

Today's project: implementing lambda calculus. It looks fairly straightforward, but I'm sure we'll hit some snags along the way. First step: definitions.

Expressions

A λ-calculus expression is like math; it's made up of smaller pieces like variables (such as x) and operations (such as +). Here are all the valid classes of expressions:

  • A variable (such as x) is a valid expression. For simplicity, I'll use just single-letter variables for today's test.
  • A function is a valid expression. Functions map a single input variable to some output expression. I like the notation x→y.A
  • Applying one expression (presumably a function) to another is a valid expression. Let's use the notation f:x. This is right-associative (because I say so), so f:g:x is f:(g:x), not (f:g):x.
  • Parentheses around an expression are a valid expression.

That's it. There are no other valid terms, not even numbers. I'm somewhat familiar with Church numbers, but we'll deal with those once we have something working here.

Before I go any further, this is probably the time to throw a quick parser together. I'm thinking I'll use a tree of some sort to store expressions once they've been parsed.

Making a Parser

I'm using C# to write this. First, a few utility bits – I'll be writing λ-calculus expressions in a separate text file, so a simple function to read in a .lambda file is needed. I should probably strip out any spaces and the like, since it'll be helpful to have those in the code. It'd be nice to be able to add comments, so I might as well strip out comments. Let's use //-to-end-of-line comments because that'll be easy to type and easy to strip out.B

Now it's time to get to the meat of the parser. There are only two operators ( and :), parentheses, and single-letter variables. I'm thinking I should start by splitting the string of code up into tokens, then have operators grab their arguments in little trees, clumping up until they've formed one single tree for the whole expression (or failed because the code wasn't well-formed). That's the approach I've taken to parsing stuff like this in the past, but maybe there's a better way to do this.

One idea is to not do anything more on the parsing side and just let the operators work on the raw text of the code. This doesn't seem like a good idea – I don't want to have to fiddle with parentheses and grouping any more than I have to. Let's look at some random valid code for a second:

x→y→x

Now it occurs to me that the operator needs to have a defined associativity. Let's go with right-associativity so it matches the : operator.

While I'm part way into the parser, it seems that I should take a moment to play around with λ-calculus on paper first.

Church Numbers

It all starts with the identity function:

x→x

Applying this function to any x results in x, no change at all. (getting started...)

0 = f→x→x
1 = f→x→(f:x)

Are these reversible in description?

0 ?= x→f→x
1 ?= x→f→f:x
2 ?= x→f→f:f:x