Abstract

Proof terms are a useful concept for comparing computations in term rewriting. The residual operation is an important operation on proof terms, used to define projection equivalence. We present a variant of the residual system (Definition 8.7.54 of TeReSe) that is (innermost) confluent and terminating, and thus can be used to decide projection equivalence.

BibTeX Entry

@inproceedings{KM-IWC19,
 author    = "Christina Kohl and Aart Middeldorp",
 title     = "Residuals Revisited",
 booktitle = "Joint Proceedings of the 10th Workshop on Higher-Order
              Rewriting and the 7th International Workshop on Confluence",
 editor    = "Mauricio Ayala-Rinc\'on and Silvia Ghilezan and Jakob Grue
              Simonsen",
 pages     = "43--47",
 year      = 2019
}