Factorización de derivaciones a través de tipos intersección

Mostrar todas las versiones(3)

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

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Ciruelos Rodríguez, Gonzalo
Formato: Tesis de Grado
Lenguaje:Español
Publicado: 28 d
Materias:
CALCULO LAMBDA
TIPOS INTERSECCION
ESPACIO DE DERIVACION
RETICULADO
LAMBDA CALCULUS
INTERSECTION TYPES
DERIVATION SPACE
LATTICE
Acceso en línea:https://hdl.handle.net/20.500.12110/seminario_nCOM000445_CiruelosRodriguez
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id todo:seminario_nCOM000445_CiruelosRodriguez
record_format dspace
spelling todo:seminario_nCOM000445_CiruelosRodriguez2023-10-03T16:48:32Z Factorización de derivaciones a través de tipos intersección Factorizing Derivations via Intersection Types Ciruelos Rodríguez, Gonzalo CALCULO LAMBDA TIPOS INTERSECCION ESPACIO DE DERIVACION RETICULADO LAMBDA CALCULUS INTERSECTION TYPES DERIVATION SPACE LATTICE 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. 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. Fil: Ciruelos Rodríguez, Gonzalo. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 28 de junio de 2018 Tesis de Grado PDF Español info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar https://hdl.handle.net/20.500.12110/seminario_nCOM000445_CiruelosRodriguez
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
language Español
orig_language_str_mv Español
topic CALCULO LAMBDA
TIPOS INTERSECCION
ESPACIO DE DERIVACION
RETICULADO
LAMBDA CALCULUS
INTERSECTION TYPES
DERIVATION SPACE
LATTICE
spellingShingle CALCULO LAMBDA
TIPOS INTERSECCION
ESPACIO DE DERIVACION
RETICULADO
LAMBDA CALCULUS
INTERSECTION TYPES
DERIVATION SPACE
LATTICE
Ciruelos Rodríguez, Gonzalo
Factorización de derivaciones a través de tipos intersección
topic_facet CALCULO LAMBDA
TIPOS INTERSECCION
ESPACIO DE DERIVACION
RETICULADO
LAMBDA CALCULUS
INTERSECTION TYPES
DERIVATION SPACE
LATTICE
description 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.
format Tesis de Grado
author Ciruelos Rodríguez, Gonzalo
author_facet Ciruelos Rodríguez, Gonzalo
author_sort Ciruelos Rodríguez, Gonzalo
title Factorización de derivaciones a través de tipos intersección
title_short Factorización de derivaciones a través de tipos intersección
title_full Factorización de derivaciones a través de tipos intersección
title_fullStr Factorización de derivaciones a través de tipos intersección
title_full_unstemmed Factorización de derivaciones a través de tipos intersección
title_sort factorización de derivaciones a través de tipos intersección
publishDate 28 d
url https://hdl.handle.net/20.500.12110/seminario_nCOM000445_CiruelosRodriguez
work_keys_str_mv AT ciruelosrodriguezgonzalo factorizaciondederivacionesatravesdetiposinterseccion
AT ciruelosrodriguezgonzalo factorizingderivationsviaintersectiontypes
_version_ 1782030444817022976

Ejemplares similares