A normalisation result for higher-order calculi with explicit substitutions
Material type:
ArticleSeries: ^p Datos electrónicos (1 archivo : 323 KB)Subject(s): Online resources: Summary: 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 P.- A. Melli`es 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.
| Item type | Home library | Collection | Call number | URL | Status | Date due | Barcode | |
|---|---|---|---|---|---|---|---|---|
Capítulo de libro
|
Biblioteca de la Facultad de Informática | Biblioteca digital | A0051 (Browse shelf(Opens below)) | Link to resource | No corresponde |
Formato de archivo: PDF. -- Este documento es producción intelectual de la Facultad de Informática-UNLP (Colección BIPA / Biblioteca.) -- Disponible también en línea vía suscripción BECyT (Cons. 10-03-2008)
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 P.- A. Melli`es 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.
International Conference on Foundations of Software Science and Computation Structures (FOSSACS), satellite event of the European Joint Conferences on Theory and Practice of Software (ETAPS). A.D. Gordon (Ed.): FOSSACS 2003, Lecture Notes in Computer Science (LNCS) 2620, pp. 153–168, April 2003.