Dos temas en reescritura : combinadores para cálculos con patrones e isomorfismo de Curry-Howard para la Lógica de Pruebas

Mostrar todas las versiones(3)

Pattern matching es una herramienta fundamental de la programación funcional. Permitedescribir conjuntos de datos que tienen una misma forma (a través de una expresión llamada \\patrón"). Esta facilidad ha comenzado a adoptarse también en otros paradigmas, y ha demostradosu utilidad para analiz...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Steren, Gabriela
Otros Autores: Bonelli, Eduardo
Formato: Tesis doctoral publishedVersion
Lenguaje:Inglés
Publicado: Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2014
Materias:
PATRONES
CALCULO LAMBDA
LOGICA COMBINATORIA
LOGICA MODAL
ISOMORFISMO DE CURRY-HOWARD
LOGICA DE PRUEBAS
PATTERNS
LAMBDA CALCULUS
COMBINATORY LOGIC
MODAL LOGIC
CURRY-HOWARD ISOMORPHISM
LOGIC OF PROOFS
Acceso en línea:https://hdl.handle.net/20.500.12110/tesis_n5634_Steren
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id tesis:tesis_n5634_Steren
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
topic PATRONES
CALCULO LAMBDA
LOGICA COMBINATORIA
LOGICA MODAL
ISOMORFISMO DE CURRY-HOWARD
LOGICA DE PRUEBAS
PATTERNS
LAMBDA CALCULUS
COMBINATORY LOGIC
MODAL LOGIC
CURRY-HOWARD ISOMORPHISM
LOGIC OF PROOFS
spellingShingle PATRONES
CALCULO LAMBDA
LOGICA COMBINATORIA
LOGICA MODAL
ISOMORFISMO DE CURRY-HOWARD
LOGICA DE PRUEBAS
PATTERNS
LAMBDA CALCULUS
COMBINATORY LOGIC
MODAL LOGIC
CURRY-HOWARD ISOMORPHISM
LOGIC OF PROOFS
Steren, Gabriela
Dos temas en reescritura : combinadores para cálculos con patrones e isomorfismo de Curry-Howard para la Lógica de Pruebas
topic_facet PATRONES
CALCULO LAMBDA
LOGICA COMBINATORIA
LOGICA MODAL
ISOMORFISMO DE CURRY-HOWARD
LOGICA DE PRUEBAS
PATTERNS
LAMBDA CALCULUS
COMBINATORY LOGIC
MODAL LOGIC
CURRY-HOWARD ISOMORPHISM
LOGIC OF PROOFS
description Pattern matching es una herramienta fundamental de la programación funcional. Permitedescribir conjuntos de datos que tienen una misma forma (a través de una expresión llamada \\patrón"). Esta facilidad ha comenzado a adoptarse también en otros paradigmas, y ha demostradosu utilidad para analizar datos en diversos formatos, como por ejemplo datos semiestructurados. Los cálculos de patrones son lenguajes minimales basados en cálculo lambda enlos que se introducen formas sofisticadas de pattern matching para estudiar sus fundamentosformales. La primera parte de esta tesis propone una contribución a este campo, desarrollandouna lógica combinatoria para λP, un cálculo de patrones donde cualquier término puede serun patrón. La lógica combinatoria carece de variables ligadas. Nos encontramos ante dos desafíos. Por un lado, tratar con las variables ligadas en los patrones, ya que una abstracción esun patrón válido en λP. Para esto contamos con la guía de la lógica combinatoria estándar. El segundo desafío consiste en computar, en un escenario combinatorio, la contraparte de lasustitución obtenida ante un matching exitoso. Esto requiere la introducción de reglas capacesde descomponer las aplicaciones. Proponemos una lógica combinatoria que logra este propósito,y estudiamos sus propiedades salientes y extensiones, incluyendo una presentación tipada y larepresentación de estructuras de datos. La segunda parte de esta tesis se centra en la interpretación computacional de la Lógicade Pruebas, o LP, via el isomorfismo de Curry-Howard. LP, dada a conocer por Artemov en 1995, es un refinamiento de la lógica modal en la cual la modalidad 2A es revisitada como [[t]]A, donde t es una expresión que testifica sobre la validez de A. Es aritméticamente correctay completa, puede realizar todos los teoremas de S4 y posee la capacidad de versar sobre suspropias pruebas (` A implica ` [[t]]A, para algún t). Nuestra contribución principal es unaformulación en Deducción Natural con buen comportamiento, desarrollada con el fin de develarlas metáforas computacionales que surgen de esta capacidad de reflexión de LP. Esta es laprimera formulación en Deducción Natural capaz de capturar a LP en su totalidad. Para esto,adoptamos la Deducción Natural Clásica de Parigot y la unimos al razonamiento hipotético. Como resultado, obtenemos una presentación en Deducción Natural de LP proposicional, parala cual se demuestran ciertas propiedades claves. Luego extendemos nuestro análisis al caso deprimer orden, presentando FOHLP, una extensión de primer orden de HLP. Nuestro punto departida es una reciente formulación de primer orden de LP, llamada FOLP, que goza de correcciónaritmética y tiene una semántica de demostrabilidad exacta (la completitud es inalcanzabledado que no es finitamente axiomatizable). Presentamos una formulación en Deducción Naturalllamada FOHLP, traducciones desde y hacia FOLP, una asignación de términos (cálculo lambda)y una prueba de terminación del proceso de normalización de derivaciones.
author2 Bonelli, Eduardo
author_facet Bonelli, Eduardo
Steren, Gabriela
format Tesis doctoral
Tesis doctoral
publishedVersion
author Steren, Gabriela
author_sort Steren, Gabriela
title Dos temas en reescritura : combinadores para cálculos con patrones e isomorfismo de Curry-Howard para la Lógica de Pruebas
title_short Dos temas en reescritura : combinadores para cálculos con patrones e isomorfismo de Curry-Howard para la Lógica de Pruebas
title_full Dos temas en reescritura : combinadores para cálculos con patrones e isomorfismo de Curry-Howard para la Lógica de Pruebas
title_fullStr Dos temas en reescritura : combinadores para cálculos con patrones e isomorfismo de Curry-Howard para la Lógica de Pruebas
title_full_unstemmed Dos temas en reescritura : combinadores para cálculos con patrones e isomorfismo de Curry-Howard para la Lógica de Pruebas
title_sort dos temas en reescritura : combinadores para cálculos con patrones e isomorfismo de curry-howard para la lógica de pruebas
publisher Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
publishDate 2014
url https://hdl.handle.net/20.500.12110/tesis_n5634_Steren
work_keys_str_mv AT sterengabriela dostemasenreescrituracombinadoresparacalculosconpatroneseisomorfismodecurryhowardparalalogicadepruebas
AT sterengabriela twotopicsinrewritingcombinatorsforpatterncalculiandcurryhowardforthelogicofproofs
_version_ 1782022819150823424
spelling tesis:tesis_n5634_Steren2023-10-02T20:09:57Z Dos temas en reescritura : combinadores para cálculos con patrones e isomorfismo de Curry-Howard para la Lógica de Pruebas Two topics in rewriting: combinators for pattern calculi and Curry-Howard for the Logic of Proofs Steren, Gabriela Bonelli, Eduardo PATRONES CALCULO LAMBDA LOGICA COMBINATORIA LOGICA MODAL ISOMORFISMO DE CURRY-HOWARD LOGICA DE PRUEBAS PATTERNS LAMBDA CALCULUS COMBINATORY LOGIC MODAL LOGIC CURRY-HOWARD ISOMORPHISM LOGIC OF PROOFS Pattern matching es una herramienta fundamental de la programación funcional. Permitedescribir conjuntos de datos que tienen una misma forma (a través de una expresión llamada \\patrón"). Esta facilidad ha comenzado a adoptarse también en otros paradigmas, y ha demostradosu utilidad para analizar datos en diversos formatos, como por ejemplo datos semiestructurados. Los cálculos de patrones son lenguajes minimales basados en cálculo lambda enlos que se introducen formas sofisticadas de pattern matching para estudiar sus fundamentosformales. La primera parte de esta tesis propone una contribución a este campo, desarrollandouna lógica combinatoria para λP, un cálculo de patrones donde cualquier término puede serun patrón. La lógica combinatoria carece de variables ligadas. Nos encontramos ante dos desafíos. Por un lado, tratar con las variables ligadas en los patrones, ya que una abstracción esun patrón válido en λP. Para esto contamos con la guía de la lógica combinatoria estándar. El segundo desafío consiste en computar, en un escenario combinatorio, la contraparte de lasustitución obtenida ante un matching exitoso. Esto requiere la introducción de reglas capacesde descomponer las aplicaciones. Proponemos una lógica combinatoria que logra este propósito,y estudiamos sus propiedades salientes y extensiones, incluyendo una presentación tipada y larepresentación de estructuras de datos. La segunda parte de esta tesis se centra en la interpretación computacional de la Lógicade Pruebas, o LP, via el isomorfismo de Curry-Howard. LP, dada a conocer por Artemov en 1995, es un refinamiento de la lógica modal en la cual la modalidad 2A es revisitada como [[t]]A, donde t es una expresión que testifica sobre la validez de A. Es aritméticamente correctay completa, puede realizar todos los teoremas de S4 y posee la capacidad de versar sobre suspropias pruebas (` A implica ` [[t]]A, para algún t). Nuestra contribución principal es unaformulación en Deducción Natural con buen comportamiento, desarrollada con el fin de develarlas metáforas computacionales que surgen de esta capacidad de reflexión de LP. Esta es laprimera formulación en Deducción Natural capaz de capturar a LP en su totalidad. Para esto,adoptamos la Deducción Natural Clásica de Parigot y la unimos al razonamiento hipotético. Como resultado, obtenemos una presentación en Deducción Natural de LP proposicional, parala cual se demuestran ciertas propiedades claves. Luego extendemos nuestro análisis al caso deprimer orden, presentando FOHLP, una extensión de primer orden de HLP. Nuestro punto departida es una reciente formulación de primer orden de LP, llamada FOLP, que goza de correcciónaritmética y tiene una semántica de demostrabilidad exacta (la completitud es inalcanzabledado que no es finitamente axiomatizable). Presentamos una formulación en Deducción Naturalllamada FOHLP, traducciones desde y hacia FOLP, una asignación de términos (cálculo lambda)y una prueba de terminación del proceso de normalización de derivaciones. Pattern matching is a basic building block on which functional programming depends, wherethe computation mechanism is based on finding a correspondence between the argument of afunction and an expression called \\pattern". It has also found its way into other programmingparadigms and has proved convenient for querying data in different formats, such as semistructureddata. In recognition of this, a recent effort is observed in which pattern matchingis studied in its purest form, namely by means of pattern calculi. These are lambda calculiwith sophisticated forms of pattern matching. The first part of this two part thesis proposes tocontribute to this effort by developing a combinatory logic for one such pattern calculus, namelyλP. We seek to mimic the computational process of λP where arguments can be matchedagainst arbitrary terms, without the use of variables. Two challenges must be met. On theone hand, dealing with bound variables in patterns. Indeed, an abstraction is a valid patternin λP. Here the standard combinatory logic will provide guidance. The second is computingthe counterpart, in the combinatory setting, of the substitution that is obtained in a successfulmatch. This requires devising rules that pull applications apart, so to speak. We proposea combinatory logic that serves this purpose and study its salient properties and extensionsincluding typed presentations and modeling data structures. In the second part, we are concerned with the computational interpretation of a particularmodal logic, the Logic of Proofs or LP, via the Curry-Howard isomorphism. LP, introduced by Artemov in 1995, is a refinement of modal logic in which the modality 2A is revisited as [[t]]Awhere t is an expression that bears witness to the validity of A. It enjoys arithmetical soundnessand completeness, can realize all S4 theorems and is capable of reecting its own proofs (` Aimplies ` [[t]]A, for some t). Esta es la primera formulación en Deducción Natural capaz decapturar a LP en su totalidad. Our main contribution is a well-behaved Natural Deductionpresentation, developed with the aim of unveiling the computational metaphors which arisefrom the reective capabilities of LP. This is the first Natural Deduction formulation capable ofproving all LP-theorems. For that, we adopt Parigot's Classical Natural Deduction and mergeit with a hypothetical reasoning which guide the construction of the inference schemes. As anoutcome we obtain a Natural Deduction presentation of propositional LP for which a number ofkey properties are shown to hold. We then extend our analysis to the first-order case, introducing FOHLP, a first-order extension of HLP. Our point of departure is a recent first-order formulationof LP, called FOLP, which enjoys arithmetical soundness and has an exact provability semantics (completeness is unattainable given that a complete FOLP is not finitely axiomatizable). Weprovide a Natural Deduction presentation dubbed FOHLP, mappings to and from FOLP, a termassignment (λ-calculus) and a proof of termination of normalisation of derivations. Fil: Steren, Gabriela. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2014-12-15 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_n5634_Steren

Ejemplares similares