| Erasure and Termination in Higher-Order Rewriting (2008) | |||||||||||||||
Abstract | |||||||||||||||
| Abstract. Two applications of the Erasure Lemma for first-order orthogonal term rewriting systems are: weak innermost termination implies termination, and weak normalization implies strong normalization for non-erasing systems. We discuss these two results in the setting of higher-order rewriting. 1 | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||