Normalisation 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 Melliès observed that the dynamical properties of a rewrite system and its ES-based implementation may not...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Bonelli, Eduardo
Formato: Articulo
Lenguaje:Inglés
Publicado: 2005
Materias:
Ciencias Informáticas
Explicit substitutions
Higher-order rewriting
Lamda calculus
Needed-strategies
Normalisation
Normalización
Estrategias
Cálculo
Substituciones explícitas
Acceso en línea:http://sedici.unlp.edu.ar/handle/10915/84837
Aporte de:
SEDICI (UNLP) de Universidad Nacional de La Plata
id I19-R120-10915-84837
record_format dspace
institution Universidad Nacional de La Plata
institution_str I-19
repository_str R-120
collection SEDICI (UNLP)
language Inglés
topic Ciencias Informáticas
Explicit substitutions
Higher-order rewriting
Lamda calculus
Needed-strategies
Normalisation
Normalización
Estrategias
Cálculo
Substituciones explícitas
spellingShingle Ciencias Informáticas
Explicit substitutions
Higher-order rewriting
Lamda calculus
Needed-strategies
Normalisation
Normalización
Estrategias
Cálculo
Substituciones explícitas
Bonelli, Eduardo
Normalisation for higher-order calculi with explicit substitutions
topic_facet Ciencias Informáticas
Explicit substitutions
Higher-order rewriting
Lamda calculus
Needed-strategies
Normalisation
Normalización
Estrategias
Cálculo
Substituciones explícitas
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 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.
format Articulo
Articulo
author Bonelli, Eduardo
author_facet Bonelli, Eduardo
author_sort Bonelli, Eduardo
title Normalisation for higher-order calculi with explicit substitutions
title_short Normalisation for higher-order calculi with explicit substitutions
title_full Normalisation for higher-order calculi with explicit substitutions
title_fullStr Normalisation for higher-order calculi with explicit substitutions
title_full_unstemmed Normalisation for higher-order calculi with explicit substitutions
title_sort normalisation for higher-order calculi with explicit substitutions
publishDate 2005
url http://sedici.unlp.edu.ar/handle/10915/84837
work_keys_str_mv AT bonellieduardo normalisationforhigherordercalculiwithexplicitsubstitutions
bdutipo_str Repositorios
_version_ 1764820488634236928

Ejemplares similares