Theory LambdaCalculus
chapter "The Lambda Calculus"
text ‹
In this second part of the article, we apply the residuated transition system framework
developed in the first part to the theory of reductions in Church's ‹λ›-calculus.
The underlying idea is to exhibit ‹λ›-terms as states (identities) of an RTS,
with reduction steps as non-identity transitions. We represent both states and transitions
in a unified, variable-free syntax based on de Bruijn indices.
A difficulty one faces in regarding the ‹λ›-calculus as an RTS is that
``elementary reductions'', in which just one redex is contracted, are not preserved by
residuation: an elementary reduction can have zero or more residuals along another
elementary reduction. However, ``parallel reductions'', which permit the contraction of
multiple redexes existing in a term to be contracted in a single step, are preserved
by residuation. For this reason, in our syntax each term represents a parallel reduction
of zero or more redexes; a parallel reduction of zero redexes representing an identity.
We have syntactic constructors for variables, ‹λ›-abstractions, and applications.
An additional constructor represents a ‹β›-redex that has been marked for contraction.
This is a slightly different approach that that taken by other authors
(\emph{e.g.}~\<^cite>‹"barendregt"› or \<^cite>‹"huet-residual-theory"›), in which it is the
application constructor that is marked to indicate a redex to be contracted,
but it seems more natural in the present setting in which a single syntax is used to
represent both terms and reductions.
Once the syntax has been defined, we define the residuation operation and prove
that it satisfies the conditions for a weakly extensional RTS. In this RTS, the source
of a term is obtained by ``erasing'' the markings on redexes, leaving an identity term.
The target of a term is the contractum of the parallel reduction it represents.
As the definition of residuation involves the use of substitution, a necessary prerequisite
is to develop the theory of substitution using de Bruijn indices.
In addition, various properties concerning the commutation of residuation and substitution
have to be proved. This part of the work has benefited greatly from previous work
of Huet \<^cite>‹"huet-residual-theory"›, in which the theory of residuation was formalized
in the proof assistant Coq. In particular, it was very helpful to have already available
known-correct statements of various lemmas regarding indices, substitution, and residuation.
The development of the theory culminates in the proof of L\'{e}vy's ``Cube Lemma''
\<^cite>‹"levy"›, which is the key axiom in the definition of RTS.
Once reductions in the ‹λ›-calculus have been cast as transitions of an RTS,
we are able to take advantage of generic results already proved for RTS's; in particular,
the construction of the RTS of paths, which represent reduction sequences.
Very little additional effort is required at this point to prove the Church-Rosser Theorem.
Then, after proving a series of miscellaneous lemmas about reduction paths,
we turn to the study of developments. A development of a term is a reduction path from
that term in which the only redexes that are contracted are those that are residuals of
redexes in the original term. We prove the Finite Developments Theorem: all developments
are finite. The proof given here follows that given by de Vrijer \<^cite>‹"deVrijer"›,
except that here we make the adaptations necessary for a syntax based on de Bruijn
indices, rather than the classical named-variable syntax used by de Vrijer.
Using the Finite Developments Theorem, we define a function that takes a term and constructs
a ``complete development'' of that term, which is a development in which no residuals of
original redexes remain to be contracted.
We then turn our attention to ``standard reduction paths'', which are reduction paths in
which redexes are contracted in a left-to-right order, perhaps with some skips.
After giving a definition of standard reduction paths, we define a function that takes a
term and constructs a complete development that is also standard.
Using this function as a base case, we then define a function that takes an arbitrary
parallel reduction path and transforms it into a standard reduction path that is congruent
to the given path. The algorithm used is roughly analogous to insertion sort.
We use this function to prove strong form of the Standardization Theorem: every reduction
path is congruent to a standard reduction path. As a corollary of the Standardization
Theorem, we prove the Leftmost Reduction Theorem: leftmost reduction is a normalizing
reduction strategy.
It should be noted that, in this article, we consider only the ‹λβ›-calculus.
In the early stages of this work, I made an exploratory attempt to incorporate ‹η›-reduction
as well, but after encountering some unanticipated difficulties I decided not to attempt that
extension until the ‹β›-only case had been well-developed.
›
theory LambdaCalculus
imports Main ResiduatedTransitionSystem
begin
section "Syntax"
locale lambda_calculus
begin
text ‹
The syntax of terms has constructors ‹Var› for variables, ‹Lam› for ‹λ›-abstraction,
and ‹App› for application. In addition, there is a constructor ‹Beta› which is used
to represent a ‹β›-redex that has been marked for contraction. The idea is that
a term ‹Beta t u› represents a marked version of the term ‹App (Lam t) u›.
Finally, there is a constructor ‹Nil› which is used to represent the null element
required for the residuation operation.
›