1. RODNA
  2. FCEN
  3. FCEN - Facultad de Ciencias Exactas y Naturales. UBA
Registro completo de metadatos
Campo DC Valor Lengua/Idioma
dc.provenanceFacultad de Ciencias Exactas y Naturales de la UBA-
dc.contributorBonelli, Eduardo-
dc.contributorSteren, Gabriela-
dc.creatorSteren, Gabriela-
dc.date.accessioned2018-05-04T22:07:18Z-
dc.date.accessioned2018-05-28T16:53:04Z-
dc.date.available2018-05-04T22:07:18Z-
dc.date.available2018-05-28T16:53:04Z-
dc.date.issued2014-12-15-
dc.identifier.urihttp://10.0.0.11:8080/jspui/handle/bnmm/75149-
dc.descriptionPattern matching es una herramienta fundamental de la programación funcional. Permite describir 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 demostrado su 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 en los que se introducen formas sofisticadas de pattern matching para estudiar sus fundamentos formales. La primera parte de esta tesis propone una contribución a este campo, desarrollando una lógica combinatoria para λP, un cálculo de patrones donde cualquier término puede ser un 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 es un 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 la sustitución obtenida ante un matching exitoso. Esto requiere la introducción de reglas capaces de 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 la representación de estructuras de datos. La segunda parte de esta tesis se centra en la interpretación computacional de la Lógica de 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 correcta y completa, puede realizar todos los teoremas de S4 y posee la capacidad de versar sobre sus propias pruebas (` A implica ` [[t]]A, para algún t). Nuestra contribución principal es una formulación en Deducción Natural con buen comportamiento, desarrollada con el fin de develar las metáforas computacionales que surgen de esta capacidad de reflexión de LP. Esta es la primera 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, para la cual se demuestran ciertas propiedades claves. Luego extendemos nuestro análisis al caso de primer orden, presentando FOHLP, una extensión de primer orden de HLP. Nuestro punto de partida es una reciente formulación de primer orden de LP, llamada FOLP, que goza de corrección aritmética y tiene una semántica de demostrabilidad exacta (la completitud es inalcanzable dado que no es finitamente axiomatizable). Presentamos una formulación en Deducción Natural llamada 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.-
dc.descriptionPattern matching is a basic building block on which functional programming depends, where the computation mechanism is based on finding a correspondence between the argument of a function and an expression called \pattern". It has also found its way into other programming paradigms and has proved convenient for querying data in different formats, such as semistructured data. In recognition of this, a recent effort is observed in which pattern matching is studied in its purest form, namely by means of pattern calculi. These are lambda calculi with sophisticated forms of pattern matching. The first part of this two part thesis proposes to contribute 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 matched against arbitrary terms, without the use of variables. Two challenges must be met. On the one hand, dealing with bound variables in patterns. Indeed, an abstraction is a valid pattern in λP. Here the standard combinatory logic will provide guidance. The second is computing the counterpart, in the combinatory setting, of the substitution that is obtained in a successful match. This requires devising rules that pull applications apart, so to speak. We propose a combinatory logic that serves this purpose and study its salient properties and extensions including typed presentations and modeling data structures. In the second part, we are concerned with the computational interpretation of a particular modal 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]]A where t is an expression that bears witness to the validity of A. It enjoys arithmetical soundness and completeness, can realize all S4 theorems and is capable of re ecting its own proofs (` A implies ` [[t]]A, for some t). Esta es la primera formulación en Deducción Natural capaz de capturar a LP en su totalidad. Our main contribution is a well-behaved Natural Deduction presentation, developed with the aim of unveiling the computational metaphors which arise from the re ective capabilities of LP. This is the first Natural Deduction formulation capable of proving all LP-theorems. For that, we adopt Parigot's Classical Natural Deduction and merge it with a hypothetical reasoning which guide the construction of the inference schemes. As an outcome we obtain a Natural Deduction presentation of propositional LP for which a number of key 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 formulation of 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). We provide a Natural Deduction presentation dubbed FOHLP, mappings to and from FOLP, a term assignment (λ-calculus) and a proof of termination of normalisation of derivations.-
dc.descriptionFil:Steren, Gabriela. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina.-
dc.formatapplication/pdf-
dc.languagespa-
dc.publisherFacultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires-
dc.rightsinfo:eu-repo/semantics/openAccess-
dc.rightshttp://creativecommons.org/licenses/by/2.5/ar-
dc.source.urihttp://digital.bl.fcen.uba.ar/gsdl-282/cgi-bin/library.cgi?a=d&c=tesis&d=Tesis_5634_Steren-
dc.subjectPATTERNS-
dc.subjectLAMBDA CALCULUS-
dc.subjectCOMBINATORY LOGIC-
dc.subjectMODAL LOGIC-
dc.subjectCURRY-HOWARD ISOMORPHISM-
dc.subjectLOGIC OF PROOFS-
dc.subjectPATRONES-
dc.subjectCALCULO LAMBDA-
dc.subjectLOGICA COMBINATORIA-
dc.subjectLOGICA MODAL-
dc.subjectISOMORFISMO DE CURRY-HOWARD-
dc.subjectLOGICA DE PRUEBAS-
dc.titleDos temas en reescritura: combinadores para cálculos con patrones e isomorfismo de Curry-Howard para la Lógica de Pruebas-
dc.titleTwo topics in rewriting: combinators for pattern calculi and Curry-Howard for the Logic of Proofs-
dc.typeinfo:eu-repo/semantics/doctoralThesis-
dc.typeinfo:ar-repo/semantics/tesis doctoral-
dc.typeinfo:eu-repo/semantics/publishedVersion-
Aparece en las colecciones: FCEN - Facultad de Ciencias Exactas y Naturales. UBA

Ficheros en este ítem:
No hay ficheros asociados a este ítem.
Mostrar el registro sencillo del ítem