We present a new and formal coinductive proof of confluence and normalisation of B "ohm reduction in infinitary lambda calculus. The proof is simpler than previous proofs of this result. The technique of the proof is new, i.e., it is not merely a coinductive reformulation of any earlier proofs. We formalised the proof in the Coq proof assistant.
Infinitary lambda calculus was introduced in @cite_12 @cite_4 . Meaningless terms were defined in @cite_22 . The confluence and normalisation results of this paper were already obtained in @cite_12 @cite_22 , by a different proof method. See also @cite_39 @cite_36 @cite_18 for an overview of various results in infinitary lambda calculus and infinitary rewriting.
@cite_18 @cite_4 @cite_22 @cite_36 @cite_39 @cite_12
2078043326 1492737256 1541163474 1970779642 2403774400 1968168625
We present some highlights from the emerging theory of infinitary rewriting, both for first-order term rewriting systems and @l-calculus. In the first section we introduce the framework of infinitary rewriting for first-order rewrite systems, so without bound variables. We present a recent observation concerning the continuity of infinitary rewriting. In the second section we present an excursion to the infinitary @l-calculus. After the main definitions, we mention a recent observation about infinite looping @l-terms, that is, terms that reduce in one step to themselves. Next we describe the fundamental trichotomy in the semantics of @l-calculus: Bohm trees, Levy-Longo trees, and Berarducci trees. We conclude with a short description of a new refinement of Bohm tree semantics, called clocked semantics. In a previous paper we have established the theory of transfinite reduction for orthogonal term rewriting systems. In this paper we perform the same task for the lambda calculus. This results in several new Bohm-like models of the lambda calculus, and new descriptions of existing models. We present an introduction to infinitary lambda calculus, highlighting its main properties. Subsequently we give three applications of infinitary lambda calculus. The first addresses the non-definability of Surjective Pairing, which was shown by the first author not to be definable in lambda calculus. We show how this result follows easily as an application of Berry's Sequentiality Theorem, which itself can be proved in the setting of infinitary lambda calculus. The second pertains to the notion of relative recursiveness of number-theoretic functions. The third application concerns an explanation of counterexamples to confluence of lambda calculus extended with non-left-linear reduction rules: Adding non-left-linear reduction rules such as @dxx->x or the reduction rules for Surjective Pairing to the lambda calculus yields non-confluence, as proved by the second author. We discuss how an extension to the infinitary lambda calculus, where Bohm trees can be directly manipulated as infinite terms, yields a more simple and intuitive explanation of the correctness of these Church-Rosser counterexamples. We provide a coinductive definition of strongly convergent reductions between infinite lambda terms. This approach avoids the notions of ordinals and metric convergence which have appeared in the earlier definitions of the concept. As an illustration, we prove the existence part of the infinitary standardization theorem. The proof is fully formalized in Coq using coinductive types. The paper concludes with a characterization of infinite lambda terms which reduce to themselves in a single beta step. In a previous paper we have established the theory of transfinite reduction for orthogonal term rewriting systems. In this paper we perform the same task for the lambda calculus. From the viewpoint of infinitary rewriting, the Bohm model of the lambda calculus can be seen as an infinitary term model. In contrast to term rewriting, there are several different possible notions of infinite term, which give rise to different Bohm-like models, which embody different notions of lazy or eager computation.