HIGHER-ORDER REWRITE SYSTEMS AND THEIR CONFLUENCE

We study higher-order rewrite systems (HRSs) which extend term rewriti ng to lambda-terms. HRSs can describe computations over terms with bou nd variables. We show that rewriting with HRSs is closely related to u ndirected equational reasoning. We define pattern rewrite systems (PRS s) as a special case of HRSs and extend three confluence results from term rewriting to PRSs: the critical pair lemma by Knuth and Bendix, c onfluence of rewriting module equations a la Huet, and confluence of o rthogonal PRSs.