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

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