Four equivalent equivalences of reductions

V. van Oostrom; R.C. de Vrijer

doi:10.1016/s1571-0661(04)80599-1

Four equivalent equivalences of reductions

V. van Oostrom
, R.C. de Vrijer

Research output: Contribution to Journal › Article › Academic › peer-review

Abstract

Two co-initial reductions in a term rewriting system are said to be equivalent if they perform the same steps, albeit maybe in a different order. We present four characterisations of such a notion of equivalence, based on permutation, standardisation, labelling and projection, respectively. We prove that the characterisations all yield the same notion of equivalence, for the class of first-order left-linear term rewriting systems. A crucial rôle in our development is played by the notion of a proof term. ©2002 Published by Elsevier Science B. V.

Original language	English
Journal	Electronic Notes in Theoretical Computer Science
Volume	70
DOIs	https://doi.org/10.1016/s1571-0661(04)80599-1
Publication status	Published - 2002

Bibliographical note

DBLP:journals/entcs/OostromV02
Proceedings title: Proceedings of the 2nd International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2002)
Publisher: Elsevier

Access to Document

10.1016/s1571-0661(04)80599-1

Persistent URL (handle)

Persistent link

Cite this

@article{7453e4f9095a4a509b5e5045efa209a5,

title = "Four equivalent equivalences of reductions",

abstract = "Two co-initial reductions in a term rewriting system are said to be equivalent if they perform the same steps, albeit maybe in a different order. We present four characterisations of such a notion of equivalence, based on permutation, standardisation, labelling and projection, respectively. We prove that the characterisations all yield the same notion of equivalence, for the class of first-order left-linear term rewriting systems. A crucial r{\^o}le in our development is played by the notion of a proof term. {\textcopyright}2002 Published by Elsevier Science B. V.",

author = "\{van Oostrom\}, V. and \{de Vrijer\}, R.C.",

note = "DBLP:journals/entcs/OostromV02 Proceedings title: Proceedings of the 2nd International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2002) Publisher: Elsevier",

year = "2002",

doi = "10.1016/s1571-0661(04)80599-1",

language = "English",

volume = "70",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier B.V.",

}

TY - JOUR

T1 - Four equivalent equivalences of reductions

AU - van Oostrom, V.

AU - de Vrijer, R.C.

N1 - DBLP:journals/entcs/OostromV02 Proceedings title: Proceedings of the 2nd International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2002) Publisher: Elsevier

PY - 2002

Y1 - 2002

N2 - Two co-initial reductions in a term rewriting system are said to be equivalent if they perform the same steps, albeit maybe in a different order. We present four characterisations of such a notion of equivalence, based on permutation, standardisation, labelling and projection, respectively. We prove that the characterisations all yield the same notion of equivalence, for the class of first-order left-linear term rewriting systems. A crucial rôle in our development is played by the notion of a proof term. ©2002 Published by Elsevier Science B. V.

AB - Two co-initial reductions in a term rewriting system are said to be equivalent if they perform the same steps, albeit maybe in a different order. We present four characterisations of such a notion of equivalence, based on permutation, standardisation, labelling and projection, respectively. We prove that the characterisations all yield the same notion of equivalence, for the class of first-order left-linear term rewriting systems. A crucial rôle in our development is played by the notion of a proof term. ©2002 Published by Elsevier Science B. V.

U2 - 10.1016/s1571-0661(04)80599-1

DO - 10.1016/s1571-0661(04)80599-1

M3 - Article

SN - 1571-0661

VL - 70

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

ER -

Four equivalent equivalences of reductions

Abstract

Bibliographical note

Access to Document

Persistent URL (handle)

Fingerprint

Cite this