Catálogo de publicaciones - tesis
Título de Acceso Abierto
Sistemas y subsistemas de sustituciones explícitas
Ariel Arbiser Alejandro N. Ríos
publishedVersion.
Resumen/Descripción – provisto por el repositorio digital
Esta tesis trata acerca de alguinos problemas en la teoría de reescritura y cálculos con sustituciónes explícitas. El tema principal es el estudio de sub cálculos de algunos sistemas de reescritura. Luego de una introducción sesgada a la reescritura, el cálculo lamba y las sustituciónes explícitas, hacemos un estudio comparativo de los principales formalismos de la reescritura, identificando una jerarquía entre éstos. Como primer aproximación a nuevos cálculos, estudiamos el cálculo lambda con nombres de Revesz, que utiliza cuatro reglas de reescriotura, con la particularidad de que no cuenta con sustirución alguna. Se prueba la correctitud relativa y la confluencia. También se proponen y se estudian dos versiones que usan índices de de Bruijn, y se prueba que estas dos propiedades se preservan. Luego pasamos a la perpetualidad en el cálculo de sustituciónes explícitas lambda v y estudiamos estrategias de reducción perpertias, i.e. aquellas que preservan la posibilidad de derivaciónes infinitas. Se da como una aplicación un conjunto de reglas de inferencia determinísticas que caracterizan inductivamente el sub sistema de los términos fuertemente normalizantes, y presentamos una estrategia de reducción perpetia efectiva para lambda v. A continuación se estudian distintas extensiones del cálculo lambda v, con reglas al estilo de las de composición. Se prueba la confluencia débil sobre términos abiertos. Como aplicación de lo anterior, se puede dar un cálculo simplificado, derivado de lambda v, que usa un solo índice de de Bruijn, el cual es un sub cálculo del anterior y con las mismas propiedades. Se demuestra luego la normalización débil del cálculo lambda Se simplemente tipado sobre términos abiertos, en donde las abstracciones se decoran con tipos, y las meta variables, índices de de Bruijn y operadores de actualización se decoran con contextos. La prueba se basa en el cálculo Lambda omega e, que sobre términos semi-abiertos (i.e. aquellos que admiten variables de término pero no de sustitución) es isomorfo a Lambda Se sobre términos abiertos. Esta prueba está fuertemente influenciada por otra previa de normalización débil para el cálculo lambda sigma simplemente tipado pero con diferencias substanciales que indican que los dos estilos requieren distinto tratamiento. Además, introducimos el cálculo lambda omega e, sub cálculo de lambda omega e, el cual usa sólo un índice de de Bruijn, con lo que es más cercano a lambda sigma que lambda omega e. Para lambda omega'e tipado probamos también la normalización débil sobre términos tipados semi-abiertos. Presentamos una extensión del cálculo lambda (nu) que incluye un constructor de casos primitivo que se propaga a través de las abstracciónes como una sustitución lineal de cabeza antes de actuar sobre los constructores, y probamos que este modo de descomposición del apareamiento de patrones permite recuperar la expresividad del estilo de los patrones de ML. Se demuestra que este sistema satisfase confluencia, usando una técnica de "dividir y conquistar" semi automática por al cual se determinan todo los pares de sub sistemas de este cálculo que conmutan (considerando todas las combinaciones de las nueve reglas de reducción). Finalmente, se prueba un teorema de separación (débil) para todo el formalismo, usando una técnica de separación inspirada en la técnica Böhm-out. Por último, como otra faceta de exploración de sub cálculos, analizamos los términos que se satisfacen la propiedad de expandir a términos puros, para lambda v y lambda S. Probamos que estos conjuntos de términos con propios yu no recursivos. Como aplicación, se prueba la imposibilidad de mapeos adecuados entre ciertos pares de cálculos.Palabras clave – provistas por el repositorio digital
CALCULO LAMBDA; CONFLUENCIA; CONMUTACION; CONSTRUCTOR; ESTRATEGIA; EXPANSION; INDICE DE BRUIJN; NORMALIZACION; PATRON; PERPETUALIDAD; REESCRITURA; SUB SISTEMA; SUSTITUCIONES EXPLICITAS; TIPADO; COMMUTATION; CONFLUENCE; DE BRUIJN INDEX; EXPLICIT SUBSTITUTION; LAMBDA-CALCULUS; NORMALIZATION; PATTERN; PERPETUALITY; REWRITING; STRATEGY; SUBSYSTEM; TYPING
Disponibilidad
| Institución detectada | Año de publicación | Navegá | Descargá | Solicitá |
|---|---|---|---|---|
| No requiere | 2005 | 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
2005
Información sobre licencias CC
