A canonical calculus of residuals
Yves Bertot · 1993
We introduce a formal language to describe origin functions, which permit to study the notions of descendance and residuals in reduction systems. Computation on this formal language are defined using a term rewriting system, which we show to be canonical. This work has application in semantics and debugging. 1 Introduction. We introduce new tools to capture the notions of descendance and residuals that appear regularly in the study of rewriting and reduction systems. These new tools provide an easier encoding of these notions and may have applications in implementing evaluation strategies [1, 5, 8, 13, 14] or debugging algorithms based on rewriting or reduction [3]. Most presentations of descendance and residuals use labeling of terms. For any reduction system, one simply produces a labeled version of the system, together with a procedure to transform a derivation on labeled terms into a derivation on unlabeled terms (called erasure) and a procedure to transform a derivation on unlab...