cl-banner

Residuals Revisited

Christina Kohl and Aart Middeldorp

Joint Proceedings of the 10th Workshop on Higher-Order Rewriting (HOR 2019) and the 7th International Workshop on Confluence (IWC 2019), pp. 43 – 47, 2019.

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.

 

  PDF

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
}
Nach oben scrollen