A normalisation result for higher-order calculi with explicit substitutions

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. Mellies observed that the dynamical properties of a rewrite system and its ES-based implementation...

Descripción completa

Detalles Bibliográficos
Autor principal: Bonelli, Eduardo
Formato: Objeto de conferencia
Lenguaje:Inglés
Publicado: 2003
Materias:
Informática
Acceso en línea:http://sedici.unlp.edu.ar/handle/10915/138308
Aporte de:
SEDICI (UNLP) de Universidad Nacional de La Plata
id I19-R120-10915-138308
record_format dspace
institution Universidad Nacional de La Plata
institution_str I-19
repository_str R-120
collection SEDICI (UNLP)
language Inglés
topic Informática
spellingShingle Informática
Bonelli, Eduardo
A normalisation result for higher-order calculi with explicit substitutions
topic_facet Informática
description 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. Mellies 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.
format Objeto de conferencia
Objeto de conferencia
author Bonelli, Eduardo
author_facet Bonelli, Eduardo
author_sort Bonelli, Eduardo
title A normalisation result for higher-order calculi with explicit substitutions
title_short A normalisation result for higher-order calculi with explicit substitutions
title_full A normalisation result for higher-order calculi with explicit substitutions
title_fullStr A normalisation result for higher-order calculi with explicit substitutions
title_full_unstemmed A normalisation result for higher-order calculi with explicit substitutions
title_sort normalisation result for higher-order calculi with explicit substitutions
publishDate 2003
url http://sedici.unlp.edu.ar/handle/10915/138308
work_keys_str_mv AT bonellieduardo anormalisationresultforhigherordercalculiwithexplicitsubstitutions
AT bonellieduardo normalisationresultforhigherordercalculiwithexplicitsubstitutions
bdutipo_str Repositorios
_version_ 1764820457057419264

Ejemplares similares