Higher-Order Rewrite Systems and their Confluence
Richard Mayr, Tobias Nipkow
We study Higher-Order Rewrite Systems (HRSs) which extend term rewriting to
lambda-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.
dvi
ps
BibTeX:
@article{Mayr-Nipkow-TCS,author={Richard Mayr and Tobias Nipkow},
title={Higher-Order Rewrite Systems and their Confluence},
journal=TCS,volume=192,year=1998,pages={3--29}}