Tesis Doctorales > Documento

BúsquedaAUTORTÍTULOAÑOTEMA


Ver el documento (formato PDF)   Arbiser, Ariel.  "Sistemas y subsistemas de sustituciones explícitas"  (2005)
Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires
URL:
           

Resumen:
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.

Abstract:
This thesis is about some problems on rewriting theory and explicit substitution calculi. The main topic is the study of sub-calculi for several rewriting systems. After a biased introduction to rewriting, lambda-calculus and explicit substitution, we make a compatative study of the mail rewriting formalisms, identifying a hierarchy between them. As a first approach to new calculi, we address Revesz'lambda-calculus with names, involving four rewriting rules, with the particularity that it does not have any substitution at all. We show the relative soundness and the confluence. We also propose and study two versions using de Bruijn indices, proving that all these properties are preserved. We then move to perpetuality in the lambda v explicit substitution calculus, and study perpetual rewrite strategies, i.e. those strategies that preserve the possibility of infinite derivarions. We give as an application a set of deterministic inference rules wich characterize inductively the subsystem of strongly normalizing terms, and we present an effective perpetual reduction strategy for lambda v. Then we study different extensions of lambda v-calculus, with the addition of composition-like rules. Weak confluence on open terms is proved. As an application, a derived simplification of lambda v with a unique de Bruijn index can be given, which is a sub-calculus of the former and has the same properties. We show the weak normalization of the simply-typed lambda Se-calculus with open terms where abstractions are decorated with types, and meta-variables, de Bruijn indices and updating operators are decorated whit environments. The proof is based on the lambda omega e-calculus, a calculus wich over semi-open terms (i.e. those wich allow term variables but not substitution variables) is isomorphic to lambda Se, over open terms. This proof is strongly influenced by a previous proof of weak normalization for the simply-typed lambad sigma-calculus but with subtle differences which show that the two styles require different attention. Ferthermore, we give a new calculus, lambda omega'e, sub-calculus of lambda omega e, which handles a unique de Bruijn index, which is then closer to lambda sigma than lambda omega e. For lambda omega'e we also prove the weak normalization for typed semi-open terms. We present an extension of the lambda nu-calculus with a primitive case construct that propagares through abstractions like a head linear substitution before doing constructor substitution, and show that this way of decomposing pattern matching allows to recover the expressiveness of ML-style pattern matching. Then we prove that this system enjoys confluence using a semi-automatic "divide and conquer" technique by wich we determine all the pairs of commuting subsystens of the fornalism (considering all the possible combinations of the nine reduction rules). Finally, we prove a (weak) separation theorem for the whole formalism, using a separation technique inspired by the Bóhm-out technique. And, as another facet of sub-calculi exploration, we inverstigate the terms wich satisfy the property of expansion to pure terms, for lambda v and lambad S. We prove that these sets of terms are proper and non-recursive. As an application, we prove the impossibility id adequate mapping between certain pairs of calculi.

Registro:
Título : Sistemas y subsistemas de sustituciones explícitas     =     : Explicit substitution systems and subsystems
Autor : Arbiser, Ariel
Director : Ríos, Alejandro N.
Jurados : Kesner, D.  ; Szasz, N.  ; Ayala-Rincón, M.
Año : 2005
Editor : Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires
Filiación   
institucional : 
Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
Nombre del grado   
obtenido : 
Doctor de la Universidad de Buenos Aires en Ciencias de la Computación
Ubicación : Preservación - 003954
Idioma : Inglés
Area Temática : Computación /Lógica y Computabilidad
Palabras claves : CALCULO LAMBDA; CONFLUENCIA; CONMUTACION; CONSTRUCTOR; ESTRATEGIA; EXPANSION; INDICE DE BRUIJN; NORMALIZACION; PATRON; PERPETUALIDAD; REESCRITURA; SUB SISTEMA; SUSTITUCIONES EXPLICITAS; TIPADO; COMMUTATION; CONFLUENCE; CONSTRUCTOR; DE BRUIJN INDEX; EXPANSION; EXPLICIT SUBSTITUTION; LAMBDA-CALCULUS; NORMALIZATION; PATTERN; PERPETUALITY; REWRITING; STRATEGY; SUBSYSTEM; TYPING
URL al Documento : http://digital.bl.fcen.uba.ar/Download/Tesis/Tesis_3954_Arbiser.pdf
URL al Registro : http://digital.bl.fcen.uba.ar/gsdl-282/cgi-bin/library.cgi?a=d&c=tesis&d=Tesis_3954_Arbiser
     www.digital.bl.fcen.uba.ar
Biblioteca Central Dr. Luis Federico Leloir - Facultad de Ciencias Exactas y Naturales - Universidad de Buenos Aires
Intendente Güiraldes 2160 - Ciudad Universitaria - Pabellón II - C1428EGA - Tel. (54 11) 4789-9293 int 34