Projections for infinitary rewriting (extended version)

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 the literature. 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 modelled using proof terms. Again, the foundation is a characterisation of projections for finitary rewriting. 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 behaviour 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 language English 92-110 19 Theoretical Computer Science 781 https://doi.org/10.1016/j.tcs.2019.02.017 Published - 16 Aug 2019

Rewriting
Projection
Term Rewriting
Term
Contraction
Equivalence
First-order
Reduct
Permutation

Keywords

• Infinitary term rewriting
• Permutation equivalence
• Projection
• Proof terms

Cite this

Lombardi, Carlos ; Ríos, Alejandro ; de Vrijer, Roel. / Projections for infinitary rewriting (extended version). In: Theoretical Computer Science. 2019 ; Vol. 781. pp. 92-110.
@article{baff720806d44036b1dfe5506fdc28b4,
title = "Projections for infinitary rewriting (extended version)",
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 literature. 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 modelled using proof terms. Again, the foundation is a characterisation of projections for finitary rewriting. 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 behaviour 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.",
keywords = "Infinitary term rewriting, Permutation equivalence, Projection, Proof terms",
author = "Carlos Lombardi and Alejandro R{\'i}os and {de Vrijer}, Roel",
year = "2019",
month = "8",
day = "16",
doi = "10.1016/j.tcs.2019.02.017",
language = "English",
volume = "781",
pages = "92--110",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier",

}

Projections for infinitary rewriting (extended version). / Lombardi, Carlos; Ríos, Alejandro; de Vrijer, Roel.

In: Theoretical Computer Science, Vol. 781, 16.08.2019, p. 92-110.

Research output: Contribution to JournalArticleAcademicpeer-review

TY - JOUR

T1 - Projections for infinitary rewriting (extended version)

AU - Lombardi, Carlos

AU - Ríos, Alejandro

AU - de Vrijer, Roel

PY - 2019/8/16

Y1 - 2019/8/16

N2 - 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 literature. 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 modelled using proof terms. Again, the foundation is a characterisation of projections for finitary rewriting. 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 behaviour 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.

AB - 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 literature. 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 modelled using proof terms. Again, the foundation is a characterisation of projections for finitary rewriting. 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 behaviour 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.

KW - Infinitary term rewriting

KW - Permutation equivalence

KW - Projection

KW - Proof terms

UR - http://www.scopus.com/inward/record.url?scp=85063205932&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85063205932&partnerID=8YFLogxK

U2 - 10.1016/j.tcs.2019.02.017

DO - 10.1016/j.tcs.2019.02.017

M3 - Article

VL - 781

SP - 92

EP - 110

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

ER -