Resumen:
Fundamental en el λ-cálculo es la relación de α-equivalencia, que agrupa en la misma clase a los términos que difieren sólo en los nombres de sus variables ligadas. Siendo una relación de equivalencia se tiene entonces, a partir del conjunto de términos, el conjunto cociente de las clases de α-equivalencia. Es habitualmente proclamado que todos los términos de una clase de a-equivalencia tienen idéntica interpretación en cualquier contexto del λ-cálculo, por lo cual deberían poder definirse las operaciones y relaciones sobre las clases. La α-equivalencia se define a partir de la sustitución, operación del metalenguaje definida sobre los términos. En este sentido, aparece sistemáticamente en la literatura una propiedad que garantiza que la sustitución está bien definida sobre las clases de α-equivalencia. Por otra parte están las relaciones de reducción, que modelan el concepto de cómputo y son por lo tanto esenciales al λ-cálculo. Estas relaciones se definen como la clausura contextual, transitiva y reflexiva de una noción (o axioma) de reducción, las cuales suelen considerarse como relaciones binarias arbitrarias en el conjunto de términos. En este trabajo sostenemos que, para considerar a una relación p como definida sobre las clases de α-equivalencia es necesario demostrar que tal relación y la a-equivalencia tienen la propiedad conmutativa del diamante (una variante de la propiedad del diamante), indagando además bajo qué condiciones una noción definida sobre términos generará una relación de reducción bien definida sobre clases. En este trabajo damos tres condiciones que son en conjunto suficientes para que una noción sea, en ese sentido, apropiada. Una de ellas es tener la propiedad conmutativa del diamante con la α-equivalencia, y las otras dos las hemos denominado "monotonía de variables libres" y A6 (obedeciendo esta última nominación a razones históricas). Finalmente también nos preguntamos si dichas condiciones resultan necesarias. Mostramos que si se elimina cualquiera de las tres condiciones aparecen nociones cuya relación correspondiente no está bien definida en el conjunto de clases de α-equivalencia; por otra parte, también damos ejemplos donde la noción no cumple alguna de las propiedades pero las relaciones derivadas sí resultan bien definidas sobre clases. En el desarrollo de este trabajo compilamos un marco teórico del λ-cálculo, inspirado en [HS86] pero enriquecido con algunos resultados que facilitan las demostraciones. Presentamos este marco en el capítulo 1. El capítulo 2 contiene el núcleo de nuestra investigación. Por último comentamos las lecturas realizadas en el capítulo 3, donde también comparamos distintas definiciones de α-equivalencia.
Abstract:
The α-equivalence relation is a fundamental notion in λ-calculus. It groups on the same class the terms that differ only in the names of its bound variables.Being an equivalence relation on the set of terms, it yields the quotient set composed of α-equivalence classes. It is usually claimed that all the terms of an α-equivalence class have identical interpretation in any context of the λ-calculus, thus it should be posible to define on classes the usual operations and relations of λ-calculus. The definition of α-equivalence is based on substitution, a meta-language operation defined on terms. In this direction, a property that guarantees that substitution is well-defined on classes appears systematically in the literature. On the other hand, there are reduction relations, which model the computation concept and are thus essential to the λ-calculus. These relations are defined as the contextual, transitive and reflexive closure ofaxioms of reduction, which are often considered as arbitrary binary relations on terms. In this work we hold that, before considering a relation p as defined on classes, it is necessary to prove that such relation and α-equivalence have the commuting diamond property (a variation of the diamond property), and we investigate also under which conditions an axiom defined on terms will generate a reduction relation that is well-defined on classes. We give three conditions that are together sufficient for an axiom to be, in this sense, adequate. One of these is to have the commuting diamond property with the α-equivalence, and the other two we have denominated "free variables monotonicity" and A6 (obeying this last name historical reasons). Finally, we also asked if these conditions are necessary. We show that if any of the three conditions is eliminated there appear axioms whose corresponding relation is not well-defined on classes; on the other hand, we also show examples where the axiom does not satisfy one of the properties but the derived relations are well-defined on classes. In the development of this work we compiled a theoretical framework of Acalculus, inspired by [HS86] but enriched with some results that facilitate the proofs. We present this framework in chapter 1. Chapter 2 contains the core of our research. Finally, in chapter 3 we comment on the literature we consulted, and we also compare different definitions of α-equivalence.
Citación:
---------- APA ----------
Lombardi, Carlos Alberto; Vetere, Enrique. (2002). Estudio de relaciones de reducción en el λ-cálculo puro. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000184_Lombardi
---------- CHICAGO ----------
Lombardi, Carlos Alberto; Vetere, Enrique. "Estudio de relaciones de reducción en el λ-cálculo puro". Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2002.https://hdl.handle.net/20.500.12110/seminario_nCOM000184_Lombardi
Estadísticas:
Descargas mensuales
Total de descargas desde :
https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000184_Lombardi.pdf
Distrubución geográfica
