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
Otros Autores:	Barenbaum, Pablo
Formato:	Tesis de grado publishedVersion
Lenguaje:	Español
Publicado:	Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2018
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 http://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000445_CiruelosRodriguez_oai
Aporte de:	Repositorio Digital de la Universidad de Buenos Aires (UBA) de Universidad de Buenos Aires

id	I28-R145-seminario_nCOM000445_CiruelosRodriguez_oai
record_format	dspace
spelling	I28-R145-seminario_nCOM000445_CiruelosRodriguez_oai2023-08-29 Barenbaum, Pablo Ciruelos Rodríguez, Gonzalo 2018-06-28 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. application/pdf https://hdl.handle.net/20.500.12110/seminario_nCOM000445_CiruelosRodriguez spa Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar CALCULO LAMBDA TIPOS INTERSECCION ESPACIO DE DERIVACION RETICULADO LAMBDA CALCULUS INTERSECTION TYPES DERIVATION SPACE LATTICE Factorización de derivaciones a través de tipos intersección Factorizing Derivations via Intersection Types info:eu-repo/semantics/bachelorThesis info:ar-repo/semantics/tesis de grado info:eu-repo/semantics/publishedVersion http://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000445_CiruelosRodriguez_oai
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-145
collection	Repositorio Digital de la Universidad de Buenos Aires (UBA)
language	Español
orig_language_str_mv	spa
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.
author2	Barenbaum, Pablo
author_facet	Barenbaum, Pablo Ciruelos Rodríguez, Gonzalo
format	Tesis de grado Tesis de grado publishedVersion
author	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
publisher	Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
publishDate	2018
url	https://hdl.handle.net/20.500.12110/seminario_nCOM000445_CiruelosRodriguez http://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000445_CiruelosRodriguez_oai
work_keys_str_mv	AT ciruelosrodriguezgonzalo factorizaciondederivacionesatravesdetiposinterseccion AT ciruelosrodriguezgonzalo factorizingderivationsviaintersectiontypes
_version_	1782033785656705024

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

Ejemplares similares