A normalisation result for higher-order calculi with explicit substitutions

Título:

A normalisation result for higher-order calculi with explicit substitutions

Autor:

Bonelli, Eduardo

Colaboradores:

; 

Temas:

LÓGICA COMPUTACIONALSISTEMAS DE REESCRITURACÁLCULO LAMBDA

En:

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.

Resumen:

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.

URL/DOI:

Medio:

Soporte electrónico

Tipo de documento:

Artículo

Idioma:

Inglés

Publicación:

, 2003

Puede solicitar más fácilmente el ejemplar con: A0051

Ver estantes