Reescritura de términos y sustituciones explícitas

La operación de sustitución constituye un engranaje básico en los fundamentos de la teoría de lenguajes de programación. Juega un rol central en el lambda cálculo (por ende, en lenguajes de programación funcional), en unificación de primer orden y de orden superior (por ende, en lenguajes de program...

Descripción completa

Detalles Bibliográficos
Autor principal: Bonelli, Eduardo Augusto
Otros Autores: Kesner, Delia Nora
Formato: Tesis doctoral publishedVersion
Lenguaje:Inglés
Publicado: Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2003
Acceso en línea:https://hdl.handle.net/20.500.12110/tesis_n3651_Bonelli
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id tesis:tesis_n3651_Bonelli
record_format dspace
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
language Inglés
orig_language_str_mv eng
description La operación de sustitución constituye un engranaje básico en los fundamentos de la teoría de lenguajes de programación. Juega un rol central en el lambda cálculo (por ende, en lenguajes de programación funcional), en unificación de primer orden y de orden superior (por ende, en lenguajes de programación basados en el paradigma lógico), en modalidades de pasaje de parámetros (por ende, en lenguajes de programación imperativos), etc. Recientemente, investigadores en informática se han interesado en el pasaje de la noción usual de la sustitución, atómica, y de gruesa granularidad, hacia una noción más refinada, de más fina granularidad. La noción de sustitución es transportada del metalenguaje (nuestro lenguaje de discurso) al lenguaje objeto (nuestro lenguaje de estudio). Como consecuencia de ello se obtienen los llamados cálculos de sustituciones explícitas. Estos son de sumo interés a la hora de estudiar la interpretación operacional de los formalismos en cuestión y constituyen los objetos de interés de esta tesis. Se desarrollan los siguientes tres ejes de estudio: Primero, se consideran estrategias de reescritura perpetuas en lambda cálculos con sustituciones explícitas. Estas son estrategias de reescritura que preservan la posibilidad de reducciones infinitas. Se propone una caracterización inductiva del conjunto de términos que no poseen reducciones infinitas (los llamados fuertemente normalizantes). Un lambda cálculo polimórfico con sustituciones explícitas también es analizado, incluyendo propiedades tales como subject reduction y normalización fuerte. Segundo, colocamos el ς-cálculo de M. Abadi and L. Cardelli enriquecido con sustituciones explícitas bajo el microscopio. Este cálculo se encuentra en un nivel semejante de abstracción al lambda cálculo pero se basa en objetos en lugar de funciones. Propiedades tales como simulación del lambda cálculo, confluencia y preservación de la normalización fuerte (aquellos términos que son fuertemente normalizantes en ς también lo son en ς con sustituciones explícitas) son consideradas. Finalmente, dirigimos nuestra atención a la tarea de relacionar la reescritura de orden superior con aquella de primer orden. Fijamos una variante de los ERS (apodados SERSdb) de Z. Khasidashvili como nuestro formalismo de orden superior de partida y definimos un proceso de conversión que permite codificar cualquier SERSdb como un sistema de reescritura de primer orden. En este último, cada paso de reescritura se lleva a cabo módulo una teoría ecuacional determinada por un cálculo de sustituciones explícitas. La misma se formula de manera genérica a través de una presentación de cálculos de sustituciones explícitas basada en macros y axiomas sobre estas macros, parametrizando de esta manera al procedimiento de conversión sobre cualquier cálculo de sustituciones explícitas que obedece la presentación basada en macros. El procedimiento de conversión se encarga de codificar pattern matching de orden superior y sustitución en el entorno de reescritura de primer orden. Asimismo, propiedades que relacionan la noción de reescritura en el orden superior con aquella de primer orden son analizadas en detalle. Se identifica una clase de SERSdb para los cuales el sistema de primer orden resultante de su conversión no requiere una teoría ecuacional para implementar pattern matching de orden superior, bastando para ello matching sintáctico. También se argumenta que esta clase de sistemas de orden superior es apropiada para transferir resultados del entorno de reescritura de orden superior a aquella de primer orden. A modo de ejemplo no-trivial de ello, estudiamos la transferencia del teorema de standarización (fuerte).
author2 Kesner, Delia Nora
author_facet Kesner, Delia Nora
Bonelli, Eduardo Augusto
format Tesis doctoral
Tesis doctoral
publishedVersion
author Bonelli, Eduardo Augusto
spellingShingle Bonelli, Eduardo Augusto
Reescritura de términos y sustituciones explícitas
author_sort Bonelli, Eduardo Augusto
title Reescritura de términos y sustituciones explícitas
title_short Reescritura de términos y sustituciones explícitas
title_full Reescritura de términos y sustituciones explícitas
title_fullStr Reescritura de términos y sustituciones explícitas
title_full_unstemmed Reescritura de términos y sustituciones explícitas
title_sort reescritura de términos y sustituciones explícitas
publisher Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
publishDate 2003
url https://hdl.handle.net/20.500.12110/tesis_n3651_Bonelli
work_keys_str_mv AT bonellieduardoaugusto reescrituradeterminosysustitucionesexplicitas
_version_ 1831981191906983936
spelling tesis:tesis_n3651_Bonelli2025-03-31T21:19:50Z Reescritura de términos y sustituciones explícitas Bonelli, Eduardo Augusto Kesner, Delia Nora Ríos, Alejandro La operación de sustitución constituye un engranaje básico en los fundamentos de la teoría de lenguajes de programación. Juega un rol central en el lambda cálculo (por ende, en lenguajes de programación funcional), en unificación de primer orden y de orden superior (por ende, en lenguajes de programación basados en el paradigma lógico), en modalidades de pasaje de parámetros (por ende, en lenguajes de programación imperativos), etc. Recientemente, investigadores en informática se han interesado en el pasaje de la noción usual de la sustitución, atómica, y de gruesa granularidad, hacia una noción más refinada, de más fina granularidad. La noción de sustitución es transportada del metalenguaje (nuestro lenguaje de discurso) al lenguaje objeto (nuestro lenguaje de estudio). Como consecuencia de ello se obtienen los llamados cálculos de sustituciones explícitas. Estos son de sumo interés a la hora de estudiar la interpretación operacional de los formalismos en cuestión y constituyen los objetos de interés de esta tesis. Se desarrollan los siguientes tres ejes de estudio: Primero, se consideran estrategias de reescritura perpetuas en lambda cálculos con sustituciones explícitas. Estas son estrategias de reescritura que preservan la posibilidad de reducciones infinitas. Se propone una caracterización inductiva del conjunto de términos que no poseen reducciones infinitas (los llamados fuertemente normalizantes). Un lambda cálculo polimórfico con sustituciones explícitas también es analizado, incluyendo propiedades tales como subject reduction y normalización fuerte. Segundo, colocamos el ς-cálculo de M. Abadi and L. Cardelli enriquecido con sustituciones explícitas bajo el microscopio. Este cálculo se encuentra en un nivel semejante de abstracción al lambda cálculo pero se basa en objetos en lugar de funciones. Propiedades tales como simulación del lambda cálculo, confluencia y preservación de la normalización fuerte (aquellos términos que son fuertemente normalizantes en ς también lo son en ς con sustituciones explícitas) son consideradas. Finalmente, dirigimos nuestra atención a la tarea de relacionar la reescritura de orden superior con aquella de primer orden. Fijamos una variante de los ERS (apodados SERSdb) de Z. Khasidashvili como nuestro formalismo de orden superior de partida y definimos un proceso de conversión que permite codificar cualquier SERSdb como un sistema de reescritura de primer orden. En este último, cada paso de reescritura se lleva a cabo módulo una teoría ecuacional determinada por un cálculo de sustituciones explícitas. La misma se formula de manera genérica a través de una presentación de cálculos de sustituciones explícitas basada en macros y axiomas sobre estas macros, parametrizando de esta manera al procedimiento de conversión sobre cualquier cálculo de sustituciones explícitas que obedece la presentación basada en macros. El procedimiento de conversión se encarga de codificar pattern matching de orden superior y sustitución en el entorno de reescritura de primer orden. Asimismo, propiedades que relacionan la noción de reescritura en el orden superior con aquella de primer orden son analizadas en detalle. Se identifica una clase de SERSdb para los cuales el sistema de primer orden resultante de su conversión no requiere una teoría ecuacional para implementar pattern matching de orden superior, bastando para ello matching sintáctico. También se argumenta que esta clase de sistemas de orden superior es apropiada para transferir resultados del entorno de reescritura de orden superior a aquella de primer orden. A modo de ejemplo no-trivial de ello, estudiamos la transferencia del teorema de standarización (fuerte). Substitution spans many areas in programming language theory. It plays a central role in the lambda calculus (hence functional programming), in first and higher-order unikation (hence logic programming), parameter passing methods (hence imperative programming), etc. Recently researchers became interested in shifting from the usual atomic, coarse grained view of substitution to a more refined, fine grained one. Substitution is promoted from the metalevel (our language of discourse) to the object-level (our language of study). This is interesting when studying the operational interpretation of the formalisms in question. Calculi of object-level or explicit substitution is the concern of this thesis. The following three study axes are developed. First we consider perpetual rewrite strategies in lambda calculi of explicit substitutions. These are rewrite strategies that preserve the possibility of inhite derivations. Also, we study how to characterize inductively the set of terms that do not possess infinite derivations (the strongly normalizing terms). Polymorphic lambda calculus with explicit substitutions shall receive our attention too, including properties such as subject reduction and strong normalization. Secondly, we put the ς-calculus of M.Abadi and L.Cardelli augmented with explicit substitutions under the microscope. This calculus is at the level of the lambda calculus but is based on objects instead of functions. Properties such as simulation of the lambda calculus, confluence and preservation of strong normalization (terms which are strongly normalizing in ς are also strongly normalizii in ς with explicit substitutions) are considered. Finally, we address the task of reducing higher-order rewriting to first-order rewriting. We fix a variant of Z-Khasidashvili's ERS (dubbed SERSdb) as our departing formalism and provide a conversion procedure to encode any ERS as a first-order rewrite system in which a rewrite step takes place modulo an equational theory determined by a calculus of explicit substitutions. The latter is achieved with the aid of a macro-based presentation of calculi of explicit substitutions, thus parametrizing the conversion procedure over any calculus of explicit substitutions in compliance with the aforementioned presentation. The conversion procedure is in charge of encoding higherorder pattern matching and substitution in the first-order framework. Properties relating the rewrite relation in the higher-order framework and that of the resulting first-order system are studied in detail. We then identify a class of SERSdb for which the resulting first-order system does not require the equational theory to implement higher-order pattern matching, thus contenting itself with syntactic matching. It is argued that this class of systems is appropriate for transferring results from the first-order framework to the higher-order one. As a non-trivial example we study the transfer of the (strong) standardization theorem. Fil: Bonelli, Eduardo Augusto. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2003 info:eu-repo/semantics/doctoralThesis info:ar-repo/semantics/tesis doctoral info:eu-repo/semantics/publishedVersion application/pdf eng info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar https://hdl.handle.net/20.500.12110/tesis_n3651_Bonelli

Ejemplares similares