Projections for Infinitary Rewriting

Carlos Lombardi, Alejandro Ríos, Roel de Vrijer

Research output: Contribution to JournalArticleAcademicpeer-review

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 [Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, UK, 2003], ch. 8. In a previous work [C. Lombardi, A. Ríos, and R. de Vrijer. Proof terms for infinitary rewriting. In G. Dowek, editor, RTA-TLCA'14, volume 8560 of Lecture Notes in Computer Science, pages 303–318. Springer, 2014] 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. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, UK, 2003], Sec. 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.

Original languageEnglish
Pages (from-to)131-148
Number of pages18
JournalElectronic Notes in Theoretical Computer Science
Volume332
DOIs
Publication statusPublished - 11 Jun 2017

Keywords

  • infinitary term rewriting
  • permutation equivalence
  • projection
  • proof terms

Fingerprint

Dive into the research topics of 'Projections for Infinitary Rewriting'. Together they form a unique fingerprint.

Cite this