Resumen:
Desde hace unos 20 años que distintos cálculos de sustituciones explícitas han dado diferentes resultados en la forma de imitar al λ-cálculo. Uno de los primeros, λσ, ha sido inspiración para muchos de ellos por su forma de componer sustituciones y por su forma de trabajar los índices de de Bruijn. Sin embargo, ningún cálculo derivado de éste logra combinar satisfactoriamente todas las buenas propiedades que se esperan de un cálculo de sustituciones explícitas: preservación de la normalización fuerte (PSN), simulación del λ-cálculo (Sim), meta confluencia (MC), etc. En un reciente trabajo de D. Kesner se presenta un cálculo derivado de λx que tiene todas estas propiedades. Parte fundamental de este cálculo es la eliminación de “basura” -sustituciones que no modifican el término a sustituir, que al componerse con otras sustituciones terminan generando más basura, resultando en términos con derivaciones infinitas que en el λ-cálculo tradicional son fuertemente normalizantes. En este trabajo presentamos λσgc, un cálculo basado en λσ, que resulta de agregar una regla que elimina sustituciones “basura”, y evita la composición y distribución de esta basura. Demostramos que este nuevo cálculo presenta las mismas propiedades que λσ. Además, demostramos que λσgc consigue incluir al término de Mellies en el conjunto de términos fuertemente normalizantes, aunque PSN para este cálculo sigue siendo una pregunta abierta. En el estudio de algunas propiedades del nuevo cálculo hemos desarrollado herramientas lógicas originales, que pueden servir a futuras extensiones de λσ, y hemos abierto y desarrollado la discusión sobre cómo evitar la basura en cálculos derivados de dicho cálculo.
Abstract:
For the last 20 years different calculi with explicit substitutions have been developed in order to imitate the λ-calculus, with diverse results. One of them, λσ, has been an inspiration to many of them, because of the way it composes substitutions, and the way it handles de Bruijn indices. However, no calculus derived from it is known to achieve all the good properties expected from a calculus with explicit substitutions: preservation of strong normalization (PSN), simulation of λ-calculus (Sim), metaconfluence (MC), etc. In a recent work, D. Kesner presents a new calculus obtained from λx with all these properties. To achieve this result, it does “garbage collection” -throw away substitutions that are not going to modify the term to substitute, whose composition with other substitutions ends up in the generation of more garbage, creating infinite derivations in terms which are strongly normalizing in traditional λ-calculus. In this work we present λσgc, a calculus based on λσ that performs garbage collection, avoids the distribution of garbage through the terms, and does not allow for the composition of garbage. We prove that this new calculus has the same properties as λσ. Moreover, we prove that λσgc includes the M`ellies term in the set of strongly normalizing terms. But PSN for this calculus remains an open question. In the study of some of the properties of the new calculus, we have developed some original logic tools. Future extensions of λσ can benefit from these ideas. Also, we have opened and advanced the discussion about how garbage can be avoided in calculi derived form λσ.
Citación:
---------- APA ----------
Ziliani, Luis Francisco. (2009). λσ gc : un cálculo basado en λσ con Garbage Collection. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000760_Ziliani
---------- CHICAGO ----------
Ziliani, Luis Francisco. "λσ gc : un cálculo basado en λσ con Garbage Collection". Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2009.https://hdl.handle.net/20.500.12110/seminario_nCOM000760_Ziliani
Estadísticas:
Descargas mensuales
Total de descargas desde :
https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000760_Ziliani.pdf
Distrubución geográfica
