Higher-order rewrite systems and their confluence

Richard Mayr; Tobias Nipkow

doi:10.1016/S0304-3975(97)00143-6

Higher-order rewrite systems and their confluence

Richard Mayr, Tobias Nipkow

Informatics 7 - Chair of Theoretical Computer Science

Technical University of Munich

Research output: Contribution to journal › Article › peer-review

113 Scopus citations

Abstract

We study higher-order rewrite systems (HRSs) which extend term rewriting to λ-terms. HRSs can describe computations over terms with bound variables. We show that rewriting with HRSs is closely related to undirected equational reasoning. We define pattern rewrite systems (PRSs) as a special case of HRSs and extend three confluence results from term rewriting to PRSs: the critical pair lemma by Knuth and Bendix, confluence of rewriting modulo equations à la Huet, and confluence of orthogonal PRSs.

Original language	English
Pages (from-to)	3-29
Number of pages	27
Journal	Theoretical Computer Science
Volume	192
Issue number	1
DOIs	https://doi.org/10.1016/S0304-3975(97)00143-6
State	Published - 10 Feb 1998

Access to Document

10.1016/S0304-3975(97)00143-6

Cite this

@article{c40b5990b6104874933eb788659db126,

title = "Higher-order rewrite systems and their confluence",

abstract = "We study higher-order rewrite systems (HRSs) which extend term rewriting to λ-terms. HRSs can describe computations over terms with bound variables. We show that rewriting with HRSs is closely related to undirected equational reasoning. We define pattern rewrite systems (PRSs) as a special case of HRSs and extend three confluence results from term rewriting to PRSs: the critical pair lemma by Knuth and Bendix, confluence of rewriting modulo equations {\`a} la Huet, and confluence of orthogonal PRSs.",

author = "Richard Mayr and Tobias Nipkow",

year = "1998",

month = feb,

day = "10",

doi = "10.1016/S0304-3975(97)00143-6",

language = "English",

volume = "192",

pages = "3--29",

journal = "Theoretical Computer Science",

issn = "0304-3975",

publisher = "Elsevier B.V.",

number = "1",

}

TY - JOUR

T1 - Higher-order rewrite systems and their confluence

AU - Mayr, Richard

AU - Nipkow, Tobias

PY - 1998/2/10

Y1 - 1998/2/10

N2 - We study higher-order rewrite systems (HRSs) which extend term rewriting to λ-terms. HRSs can describe computations over terms with bound variables. We show that rewriting with HRSs is closely related to undirected equational reasoning. We define pattern rewrite systems (PRSs) as a special case of HRSs and extend three confluence results from term rewriting to PRSs: the critical pair lemma by Knuth and Bendix, confluence of rewriting modulo equations à la Huet, and confluence of orthogonal PRSs.

AB - We study higher-order rewrite systems (HRSs) which extend term rewriting to λ-terms. HRSs can describe computations over terms with bound variables. We show that rewriting with HRSs is closely related to undirected equational reasoning. We define pattern rewrite systems (PRSs) as a special case of HRSs and extend three confluence results from term rewriting to PRSs: the critical pair lemma by Knuth and Bendix, confluence of rewriting modulo equations à la Huet, and confluence of orthogonal PRSs.

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

U2 - 10.1016/S0304-3975(97)00143-6

DO - 10.1016/S0304-3975(97)00143-6

M3 - Article

AN - SCOPUS:0002569005

SN - 0304-3975

VL - 192

SP - 3

EP - 29

JO - Theoretical Computer Science

JF - Theoretical Computer Science

IS - 1

ER -

Higher-order rewrite systems and their confluence

Abstract

Access to Document

Other files and links

Fingerprint

Cite this