Residuals in Higher-Order Rewriting
H. J. Sander Bruggink · 2003
Abstract. Residuals have been studied for various forms of rewriting setting. In this article we study residuals in orthogonal Pattern Rewriting Systems (PRSs). First, the rewrite relation is defined by means of a higher-order rewriting logic, and proof terms are defined that witness reductions. Then, we have the formal machinery to define a residual operator for PRSs, and we will prove that an orthogonal PRS together with the residual operator mentioned above, is a residual system. As a side-effect, all results of (abstract) residual theory are inherited by orthogonal PRSs, such as confluence, and the notion of permutation equivalence of reductions. 1