Abstract
Explicit substitutions (ES) were introduced as a bridge between the theory of rewrite systems with binders and substitution, such as the λ-calculus, and their implementation. In a seminal paper Melliès observed that the dynamical properties of a rewrite system and its ES-based implementation may not coincide: he showed that a strongly normalising term (i.e. one which does not admit infinite derivations) in the λ-calculus may lose this status in its ES-based implementation. This paper studies normalisation for the latter systems in the general setting of higher-order rewriting: Based on recent work extending the theory of needed strategies to non-orthogonal rewrite systems we show that needed strategies normalise in the ES-based implementation of any orthogonal pattern higher-order rewrite system.
Original language | English |
---|---|
Pages (from-to) | 91-125 |
Number of pages | 35 |
Journal | Theoretical Computer Science |
Volume | 333 |
Issue number | 1-2 |
DOIs | |
State | Published - 1 Mar 2005 |
Event | Foundations of Software Science and Computation Structures - Warsaw, Poland Duration: 7 Apr 2003 → 9 Apr 2003 |
Keywords
- Explicit substitutions
- Higher-order rewriting
- Lamda calculus
- Needed-strategies
- Normalisation