# formal rules for avoiding bound/unbound variable problems in lambda calculus

I have been interested in learning formal math formally enough so that I could write a proof assistant using some simple parsing tools, and explain to someone else with little math knowledge how to write one. Naturally, it would be a very clunky and tedious assistant, but this is the standard I have set for myself for "really understanding" a formal system.

I'd like to do this with a typed calculus, but you work with what you can get. The most formal explanations out there seem to be for the untyped lambda calculus. However, I haven't found a good formal explanation of how one detects/avoids problems with bound/unbound variables and problems with the same variable being bound in overlapping scopes. It seems like these kinds of problems should not just be avoided but somehow simply the result of an incorrect usage of the formal rules for constructing expressions. Does anyone know of a good way to understand these problems?

I asked a related question here.

-
If you don't get any satisfactory answers here, you may also try cstheory.stackexchange.com –  Adrian Petrescu Dec 3 '10 at 6:47
Good idea; thanks :) –  John Salvatier Dec 3 '10 at 16:24

There are a number of ways of dealing with free/bound variables. The simplest (and least user friendly) is de Bruijn Indices. In this system, a bound variable is named based on how "far" it is from the binder. For example:

$\lambda x. \lambda y.~ x~y$

is

$\lambda . \lambda .~ 1~0$

in de Bruijn notation. This makes substitution of closed terms straight-forward. Free variables are represented by indices "beyond" the number of binders. For example:

$\lambda x. x~a$

is

$\lambda. 0~1$

Since there is only one binder, $1$ is free (note that this is indexed from 0). For the full details, look at the wikipedia page linked above.

A great resource for this and other basic questions about lambda calculi is Benjamin Pierce's Types and Programming Languages. Very well written and readable. It's the closest we have to a "standard" Programming Languages book.

-
A great reference for $\lambda$-calculus and formal logic in general, which treats the subject highly rigorously is Sorensen and Urzyczyn's "Lectures on the Curry-Howard Isomorphism." I'm doing a little reading on the subject myself, but not enough to really answer your question.