Projections for infinitary rewriting

DOI10.1016/J.ENTCS.2017.04.009zbMATH Open1394.68201arXiv1605.07808OpenAlexW2403682454WikidataQ113317594 ScholiaQ113317594MaRDI QIDQ1744449FDOQ1744449

Authors: Carlos Lombardi, A. Ríos, Roel de Vrijer 

Publication date: 23 April 2018

Abstract: Proof terms in term rewriting are a representation means for reduction sequences, and more in general for contraction activity, allowing to distinguish e.g simultaneous from sequential reduction. Proof terms for finitary, first-order, left-linear term rewriting are described in the Terese book, chapter 8. In a previous work, we defined an extension of the finitary proof-term formalism, that allows to describe contractions in infinitary first-order term rewriting, and gave a characterisation of permutation equivalence. In this work, we discuss how projections of possibly infinite rewrite sequences can be modeled using proof terms. Again, the foundation is a characterisation of projections for finitary rewriting described in Terese, Section 8.7. We extend this characterisation to infinitary rewriting and also refine it, by describing precisely the role that structural equivalence plays in the development of the notion of projection. The characterisation we propose yields a definite expression, i.e. a proof term, that describes the projection of an infinitary reduction over another. To illustrate the working of projections, we show how a common reduct of a (possibly infinite) reduction and a single step that makes part of it can be obtained via their respective projections. We show, by means of several examples, that the proposed definition yields the expected behavior also in cases beyond those covered by this result. Finally, we discuss how the notion of limit is used in our definition of projection for infinite reduction.

Full work available at URL: https://arxiv.org/abs/1605.07808

Recommendations

• Projections for infinitary rewriting (extended version)
• Proof Terms for Infinitary Rewriting
• Infinitary rewriting: foundations revisited
• Infinitary rewriting: closure operators, equivalences and models
• Computing with Infinite Terms and Infinite Reductions

zbMATH Keywords

projectionpermutation equivalenceinfinitary term rewritingproof terms

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Cites Work

• The lambda calculus. Its syntax and semantics. Rev. ed.
• Title not available (Why is that?)
• Title not available (Why is that?)
• Rewrite, rewrite, rewrite, rewrite, rewrite, \dots
• Transfinite reductions in orthogonal term rewriting systems
• Infinitary normalization
• A nonstandard standardization theorem
• Projections for infinitary rewriting
• Reinterpreting compression in infinitary rewriting
• Proof Terms for Infinitary Rewriting
• A coinductive framework for infinitary rewriting and equational reasoning

Cited In (6)

• Projections for infinitary rewriting
• Projective DNF formulae and their revision
• Title not available (Why is that?)
• Proof Terms for Infinitary Rewriting
• Four equivalent equivalences of reductions
• Projections for infinitary rewriting (extended version)

This page was built for publication: Projections for infinitary rewriting

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1744449)