| Outermost-Fair Rewriting (1997) | |||||||||||||||||
Abstract | |||||||||||||||||
| . A rewrite sequence is said to be outermost-fair if every outermost redex occurrence is eventually eliminated. O'Donnell has shown that outermost-fair rewriting is normalising for almost orthogonal firstorder term rewriting systems. In this paper we extend this result to the higher-order case. 1 Introduction It may occur that a term can be rewritten to normal form but is also the starting point of an infinite rewrite sequence. In that case it is important to know how to rewrite the term such that eventually a normal form is obtained. The question of how to rewrite a term can be answered by a strategy, which selects one or more redex occurrences in every term that is not in normal form. If repeatedly contracting the redex occurrences that are selected by the strategy yields a normal form whenever the initial term has one, the strategy is said to be normalising. A classical result for -calculus with fi-reduction is that the strategy selecting the leftmost redex occurrence is normalisi... | |||||||||||||||||
Details der Publikation | |||||||||||||||||
| |||||||||||||||||