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


@article{Mayr-Nipkow-TCS,author={Richard Mayr and Tobias Nipkow},
title={Higher-Order Rewrite Systems and their Confluence},