Resumen:
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.
Citación:
---------- APA ----------
Viso, Andrés Ezequiel. (2010). Sistemas de tipos para λ-cálculo y Lógica Combinatoria. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000455_Viso
---------- CHICAGO ----------
Viso, Andrés Ezequiel. "Sistemas de tipos para λ-cálculo y Lógica Combinatoria". Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2010.https://hdl.handle.net/20.500.12110/seminario_nCOM000455_Viso
Estadísticas:
Descargas mensuales
Total de descargas desde :
https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000455_Viso.pdf
Distrubución geográfica
