Basics of Binding and Free Variables

1Introduction

This lecture defines the syntax of lambda terms and classifies every variable occurrence as bound or free. A name alone does not determine the classification; the occurrence's position and the scope of its binder are essential.

2Syntax and syntax trees

Let $\text{[PARSE ERROR: Undefined("Command("mathcal")")]}V$\mathcal V be a countably infinite set of variables. The set $\mathrm{\Lambda }$\Lambda of untyped lambda terms is defined recursively by the grammar

Here $x$x is a variable, $MN$M\;N is an application, and $\lambda x.M$\lambda x.M is an abstraction. When parentheses are omitted, application associates to the left and the body of an abstraction extends as far to the right as possible. Thus $MNP=\left(MN\right)P$M\;N\;P=(M\;N)\;P and $\lambda x.MN=\lambda x.\left(MN\right)$\lambda x.M\;N=\lambda x.(M\;N).

3Binders, scopes, and occurrences

In $\lambda x.M$\lambda x.M, the prefix $\lambda x$\lambda x is a binder for $x$x, and the subterm $M$M is its scope. An occurrence of $x$x at a leaf of the syntax tree is bound if it lies inside the body of some $\lambda x$\lambda x. If several such binders enclose the occurrence, the nearest one in the syntax tree binds it. An occurrence of $x$x that lies in the scope of no $\lambda x$\lambda x is free.

Boundness is a property of an occurrence, not merely of a variable name. For example, in

the leftmost occurrence of $x$x is free, whereas the rightmost occurrence is bound by the inner $\lambda x$\lambda x. In

the occurrence in the inner body is bound by the inner binder, while the final occurrence is bound by the outer binder. This phenomenon is called shadowing.

4The set of free variables

$\mathrm{F}\mathrm{V}\left(M\right)$\mathrm{FV}(M) is the set of variable names that have at least one free occurrence in $M$M. It is defined structurally by

For example,

A term $M$M is closed if $\mathrm{F}\mathrm{V}\left(M\right)=\text{[PARSE ERROR: Undefined("Command("varnothing")")]}$\mathrm{FV}(M)=\varnothing and open otherwise. A term is closed exactly when every variable occurrence is bound by some binder.

5Check

In $M=\lambda x.\left(x\right(\lambda y.xy\left)z\right)$M=\lambda x.(x\;(\lambda y.x\;y)\;z), both occurrences of $x$x are bound by the outer $\lambda x$\lambda x, the occurrence of $y$y is bound by $\lambda y$\lambda y, and only the occurrence of $z$z is free. Hence $\mathrm{F}\mathrm{V}\left(M\right)=\left\{z\right\}$\mathrm{FV}(M)=\{z\}. The next lecture uses this occurrence-level classification to define substitution that avoids capture.

6Related links