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.
Joachimski in @cite_14 gives a coinductive confluence proof for infinitary lambda calculus, but Joachimski's notion of reduction does not correspond to the standard notion of a strongly convergent reduction. Essentially, it allows for infinitely many parallel contractions in one step, but only finitely many reduction steps. The coinductive definition of infinitary reductions capturing strongly convergent reductions was introduced in @cite_8 . Later @cite_10 @cite_32 generalised this to infinitary term rewriting systems. @cite_16 using the definition from @cite_8 , confluence of infinitary lambda calculus modulo equivalence of root-active subterms was shown coinductively. The proof in @cite_16 follows the general strategy of @cite_12 @cite_4 . The proof in the present paper bears some similarity to the proof of the unique normal forms property of orthogonal iTRSs in @cite_25 . It is also similar to the coinductive confluence proof for nearly orthogonal infinitary term rewriting systems in @cite_20 , but there the standard'' reduction employed is not unique and need not be normalising.
@cite_14 @cite_4 @cite_8 @cite_20 @cite_32 @cite_16 @cite_10 @cite_25 @cite_12
2057918084 1492737256 2316213087 2621204639 1837997878 1968168625
The coinductive λ-calculus Aco arises by a coinductive interpretation of the grammar of the standard λ-calculus A and contains non-well-founded λ-terms. An appropriate notion of reduction is analyzed and proven to be confluent by means of a detailed analysis of the usual Tait Martin-Lof style development argument. This yields bounds for the lengths of those joining reduction sequences that are guaranteed to exist by confluence. These bounds also apply to the well-founded λ-calculus, thus adding quantitative information to the classic result. 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 give a relatively simple coinductive proof of confluence, modulo equivalence of root-active terms, of nearly orthogonal infinitary term rewriting systems. Nearly orthogonal systems allow certain root overlaps, but no non-root overlaps. Using a slightly more complicated method we also show confluence modulo equivalence of hypercollapsing terms. The condition we impose on root overlaps is similar to the condition used by Toyama in the context of finitary rewriting. We present a coinductive framework for defining and reasoning about the infinitary analogues of equational logic and term rewriting in a uniform way. We define Equation found, the infinitary extension of a given equational theory =R, and →∞, the standard notion of infinitary rewriting associated to a reduction relation →R, as follows: (Formula Presented) Equation found Here μ and ν are the least and greatest fixed-point operators, respectively, and (Formula Presented) Equation found The setup captures rewrite sequences of arbitrary ordinal length, but it has neither the need for ordinals nor for metric convergence. This makes the framework especially suitable for formalizations in theorem provers. We present a coinductive framework for defining infinitary analogues of equational reasoning and rewriting in a uniform way. The setup captures rewrite sequences of arbitrary ordinal length, but it has neither the need for ordinals nor for metric convergence. This makes the framework especially suitable for formalizations in theorem provers. 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.