Semántica dinámica de cálculos de sustituciones explicitas a distancia
Los cálculos de sustituciones explícitas son variantes del cálculo-λ en los que la operación de sustitución no se define a nivel del metalenguaje, sino con reglas de reescritura que la implementan. Nuestro principal objeto de estudio es un cálculo de sustituciones explícitas particular, el Linear Su...
Guardado en:
| Autor principal: | |
|---|---|
| Otros Autores: | |
| Formato: | Tesis doctoral publishedVersion |
| Lenguaje: | Español |
| Publicado: |
Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
2020
|
| Materias: | |
| Acceso en línea: | https://hdl.handle.net/20.500.12110/tesis_n6991_Barenbaum https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesis&d=tesis_n6991_Barenbaum_oai |
| Aporte de: |
| Sumario: | Los cálculos de sustituciones explícitas son variantes del cálculo-λ en los que la operación de sustitución no se define a nivel del metalenguaje, sino con reglas de reescritura que la implementan. Nuestro principal objeto de estudio es un cálculo de sustituciones explícitas particular, el Linear Substitution Calculus (LSC), definido por Accaoli y Kesner en 2010. Se caracteriza por el hecho de que las reglas de reescritura operan no localmente (a distancia). En esta tesis, en primer lugar, definimos máquinas abstractas que implementan estrategias de evaluacion en el LSC: call-by-name para evaluación débil y fuerte, call-by-value y call-by- need. Demostramos que dichas máquinas son correctas y preservan la complejidad temporal. En segundo lugar, denimos una extension de la estrategia de evaluación call-by-need en el LSC para evaluacion fuerte. Demostramos que la estrategia es completa con respecto a call-by- name, usando un sistema de tipos intersección no idempotente, y mostramos cómo extenderla para lidiar con pattern matching y recursión. Por último, estudiamos la teoría de residuos y familias de radicales en el LSC. Para ello denimos una variante del LSC con etiquetas de Levy, lo que nos permite demostrar que cumple con la propiedad de Finite Family Developments. Aplicamos esta propiedad para obtener resultados de optimalidad, estandarización y normalización de estrategias en el LSC, y generalizamos algunos de estos resultados al marco axiomático de Deterministic Family Structures. |
|---|