(* Title: LambdaCalculus Author: Eugene W. Stark <stark@cs.stonybrook.edu>, 2022 Maintainer: Eugene W. Stark <stark@cs.stonybrook.edu> *) 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. ›