Espacios de reducción en sistemas de reescritura no-secuenciales e infinitarios

Mostrar todas las versiones(3)

En esta tesis estudiamos distintos aspectos ligados al espacio de reducción de diversos sistemas de reescritura. Los sistemas abarcados presentan características que hacen que el estudio de sus espacios de reducción diste de ser una tarea sencilla. Las principales contribuciones son: (1) se define u...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Lombardi, Carlos Alberto
Otros Autores: Ríos, Alejandro Norberto
Formato: Tesis doctoral publishedVersion
Lenguaje:Inglés
Publicado: Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2014
Materias:
REESCRITURA
ESTANDARIZACION
ESTRATEGIAS DE REDUCCION NORMALIZANTES
EQUIVALENCIA ENTRE REDUCCIONES
CALCULOS CON PATRONES
CALCULOS CON SUSTITUCIONES EXPLICITAS
REESCRITURA INFINITARIA
SISTEMAS ABSTRACTOS DE REESCRITURA
PROOF TERMS
REWRITING
STANDARDISATION
NORMALISING REDUCTION STRATEGIES
EQUIVALENCE OF REDUCTIONS
PATTERN CALCULI
CALCULI WITH EXPLICIT SUBSTITUTIONS
INFINITARY REWRITING
ABSTRACT REWRITING SYSTEMS
Acceso en línea:https://hdl.handle.net/20.500.12110/tesis_n5644_Lombardi
https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesis&d=tesis_n5644_Lombardi_oai
Aporte de:
Repositorio Digital de la Universidad de Buenos Aires (UBA) de Universidad de Buenos Aires
id I28-R145-tesis_n5644_Lombardi_oai
record_format dspace
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-145
collection Repositorio Digital de la Universidad de Buenos Aires (UBA)
language Inglés
orig_language_str_mv eng
topic REESCRITURA
ESTANDARIZACION
ESTRATEGIAS DE REDUCCION NORMALIZANTES
EQUIVALENCIA ENTRE REDUCCIONES
CALCULOS CON PATRONES
CALCULOS CON SUSTITUCIONES EXPLICITAS
REESCRITURA INFINITARIA
SISTEMAS ABSTRACTOS DE REESCRITURA
PROOF TERMS
REWRITING
STANDARDISATION
NORMALISING REDUCTION STRATEGIES
EQUIVALENCE OF REDUCTIONS
PATTERN CALCULI
CALCULI WITH EXPLICIT SUBSTITUTIONS
INFINITARY REWRITING
ABSTRACT REWRITING SYSTEMS
PROOF TERMS
spellingShingle REESCRITURA
ESTANDARIZACION
ESTRATEGIAS DE REDUCCION NORMALIZANTES
EQUIVALENCIA ENTRE REDUCCIONES
CALCULOS CON PATRONES
CALCULOS CON SUSTITUCIONES EXPLICITAS
REESCRITURA INFINITARIA
SISTEMAS ABSTRACTOS DE REESCRITURA
PROOF TERMS
REWRITING
STANDARDISATION
NORMALISING REDUCTION STRATEGIES
EQUIVALENCE OF REDUCTIONS
PATTERN CALCULI
CALCULI WITH EXPLICIT SUBSTITUTIONS
INFINITARY REWRITING
ABSTRACT REWRITING SYSTEMS
PROOF TERMS
Lombardi, Carlos Alberto
Espacios de reducción en sistemas de reescritura no-secuenciales e infinitarios
topic_facet REESCRITURA
ESTANDARIZACION
ESTRATEGIAS DE REDUCCION NORMALIZANTES
EQUIVALENCIA ENTRE REDUCCIONES
CALCULOS CON PATRONES
CALCULOS CON SUSTITUCIONES EXPLICITAS
REESCRITURA INFINITARIA
SISTEMAS ABSTRACTOS DE REESCRITURA
PROOF TERMS
REWRITING
STANDARDISATION
NORMALISING REDUCTION STRATEGIES
EQUIVALENCE OF REDUCTIONS
PATTERN CALCULI
CALCULI WITH EXPLICIT SUBSTITUTIONS
INFINITARY REWRITING
ABSTRACT REWRITING SYSTEMS
PROOF TERMS
description En esta tesis estudiamos distintos aspectos ligados al espacio de reducción de diversos sistemas de reescritura. Los sistemas abarcados presentan características que hacen que el estudio de sus espacios de reducción diste de ser una tarea sencilla. Las principales contribuciones son: (1) se define una estrategia de reducción multipaso para el Pure Pattern Calculus, un calculo con patrones no-secuencial, y se demuestra que dicha estrategia es normalizante; (2) se propone un criterio para formalizar el concepto de reducción standard en el Linear Substitution Calculus, un cálculo de sustituciones explícitas cuyas reducciones se consideran módulo una relación de equivalencia sobre su conjunto de términos, obteniéndose un resultado de unicidad de reducciones standard para el criterio definido; y (3) se caracteriza la equivalencia entre reducciones para los sistemas de reescritura de términos infinitarios de primer orden y lineales a izquierda, utilizándose esta caracterización para desarrollar una demostración alternativa del resultado de compresión. Destacamos el uso de modelos genéricos de sistemas de reescritura: se utiliza una formulación de Sistemas Abstractos de Reescritura para estudiar el Pure Pattern Calculus y el Linear Substitution Calculus, y un modelo basado en proof terms para estudiar la reescritura infinitaria. Esta tesis incluye asimismo extensiones de los dos modelos genéricos utilizados, que pueden considerarse contribuciones adicionales de la misma.
author2 Ríos, Alejandro Norberto
author_facet Ríos, Alejandro Norberto
Lombardi, Carlos Alberto
format Tesis doctoral
Tesis doctoral
publishedVersion
author Lombardi, Carlos Alberto
author_sort Lombardi, Carlos Alberto
title Espacios de reducción en sistemas de reescritura no-secuenciales e infinitarios
title_short Espacios de reducción en sistemas de reescritura no-secuenciales e infinitarios
title_full Espacios de reducción en sistemas de reescritura no-secuenciales e infinitarios
title_fullStr Espacios de reducción en sistemas de reescritura no-secuenciales e infinitarios
title_full_unstemmed Espacios de reducción en sistemas de reescritura no-secuenciales e infinitarios
title_sort espacios de reducción en sistemas de reescritura no-secuenciales e infinitarios
publisher Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
publishDate 2014
url https://hdl.handle.net/20.500.12110/tesis_n5644_Lombardi
https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesis&d=tesis_n5644_Lombardi_oai
work_keys_str_mv AT lombardicarlosalberto espaciosdereduccionensistemasdereescrituranosecuencialeseinfinitarios
AT lombardicarlosalberto reductionspacesinnonsequencialandinfinitaryrewritingsystems
_version_ 1824355728914120704
spelling I28-R145-tesis_n5644_Lombardi_oai2024-09-02 Ríos, Alejandro Norberto Kesner, Delia Nora Bonelli, Eduardo Augusto Lombardi, Carlos Alberto 2014-11-07 En esta tesis estudiamos distintos aspectos ligados al espacio de reducción de diversos sistemas de reescritura. Los sistemas abarcados presentan características que hacen que el estudio de sus espacios de reducción diste de ser una tarea sencilla. Las principales contribuciones son: (1) se define una estrategia de reducción multipaso para el Pure Pattern Calculus, un calculo con patrones no-secuencial, y se demuestra que dicha estrategia es normalizante; (2) se propone un criterio para formalizar el concepto de reducción standard en el Linear Substitution Calculus, un cálculo de sustituciones explícitas cuyas reducciones se consideran módulo una relación de equivalencia sobre su conjunto de términos, obteniéndose un resultado de unicidad de reducciones standard para el criterio definido; y (3) se caracteriza la equivalencia entre reducciones para los sistemas de reescritura de términos infinitarios de primer orden y lineales a izquierda, utilizándose esta caracterización para desarrollar una demostración alternativa del resultado de compresión. Destacamos el uso de modelos genéricos de sistemas de reescritura: se utiliza una formulación de Sistemas Abstractos de Reescritura para estudiar el Pure Pattern Calculus y el Linear Substitution Calculus, y un modelo basado en proof terms para estudiar la reescritura infinitaria. Esta tesis incluye asimismo extensiones de los dos modelos genéricos utilizados, que pueden considerarse contribuciones adicionales de la misma. We study different aspects related to the reduction spaces of diverse rewriting systems. These systems include features which make the study of their reduction spaces a far from trivial task. The main contributions of this thesis are: (1) we define a multistep reduction strategy for the Pure Pattern Calculus, a non-sequential higher-order term rewriting system, and we prove that the defined strategy is normalizing; (2) we propose a formalisation of the concept of standard reduction for the Linear Substitution Calculus, a calculus of explicit substitutions whose reductions are considered modulo an equivalence relation defined on the set of terms, and we obtain a result of uniqueness of standard reductions for this formalisation; and nally, (3) we characterise the equivalence of reductions for the innitary, rst-order, left-linear term rewriting systems, and we use this characterisation to develop an alternative proof of the compression result. We remark that we use generic models of rewriting systems: a version of the notion of Abstract Rewriting Systems is used for the study of the Pure Pattern Calculus and the Linear Substitution Calculus, while a model based on the concept of proof terms is used for the study of infinitary rewriting. We include extensions of both used generic models; these extensions can be considered as additional contributions of this thesis. Fil: Lombardi, Carlos Alberto. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. application/pdf https://hdl.handle.net/20.500.12110/tesis_n5644_Lombardi eng Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar REESCRITURA ESTANDARIZACION ESTRATEGIAS DE REDUCCION NORMALIZANTES EQUIVALENCIA ENTRE REDUCCIONES CALCULOS CON PATRONES CALCULOS CON SUSTITUCIONES EXPLICITAS REESCRITURA INFINITARIA SISTEMAS ABSTRACTOS DE REESCRITURA PROOF TERMS REWRITING STANDARDISATION NORMALISING REDUCTION STRATEGIES EQUIVALENCE OF REDUCTIONS PATTERN CALCULI CALCULI WITH EXPLICIT SUBSTITUTIONS INFINITARY REWRITING ABSTRACT REWRITING SYSTEMS PROOF TERMS Espacios de reducción en sistemas de reescritura no-secuenciales e infinitarios Reduction spaces in non-sequencial and infinitary rewriting systems info:eu-repo/semantics/doctoralThesis info:ar-repo/semantics/tesis doctoral info:eu-repo/semantics/publishedVersion https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesis&d=tesis_n5644_Lombardi_oai

Ejemplares similares