Bound Variables and Lambda Calculus

This semester I’m taking Foundations of Software taught by professor Martin Odersky, the inventor of Scala. Most contents of this course are from the classic book Types and Programming Languages, of which lambda calculus and its extensions are the central topic.

I’m attracted by the simplicity and power of lambda calculus. Conceptually it’s much simpler than Turing machine, though it’s Turing-complete. Church numerals and Y-combinators are very eye-opening. However, there’s one thing I’m a little uncomfortable with lambda calculus - its syntax. The standard untyped lambda calculus syntax is as follows:

  t :: =
          t t

As we know, in lambda calculus everything is function. For example, we can represent numbers, booleans, pairs, recursion functions, etc based on lambda calculus:

tru = λt. λf. t
fls = λt. λf. f

and = λb. λc. b c fls
or = λb. λc. b tru c
not = λb. b fls tru

pair = λf.λs.λb. b f s
fst = λp. p tru
snd = λp. p fls

0 = λs. λz. z
1 = λs. λz.s z
2 = λs. λz.s (s z)
3 = λs. λz.s (s (s z))

scc= λn. λs. λz.s(n s z)
plus= λm. λn. λs. λ s z)
times = λm. λn. λs. λz. m (n s) z
power = λm. λn. n (times m m)

fix = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))
fact = fix ( λfct. λn. if iszero n then 1 else n * (fct (pred n)) )

However, the syntax above also allows a lot of free variables, which should not be taken as valid lambda calculus formulas. For example, terms like “x y” is allowed by the syntax, but it’s obvious invalid. If we simply remove “x” from the syntax definition, we’ll be unable to define abstraction(“λx. t”) in a recursive approach.

Another problem caused by variables is in evaluation. For example, to reduce the term “λx. (λy. λx. x y) x”, we can’t just replace “y” with “x” to get “λx. λx. x x”. The correct approach is first to rename the inner variable “x” to “z” then replace “y” with “x” to get “λx. λz. z x”.

Is it possible to get away all these subtleties? After some searching, I found something interesting.

The bound variables problem not only exists in lambda calculus, but also exists in classic logic(first or higher-order logic). There are several approaches to eliminate variables:

Corresponding to the idea of no bound variables, there’s a programming style called pointfree programming, in which there’s no need to explicitly specify the parameters. For example:

sum = foldr (+) 0
f = (+ 1)

Theoretically we can do away with parameters completely, as all fonctions can be composed from the basic functions. Extensive usage of point-free style in programming will make the code less readable. However, in some cases it makes the code cleaner, as illustrated by following example:

fn x = f (g (h x))
fn = f . g . h