Registro:
| Documento: | Tesis de Grado |
| Título: | Factorización de derivaciones a través de tipos intersección |
| Título alternativo: | Factorizing Derivations via Intersection Types |
| Autor: | Ciruelos Rodríguez, Gonzalo |
| Editor: | Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales |
| Publicación en la web: | 2023-04-02 |
| Fecha de defensa: | 2018-06-28 |
| Fecha en portada: | 28 de junio de 2018 |
| Grado Obtenido: | Grado |
| Título Obtenido: | Licenciado en Ciencias de la Computación |
| Director: | Barenbaum, Pablo |
| Jurado: | Díaz-Caro, Alejandro; Ríos, Alejandro |
| Idioma: | Español |
| Palabras clave: | CALCULO LAMBDA ; TIPOS INTERSECCION; ESPACIO DE DERIVACION; RETICULADOLAMBDA CALCULUS ; INTERSECTION TYPES; DERIVATION SPACE; LATTICE |
| Formato: | PDF |
| Handle: |
http://hdl.handle.net/20.500.12110/seminario_nCOM000445_CiruelosRodriguez |
| PDF: | https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000445_CiruelosRodriguez.pdf |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/seminario/document/seminario_nCOM000445_CiruelosRodriguez |
| Ubicación: | Dep.COM 000445 |
| Derechos de Acceso: | Esta obra puede ser leída, grabada y utilizada con fines de estudio, investigación y docencia. Es necesario el reconocimiento de autoría mediante la cita correspondiente. Ciruelos Rodríguez, Gonzalo. (2018). Factorización de derivaciones a través de tipos intersección. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de http://hdl.handle.net/20.500.12110/seminario_nCOM000445_CiruelosRodriguez |
Resumen:
En sistemas de tipos intersección no idempotentes típicos, la normalización de pruebas no es confluente. En este trabajo presentamos un sistema confluente de tipos intersección no idempotentes para el cálculo λ. Escribimos las derivaciones de tipos usando una sintaxis concisa de términos de prueba. El sistema goza de buenas propiedades: subject reduction, es fuertemente normalizante, y tiene una teoría de residuos muy regular. Establecemos una correspondencia con el cálculo lambda mediante teoremas de simulación. La maquinaria de los tipos intersección no idempotentes nos permite seguir el rastro del uso de los recursos necesarios para obtener una respuesta. En particular, induce una noción de basura: un cómputo es basura si no contribuye a hallar una respuesta. Usando estas nociones, mostramos que el espacio de derivaciones de un término λ puede ser factorizado usando una variante de la construcción de Grothendieck para semireticulados. Esto significa, en particular, que cualquier derivación del cálculo λ puede ser escrita de una única manera como un prefijo libre de basura, seguido de basura.
Abstract:
In typical non-idempotent intersection type systems, proof normalization is not confluent. In this work we introduce a confluent non-idempotent intersection type system for the λ-calculus. Typing derivations are presented using a concise proof term syntax. The system enjoys good properties: subject reduction, strong normalization, and a very regular theory of residuals. A correspondence with the λ-calculus is established by simulation theorems. The machinery of non-idempotent intersection types allows us to track the usage of resources required to obtain an answer. In particular, it induces a notion of garbage: a computation is garbage if it does not contribute to obtain an answer. Using these notions, we show that the derivation space of a λ-term may be factorized using a variant of the Grothendieck construction for semilattices. This means, in particular, that any derivation in the λ-calculus can be uniquely written as a garbage-free prefix followed by garbage.
Citación:
---------- APA ----------
Ciruelos Rodríguez, Gonzalo. (2018). Factorización de derivaciones a través de tipos intersección. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000445_CiruelosRodriguez
---------- CHICAGO ----------
Ciruelos Rodríguez, Gonzalo. "Factorización de derivaciones a través de tipos intersección". Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2018.https://hdl.handle.net/20.500.12110/seminario_nCOM000445_CiruelosRodriguez
Estadísticas:
Descargas mensuales
Total de descargas desde :
https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000445_CiruelosRodriguez.pdf
Distrubución geográfica
