Resumen:
El cálculo-λ es uno de los formalismos más utilizados para estudiar la computación desde un punto de vista abstracto. Por un lado, tiene aplicaciones prácticas en el diseño e implementación de lenguajes de programación funcionales y asistentes de demostración. Por otro, es una herramienta teórica casi indispensable para estudiar cualquier sistema que cuente con mecanismos de sustitución y ligado de variables. Las variantes débiles del cálculo-λ se caracterizan por prohibir la contracción de términos debajo de abstracciones. La relación de reducción débil propia de estas variantes es más cercana a la evaluación de los lenguajes de programación habituales, en los que no se reducen términos bajo lambdas durante la ejecución. Además, la reducción débil es interesante de por sí, en parte porque ciertas familias de propiedades, que no se cumplen en el cálculo-λ con la relación de reducción usual, se satisfacen si la relación se debilita. Otro motivo por el cual esta variante es interesante es que es una manera de relacionar la β-reducción en el cálculo-λ con la reducción en la lógica combinatoria. Un superdevelopment es una secuencia de pasos de reducción en la cual, en cada paso, sólo se permite contraer los residuos de los redexes que figuraban en el término inicial, y también algunos de los redexes creados. La razón principal que motiva el estudio de los superdevelopments es que pueden aplicarse como técnica para probar la confluencia del sistema en cuestión. En este trabajo, se estudian los superdevelopments para una variante confluente del cálculo-débil, introducida por Çaĝman y Hindley. Para ello, se estudia primero de qué maneras pueden crearse redexes en el cálculo-λ débil. Esto motiva dos caracterizaciones de superdevelopments para este cálculo: la primera definición se basa en una relación de reducción en un paso sobre términos decorados con etiquetas, y la segunda en un juicio de reducción simultánea definido inductivamente. A partir del cálculo etiquetado con el que se formulan los superdevelopments, se da en primer lugar una prueba de que son finitos. Una vez hecho esto, la parte central del trabajo consiste en el análisis y la comparación de las dos caracterizaciones de superdevelopments en el contexto del cálculo-λ débil, y en el estudio de la relación no obvia entre ellas, mostrando que las dos definiciones son esencialmente equivalentes.
Citación:
---------- APA ----------
Barenbaum, Pablo. (2010). Superdevelopments en el cálulo -Lambda débil. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000399_Barenbaum
---------- CHICAGO ----------
Barenbaum, Pablo. "Superdevelopments en el cálulo -Lambda débil". Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2010.https://hdl.handle.net/20.500.12110/seminario_nCOM000399_Barenbaum
Estadísticas:
Descargas mensuales
Total de descargas desde :
https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000399_Barenbaum.pdf
Distrubución geográfica