Sistemas de tipos para λ-cálculo y Lógica Combinatoria

Mostrar todas las versiones(3)

El λ-cálculo puede verse como un lenguaje de programación universal en el que las funciones son “ciudadanos de primera clase”. Este lenguaje puede representar todas las funciones computables. Resulta de especial interés el estudio de los sistemas tipados. Los tipos permiten una clasificación o “estr...

Descripción completa

Detalles Bibliográficos
Autor principal: Viso, Andrés Ezequiel
Otros Autores: Arbiser, Ariel
Formato: Tesis de grado publishedVersion
Lenguaje:Español
Publicado: Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2010
Acceso en línea:https://hdl.handle.net/20.500.12110/seminario_nCOM000455_Viso
https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000455_Viso_oai
Aporte de:
Repositorio Digital de la Universidad de Buenos Aires (UBA) de Universidad de Buenos Aires
id I28-R145-seminario_nCOM000455_Viso_oai
record_format dspace
spelling I28-R145-seminario_nCOM000455_Viso_oai2024-12-17 Arbiser, Ariel Viso, Andrés Ezequiel 2010-02-23 El λ-cálculo puede verse como un lenguaje de programación universal en el que las funciones son “ciudadanos de primera clase”. Este lenguaje puede representar todas las funciones computables. Resulta de especial interés el estudio de los sistemas tipados. Los tipos permiten una clasificación o “estratificación” del universo de valores y expresiones, en la cual se basan los lenguajes de programación modernos para la rápida detección del uso inapropiado de funciones, métodos, etc. Como una formulación alternativa del λ-cálculo surge la Lógica Combinatoria, que es un sistema de reescritura en cierto sentido más simple pero sin embargo igualmente expresivo. Y del mismo modo que para el λ-cálculo, existen formulaciones de Lógica Combinatoria tipada. En esta tesis se dan pruebas de consistencia para distintas versiones del λ-cálculo tipado. Para esto se plantean métodos de demostración puramente sintácticos, basados en la noción de variable positiva. Estas pruebas son comparadas con otras existentes en la literatura para algunos de los sistemas de tipos analizados. Se estudian las ventajas y limitaciones del método propuesto, identificando sistemas para los cuales éste no resulta aplicable, y sobre algunos de ellos se da una demostración adecuada. Al mismo tiempo, se estudia la Lógica Combinatoria y sus variantes tipadas con el fin de definir un sistema de tipos de segundo orden. Se consideran diferentes opciones para extender el sistema de tipos simples de Curry. El sistema obtenido reshttps://catalogo-intra.exactas.uba.ar/cgi-bin/koha/cataloguing/addbiblio.pl?biblionumber=101824#tab6XXulta equivalente al sistema de tipos polimórficos Fη del λ-cálculo, presentado por Mitchell. Fil: Viso, Andrés Ezequiel. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. application/pdf https://hdl.handle.net/20.500.12110/seminario_nCOM000455_Viso 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 Sistemas de tipos para λ-cálculo y Lógica Combinatoria info:eu-repo/semantics/bachelorThesis info:ar-repo/semantics/tesis de grado info:eu-repo/semantics/publishedVersion https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000455_Viso_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
description El λ-cálculo puede verse como un lenguaje de programación universal en el que las funciones son “ciudadanos de primera clase”. Este lenguaje puede representar todas las funciones computables. Resulta de especial interés el estudio de los sistemas tipados. Los tipos permiten una clasificación o “estratificación” del universo de valores y expresiones, en la cual se basan los lenguajes de programación modernos para la rápida detección del uso inapropiado de funciones, métodos, etc. Como una formulación alternativa del λ-cálculo surge la Lógica Combinatoria, que es un sistema de reescritura en cierto sentido más simple pero sin embargo igualmente expresivo. Y del mismo modo que para el λ-cálculo, existen formulaciones de Lógica Combinatoria tipada. En esta tesis se dan pruebas de consistencia para distintas versiones del λ-cálculo tipado. Para esto se plantean métodos de demostración puramente sintácticos, basados en la noción de variable positiva. Estas pruebas son comparadas con otras existentes en la literatura para algunos de los sistemas de tipos analizados. Se estudian las ventajas y limitaciones del método propuesto, identificando sistemas para los cuales éste no resulta aplicable, y sobre algunos de ellos se da una demostración adecuada. Al mismo tiempo, se estudia la Lógica Combinatoria y sus variantes tipadas con el fin de definir un sistema de tipos de segundo orden. Se consideran diferentes opciones para extender el sistema de tipos simples de Curry. El sistema obtenido reshttps://catalogo-intra.exactas.uba.ar/cgi-bin/koha/cataloguing/addbiblio.pl?biblionumber=101824#tab6XXulta equivalente al sistema de tipos polimórficos Fη del λ-cálculo, presentado por Mitchell.
author2 Arbiser, Ariel
author_facet Arbiser, Ariel
Viso, Andrés Ezequiel
format Tesis de grado
Tesis de grado
publishedVersion
author Viso, Andrés Ezequiel
spellingShingle Viso, Andrés Ezequiel
Sistemas de tipos para λ-cálculo y Lógica Combinatoria
author_sort Viso, Andrés Ezequiel
title Sistemas de tipos para λ-cálculo y Lógica Combinatoria
title_short Sistemas de tipos para λ-cálculo y Lógica Combinatoria
title_full Sistemas de tipos para λ-cálculo y Lógica Combinatoria
title_fullStr Sistemas de tipos para λ-cálculo y Lógica Combinatoria
title_full_unstemmed Sistemas de tipos para λ-cálculo y Lógica Combinatoria
title_sort sistemas de tipos para λ-cálculo y lógica combinatoria
publisher Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
publishDate 2010
url https://hdl.handle.net/20.500.12110/seminario_nCOM000455_Viso
https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000455_Viso_oai
work_keys_str_mv AT visoandresezequiel sistemasdetiposparalcalculoylogicacombinatoria
_version_ 1824952577448476672

Ejemplares similares