Lambda Calculus Syntax

Definition of lambda terms

[Terms] The set of terms of the lambda calculus is defined inductively by:

1. If $x$source is a variable, then $x$source is a term.

2. If $x$source is a variable and $M$source is a term, then $(\lambd[x][M])$source is a term.

3. If both $M$source and $N$source are terms, then $(MN)$source is a term.

Exercise on formation of a nested lambda term

Describe the formation of $(\lambd[g][(\lambd[x][(g (x x))]) (\lambd[x][(g (x x))])])$source.

Lemma on the first symbol of a term

A term starts with either a variable or a parenthesis.

Proof

Something counts as a term only if it is constructed according to the definition of lambda terms. If it is the result of the variable formation clause, it must be a variable. If it is the result of the abstraction formation clause or the application formation clause, it starts with a parenthesis.

Lemma on the first symbols of an application

The result of an application starts with either two parentheses or a parenthesis and a variable.

Proof

If $M$source is the result of an application, it is of the form $(PQ)$source, so it begins with a parenthesis. Since $P$source is a term, by the lemma on the first symbol of a term, it begins either with a parenthesis or a variable.

Lemma on proper initial parts

No proper initial part of a term is itself a term.

Exercise proving the initial part lemma

Prove the lemma that no proper initial part is a term by induction on the length of terms.

Unique readability proposition

[Unique Readability] There is a unique formation for each term. In other words, if a term $M$source is formed by a formation, then it is the only formation that can form this term.

Proof

We prove this by induction on the formation of terms.

1. $M$source is of the form $x$source, where $x$source is some variable. Since the results of abstractions and applications always start with parentheses, they cannot have been used to construct $M$source; Thus, the formation of $M$source must be a single step of the definition of lambda termsthe variable formation clause.

2. $M$source is of the form $(\lambd[x][N])$source, where $x$source is some variable and $N$source is a term. It could not have been constructed according to the definition of lambda termsthe variable formation clause, because it is not a single variable. It is not the result of an application, by the lemma on the first symbols of an application. Thus $M$source can only be the result of an abstraction on $N$source. By inductive hypothesis we know that formation of $N$source is itself unique.

3. $M$source is of the form $(PQ)$source, where $P$source and $Q$source are terms. Since it starts with a parentheses, it cannot also be constructed by the definition of lambda termsthe variable formation clause. By the lemma on the first symbol of a term, $P$source cannot begin with $\lambd$source, so $(PQ)$source cannot be the result of an abstraction. Now suppose there were another way of constructing $M$source by application, e.g., it is also of the form $(P'Q')$source. Then $P$source is a proper initial segment of $P'$source (or vice versa), and this is impossible by the lemma that no proper initial part is a term. So $P$source and $Q$source are uniquely determined, and by inductive hypothesis we know that formations of $P$source and $Q$source is unique.

Three uniquely determined forms of a term

A term $M$source can only be one of the following forms:

1. $x$source, where $x$source is a variable uniquely determined by $M$source.

2. $(\lambd[x][N])$source, where $x$source is a variable and $N$source is another term, both of which is uniquely determined by $M$source.

3. $(PQ)$source, where $P$source and $Q$source are two terms uniquely determined by $M$source.

Exercise expanding abbreviated syntax

Expand the abbreviated term $\lambd[g][(\lambd[x][g (x x)]) \lambd[x][g (x x)]]$source.

Definition of scope as printed

[Scope] If $\lambd[x][M]$source occurs inside a term $N$source, then the corresponding occurrence of $N$source is the scope of the $\lambd[x]$source.

Definition of free and bound occurrence

[Free and bound occurrence] An occurrence of variable $x$source in a term $M$source is free if it is not in the scope of a $\lambd[x]$source, and bound otherwise. An occurrence of a variable $x$source in $\lambd[x][M]$source is bound by the initial $\lambd[x]$source iff the occurrence of $x$source in $M$source is free.

Examples distinguishing nested binders

In $\lambd[x][x y]$source, both $x$source and $y$source are in the scope of $\lambd[x]$source, so $x$source is bound by $\lambd[x]$source. Since $y$source is not in the scope of any $\lambd[y]$source, it is free. In $\lambd[x][x x]$source, both occurrences of $x$source are bound by $\lambd[x]$source, since both are free in $xx$source. In $((\lambd[x][xx])x)$source, the last occurrence of $x$source is free, since it is not in the scope of a $\lambd[x]$source. In $\lambd[x][(\lambd[x][x])x]$source, the scope of the first $\lambd[x]$source is $(\lambd[x][x])x$source and the scope of the second $\lambd[x]$source is the second-to-last occurrence of $x$source. In $(\lambd[x][x])x$source, the last occurrence of $x$source is free, and the second-to-last is bound. Thus, the second-to-last occurrence of $x$source in $\lambd[x][(\lambd[x][x])x]$source is bound by the second $\lambd[x]$source, and the last occurrence by the first $\lambd[x]$source.

Recursive definition of free variables

[Free variables of a term] The set of free variables of a term is defined inductively by:

1. $\FV{x} = \{x\}$source

2. $\FV{\lambd[x][N]} = \FV{N} \setminus \{x\}$source

3. $\FV{PQ} = \FV{P} \cup \FV{Q}$source

Exercises identifying scopes and free variables

1. Identify the scopes of $\lambd[g]$source and the two $\lambd[x]$source in this term: $\lambd[g][(\lambd[x][g (x x)]) \lambd[x][g (x x)]]$source.

2. In $\lambd[g][(\lambd[x][g (x x)]) \lambd[x][g (x x)]]$source, are all occurrences of variables bound? By which abstractions are they bound respectively?

3. Give $\FV{\lambd[x][(\lambd[y][(\lambd[z][x y]) z]) y]}$source

Explain

A free variable is like a reference to the outside world (the environment), and a term containing free variables can be seen as a partially specified term, since its behaviour depends on how we set up the environment. For example, in the term $\lambd[x][f x]$source, which accepts an argument $x$source and returns $f$source of that argument, the variable $f$source is free. This value of the term is dependent on the environment it is in, in particular the value of $f$source in that environment.

If we apply abstraction to this term, we get $\lambd[f][\lambd[x][f x]]$source. This term is no longer dependent on the environment variable $f$source, because it now designates a function that accepts two arguments and returns the result of applying the first to the second. Changing $f$source in the environment won't have any effect on the behavior of this term, as the term will only use whatever is passed as an argument, and not the value of $f$source in the environment.

Definition of closed term and combinator

[Closed term, combinator] A term with no free variables is called a closed term, or a combinator.

Free variable membership lemma

1. If $y \neq x$source, then $y \in \FV{\lambd[x][N]}$source iff $y \in \FV{N}$source.

2. $y \in \FV{PQ}$source iff $y \in \FV{P}$source or $y \in \FV{Q}$source.

Proof

Exercise.

Exercise proving free variable membership

Prove the free variable membership lemma.

Explain

Free variables are references to environment variables, thus it makes sense to actually use a specific value in the place of a free variable. For example, we may want to replace $f$source in $\lambd[x][f x]$source with a specific term, like the identity function $\lambd[y][y]$source. This results in $\lambd[x][(\lambd[y][y]) x]$source. The process of replacing free variables with lambda terms is called substitution.

Definition of partial substitution on terms

[Substitution] The substitution of a term $N$source for a variable $x$source in a term $M$source, $\Subst{M}{N}{x}$source, is defined inductively by:

1. $\Subst{x}{N}{x} = N$source.

2. $\Subst{y}{N}{x} = y$source if $x \neq y$source.

3. $\Subst{PQ}{N}{x} = (\Subst{P}{N}{x}) (\Subst{Q}{N}{x})$source.

4. $\Subst{(\lambd[y][P])}{N}{x} = \lambd[y][\Subst{P}{N}{x}]$source, if $x \neq y$source and $y \notin \FV{N}$source, otherwise undefined.

Explain

In the definition of partial substitutionthe substitution definition's abstraction clause, we require $x \neq y$source because we don't want to replace bound occurrences of the variable $x$source in $M$source by $N$source. For example, if we compute the substitution $\Subst{\lambd[x][x]}{y}{x}$source, the result should not be $\lambd[x][y]$source but simply $\lambd[x][x]$source.

When substituting $N$source for $x$source in $\lambd[y][P]$source, we also require that $y \notin \FV{N}$source. For example, we cannot substitute $y$source for $x$source in $\lambd[y][x]$source, i.e., $\Subst{\lambd[y][x]}{y}{x}$source, because it would result in $\lambd[y][y]$source, a term that stands for the function that accepts an argument and returns it directly. But the term $\lambd[y][x]$source stands for a function that always returns the term $x$source (or whatever $x$source refers to). So the result we actually want is a function that accepts an argument, drop it, and returns the environment variable $y$source. To do this properly, we would first have to “rename” the bound variable $y$source.

Exercises evaluating partial substitutions

What is the result of the following substitutions?

1. $\Subst{\lambd[y][x(\lambd[w][vwx])]}{(uv)}{x}$source

2. $\Subst{\lambd[y][x(\lambd[x][x])]}{(\lambd[y][xy])}{x}$source

3. $\Subst{y(\lambd[v][xv])}{(\lambd[y][vy])}{x}$source

Free variables after substitution for a variable not free

If $x \notin \FV{M}$source, then $\FV{\Subst{M}{N}{x}} = \FV{M}$source, if the left-hand side is defined.

Proof

By induction on the formation of $M$source.

1. $M$source is a variable: exercise.

2. $M$source is of the form $(PQ)$source: exercise.

3. $M$source is of the form $\lambd[y][P]$source, and since $\Subst{\lambd[y][P]}{N}{x}$source is defined, it has to be $\lambd[y][\Subst{P}{N}{x}]$source. Then $\Subst{P}{N}{x}$source has to be defined; also, $x \neq y$source and $x \notin \FV{Q}$source. Then:

   $$\FV{\Subst{\lambd[y][P]}{N}{x}} = \\ \begin{aligned} & = \FV{\lambd[y][\Subst{P}{N}{x}]} && \text{by \olref{defn:substitution-4}}\\ & = \FV{\Subst{P}{N}{x}} \setminus \{y\} && \text{by \olref[fv]{def:fv}\olref[fv]{def:fv2}}\\ & = \FV{P} \setminus \{y\} && \text{by inductive hypothesis} \\ & = \FV{\lambd[y][P]} && \text{by \olref[fv]{def:fv}\olref[fv]{def:fv2}} \end{aligned}$$source
   References in this expression: the substitution definition's abstraction clause, the definition of free variables, the free variable definition's abstraction clause, the definition of free variables, the free variable definition's abstraction clause.

Exercise completing the nonfree substitution proof

Complete the proof of the substitution theorem for a variable not free in the term.

Free variables after substitution for a free variable

If $x \in \FV{M})$source, then $\FV{\Subst{M}{N}{x}} = (\FV{M} \setminus \{x\}) \cup \FV{N}$source, provided the left hand is defined.

Proof

By induction on the formation of $M$source.

1. $M$source is a variable: exercise.

2. $M$source is of the form $PQ$source: Since $\Subst{(PQ)}{N}{y}$source is defined, it has to be $(\Subst{P}{N}{x})(\Subst{Q}{N}{x})$source with both substitution defined. Also, since $x \in \FV{PQ}$source, either $x \in \FV{P}$source or $x \in \FV{Q}$source or both. The rest is left as an exercise.

3. $M$source is of the form $\lambd[y][P]$source. Since $\Subst{\lambd[y][P]}{N}{x}$source is defined, it has to be $\lambd[y][\Subst{P}{N}{x}]$source, with $\Subst{P}{N}{x}$source defined, $x \neq y$source and $y \notin \FV{N}$source; also, since $y \in \FV{\lambd[x][P]}$source, we have $y \in \FV{P}$source too. Now:

   $$\FV{\Subst{(\lambd[y][P])}{N}{x}} = \\ \begin{aligned} & = \FV{\lambd[y][\Subst{P}{N}{x}]} \\ & = \FV{\Subst{P}{N}{x}} \setminus \{y\} \\ & = ((\FV{P} \setminus \{y\}) \cup (\FV{N} \setminus \{x\}) && \text{by inductive hypothesis} \\ & = (\FV{P} \setminus \{x, y\}) \cup \FV{N} && x \notin \FV{N} \\ & = (\FV{\lambd[y][P]} \setminus \{x\}) \cup \FV{N} \end{aligned}$$source

Exercise completing the free substitution proof

Complete the proof of the substitution theorem for a variable free in the term.

Theorem on removal of a free variable

$x \notin \FV{\Subst{M}{N}{x}}$source, if the right-hand side is defined and $x \notin \FV{N}$source.

Proof

Exercise.

Exercise proving removal of a free variable

Prove the theorem on removal of a free variable by substitution.

Theorem on inverse variable substitution

If $\Subst{M}{y}{x}$source is defined and $y \notin \FV{M}$source, then $\Subst{\Subst{M}{y}{x}}{x}{y} = M$source.

Proof

By induction on the formation of $M$source.

1. $M$source is a variable $z$source: Exercise.

2. $M$source is of the form $(PQ)$source. Then:

   $$\Subst{\Subst{(PQ)}{y}{x}}{x}{y} &=\Subst{((\Subst{P}{y}{x})(\Subst{Q}{y}{x}))}{x}{y} \\ &= (\Subst{\Subst{P}{y}{x}}{x}{y})(\Subst{\Subst{Q}{y}{x}}{x}{y}) \\ &= (PQ) \text{ by inductive hypothesis}$$source

3. $M$source is of the form $\lambd[z][N]$source. Because $\Subst{\lambd[z][N]}{y}{x}$source is defined, we know that $z \neq y$source. So:

   $$\Subst{\Subst{(\lambd[z][N])}{y}{x}}{x}{y}\\ & = \Subst{(\lambd[z][\Subst{N}{y}{x}])}{x}{y} \\ & = \lambd[z][\Subst{\Subst{N}{y}{x}}{x}{y}] \\ &= \lambd[z][N] \text{ by inductive hypothesis}$$source

Exercise completing the inverse substitution proof

Complete the proof of the inverse substitution theorem.

Local definition of change of bound variable

[Change of bound variable, $\aconvone$source] If a term $M$source contains an occurrence of $\lambd[x][N]$source, $y \notin \FV{N}$source, and $\Subst{N}{y}{x}$source is defined, then replacing this occurrence by

resulting in $M'$source is called a change of bound variable, written as $M \redone[\alpha] M'$source.

Definition of compatible relation

[Compatibility of relation] A relation $R$source on terms is said to be compatible if it satisfies following conditions:

1. If $R N N'$source then $R \lambd[x][N] \lambd[x][N']$source

2. If $R P P'$source then $R (PQ) (P'Q)$source

3. If $R Q Q'$source then $R (PQ) (PQ')$source

Compatible closure definition of bound variable change

[Change of bound variable, $\aconvone$source] Change of bound variable ($\redone[\alpha]$source) is the smallest compatible relation on terms satisfying following condition:

Inductive definition of one alpha change

[Change of bound variable, $\aconvone$source] Change of bound variable ($\aconvone$source) is inductively defined as follows:

1. If $N \aconvone N'$source then $\lambd[x][N] \aconvone \lambd[x][N']$source

2. If $P \aconvone P'$source then $(PQ) \aconvone (P'Q)$source

3. If $Q \aconvone Q'$source then $(PQ) \aconvone (PQ')$source

4. If $x \neq y$source, $y \notin \FV{N}$source and $\Subst{N}{y}{x}$source is defined, then $\lambd[x][N] \redone[\alpha] \lambd[y][\Subst{N}{y}{x}]$source.

Reflexive transitive closure definition of alpha conversion

[$\alpha$source-conversion, $\aconv$source] $\alpha$source-conversion ($\aconv$source) is the smallest reflexitive and transitive relation on terms containing $\aconvone$source.

Inductive definition of alpha conversion

[$\alpha$source-conversion, $\aconv$source] $\alpha$source-conversion ($\aconv$source) is inductively defined as follows:

1. If $P \aconv Q$source and $Q \aconv R$source, then $P \aconv R$source.

2. If $P \aconvone Q$source, then $P \aconv Q$source.

3. $P \aconv P$source.

Examples of alpha conversion and free names

$\lambd[x][f x]$source $\alpha$source-converts to $\lambd[y][f y]$source, and conversely. Informally speaking, they are both functions that accept an argument and return $f$source of that argument, refering to the environment variable $f$source.

$\lambd[x][f x]$source does not $\alpha$source-convert to $\lambd[x][g x]$source. Informally speaking, they refer to the environment variables $f$source and $g$source respectively, and this makes them different functions: they behave differently in environments where $f$source and $g$source are different.

Exercise deciding alpha convertibility

Are the following pairs of terms $\alpha$source-convertible?

1. $\lambd[x][\lambd[y][x]]$source and $\lambd[y][\lambd[x][y]]$source

2. $\lambd[x][\lambd[y][x]]$source and $\lambd[c][\lambd[b][a]]$source

3. $\lambd[x][\lambd[y][x]]$source and $\lambd[c][\lambd[b][a]]$source

Lemma that one alpha change preserves free variables

If $P \aconvone Q$source then $\FV{P} = \FV{Q}$source.

Proof

By induction on the derivation of $P \aconvone Q$source.

1. If the last rule is the bound variable renaming clause, then $P$source is of the form $\lambd[x][N]$source and $Q$source of the form $\lambd[y][\Subst{N}{y}{x}]$source, with $x \neq y$source, $y \notin \FV{N}$source and $\Subst{N}{y}{x}$source defined. We distinguish cases according to whether $x \in \FV{N}$source:

   1. If $x \in FV(N)$source, then:

      $$\FV{\lambd[y][\Subst{N}{y}{x}]} &= \FV{\Subst{N}{y}{x}} \setminus \{y\} \\ & = ((\FV{N} \setminus \{x\}) \cup \{y\}) \setminus \{y\} && \text{ by \olref[sub]{thm:infv}} \\ & = \FV{N} \setminus \{x\} \\ & = \FV{\lambd[x][N]}$$source
      References in this expression: the substitution theorem for a variable free in the term.

   2. If $x \notin FV(N)$source, then:

      $$\FV{\lambd[y][\Subst{N}{y}{x}]} & = FV{\Subst{N}{y}{x}} \setminus \{y\} \\ & = \FV{N} \setminus \{x\} && \text{by \olref[sub]{thm:notinfv}} \\ & = \FV{\lambd[x][N]}.$$source
      References in this expression: the substitution theorem for a variable not free in the term.

2. The other three cases are left as exercises.

Exercise completing preservation of free variables

Complete the proof of the lemma that one alpha change preserves free variables.

Lemma reversing one alpha change

If $P \aconvone Q$source then $Q \aconvone P$source.

Proof

Induction on the derivation of $P \aconvone Q$source.

1. If the last rule is the bound variable renaming clause, then $P$source is of the form $\lambd[x][N]$source and $Q$source of the form $\lambd[y][\Subst{N}{y}{x}]$source, where $x \neq y$source, $y \notin \FV{N}$source and $\Subst{N}{y}{x}$source defined. First, we have $y \notin \FV{\Subst{N}{y}{x}}$source by the theorem on removal of a free variable by substitution. By the inverse substitution theorem we have that $\Subst{\Subst{N}{y}{x}}{x}{y}$source is not only defined, but also equal to $N$source. Then by the bound variable renaming clause, we have $\lambd[y][\Subst{N}{y}{x}] \aconvone \lambd[x][\Subst{\Subst{N}{y}{x}}{x}{y}] = \lambd[x][N]$source.

Exercise completing reversibility of alpha change

Complete the proof of the lemma reversing one change of bound variable

Theorem that alpha conversion is an equivalence relation

$\alpha$source-Conversion is an equivalence relation on terms, i.e., it is reflexive, symmetric, and transitive.

Proof

1. For each term $M$source, $M$source can be changed to $M$source by zero changes of bound variables.

2. If $P$source is $\alpha$source-converts to $Q$source by a series of changes of bound variables, then from $Q$source we can just inverse these changes (by the lemma reversing one change of bound variable) in opposite order to obtain $P$source.

3. If $P$source $\alpha$source-converts to $Q$source by a series of changes of bound variables, and $Q$source to $R$source by another series, then we can change $P$source to $R$source by first applying the first series and then the second series.

Alpha equivalence preserves free variables

If $M \aeq N$source, then $\FV{M} = \FV{N}$source.

Proof

Immediate from the lemma that one alpha change preserves free variables.

Lemma on an alpha equivalent replacement term

If $R \aeq R'$source and $\Subst{M}{R}{y}$source is defined, then $\Subst{M}{R'}{y}$source is defined and $\alpha$source-equivalent to $\Subst{M}{R}{y}$source.

Proof

Exercise.

Exercise on an alpha equivalent replacement term

Prove the substitution lemma for alpha equivalent replacement terms.

Theorem making substitution defined by alpha conversion

For any $M$source, $R$source, and $y$source, there exists $M'$source such that $M \aeq M'$source and $\Subst{M'}{R}{y}$source is defined. Moreover, if there is another pair $M'' \aeq M$source and $R''$source where $\Subst{M''}{R''}{y}$source is defined and $R'' \aeq R$source, then $\Subst{M'}{R}{y} \aeq \Subst{M''}{R''}{y}$source.

Proof

By induction on the formation of $M$source:

1. $M$source is a variable $z$source: Exercise.

2. Suppose $M$source is of the form $\lambd[x][N]$source. Select a variable $z$source other than $x$source and $y$source and such that $z \notin \FV{N}$source and $z \notin \FV{R}$source. By inductive hypothesis, we there is $N'$source such that $N' \aeq N$source and $\Subst{N'}{z}{x}$source is defined. Then $\lambd[x][N] \aeq \lambd[x][N']$source too, by the inductive definition of one change of bound variableits abstraction compatibility clause. Now $\lambd[x][N'] \aeq \lambd[z][\Subst{N'}{z}{x}]$source by the inductive definition of one change of bound variablethe bound variable renaming clause. We can do this because $z \ne x$source, $z \notin FV(N')$source and $\Subst{N'}{z}{x}$source is defined. Finally, $\Subst{\lambd[z][\Subst{N'}{z}{x}]}{R}{y}$source is defined, because $z \neq y$source and $z \notin FV(R)$source.

   Moreover, if there is another $N''$source and $R''$source satisfying the same conditions,

   $$\Subst{(\lambd[z][\Subst{N''}{z}{x}])}{R''}{y} =\\ \begin{aligned} &= \lambd[z][\Subst{\Subst{N''}{z}{x}}{R''}{y}] \\ &= \lambd[z][\Subst{\Subst{N''}{z}{x}}{R}{y}] && \text{by \olref{lem:sub:R}}\\ &=\lambd[z][\Subst{\Subst{N'}{z}{x}}{R}{y}] && \text{by inductive hypothesis}\\ &=\Subst{(\lambd[z][\Subst{N'}{z}{x}])}{R}{y} \end{aligned}$$source
   References in this expression: the substitution lemma for alpha equivalent replacement terms.

3. $M$source is of the form $(PQ)$source: Exercise.

Exercise completing alpha representative substitution

Complete the proof of the theorem choosing alpha equivalent representatives for defined substitution.

Printed corollary on pairs of representatives

For any $M$source, $R$source, and $y$source, there exists a pair of $M'$source and $R'$source such that $M' \aeq M$source, $R \aeq R'$source and $\Subst{M'}{R'}{y}$source is defined. Moreover, if there is another pair $M'' \aeq M$source and $R''$source with $\Subst{M'}{R'}{y}$source defined, then $\Subst{M'}{R'}{y} \aeq \Subst{M''}{R''}{y}$source.

Proof

Immediate from the theorem choosing alpha equivalent representatives for defined substitution.

Definition of de Bruijn terms

De Bruijn terms are inductively defines as follows:

1. $n$source, where $n$source is any natural number.

2. $PQ$source, where $P$source and $Q$source are both De Bruijn terms.

3. $\lambd[][N]$source, where $N$source is a De Bruijn term.

Translation from named terms to de Bruijn terms

where $\Gamma$source is a list of variables indexed from zero, and $\Gamma(x)$source denotes the position of the variable $x$source in $\Gamma$source. For example, if $\Gamma$source is $x,y,z$source, then $\Gamma(x)$source is $0$source and $\Gamma(z)$source is $2$source.

$x,\Gamma$source denotes the list resulted from pushing $x$source to the head of $\Gamma$source; for instance, continuing the $\Gamma$source in last example, $w,\Gamma$source is $w,x,y,z$source.