Catálogo de publicaciones - tesis
Título de Acceso Abierto
Dos temas en reescritura: combinadores para cálculos con patrones e isomorfismo de Curry-Howard para la Lógica de Pruebas
Gabriela Steren Eduardo Bonelli
publishedVersion.
Resumen/Descripción – provisto por el repositorio digital
Pattern 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.Palabras clave – provistas por el repositorio digital
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
Disponibilidad
| Institución detectada | Año de publicación | Navegá | Descargá | Solicitá |
|---|---|---|---|---|
| No requiere | 2014 | Biblioteca Digital (FCEN-UBA) (SNRD) |
|
Información
Tipo de recurso:
tesis
Idiomas de la publicación
- español castellano
País de edición
Argentina
Fecha de publicación
2014-12-15
Información sobre licencias CC
