En informática , se dice que los cálculos lambda tienen sustituciones explícitas si prestan especial atención a la formalización del proceso de sustitución . Esto contrasta con el cálculo lambda estándar donde las sustituciones se realizan mediante reducciones beta de una manera implícita que no se expresa en el cálculo; las condiciones de "frescura" en tales cálculos implícitos son una fuente notoria de errores. [1] El concepto ha aparecido en una gran cantidad de artículos publicados en campos bastante diferentes, como máquinas abstractas , lógica de predicados y computación simbólica .
Un ejemplo simple de cálculo lambda con sustitución explícita es "λx", que agrega una nueva forma de término al cálculo lambda , a saber, la forma M⟨x:=N⟩, que dice "M donde x será sustituido por N" . (El significado del nuevo término es el mismo que el modismo común let x:=N en M de muchos lenguajes de programación). λx se puede escribir con las siguientes reglas de reescritura :
Si bien hace explícita la sustitución, esta formulación aún conserva la complejidad de la "convención de variables" del cálculo lambda , que requiere un cambio de nombre arbitrario de las variables durante la reducción para garantizar que la condición "(x≠y y x no libres en N)" en la última regla sea Siempre satisfecho antes de aplicar la regla. Por lo tanto, muchos cálculos de sustitución explícita evitan por completo los nombres de variables utilizando la notación de índice de De Bruijn denominada "sin nombre" .
Las sustituciones explícitas se esbozaron en el prefacio del libro de Curry sobre lógica combinatoria [2] y surgieron de un "truco de implementación" utilizado, por ejemplo, por AUTOMATH , y se convirtieron en una teoría sintáctica respetable en el cálculo lambda y la teoría de reescritura . Aunque en realidad se originó con De Bruijn , [3] la idea de un cálculo específico donde las sustituciones son parte del lenguaje objeto, y no de la metateoría informal, se atribuye tradicionalmente a Abadi , Cardelli , Curien y Lévy. Su artículo fundamental [4] sobre el cálculo λσ explica que las implementaciones del cálculo lambda deben ser muy cuidadosas al tratar con sustituciones. Sin mecanismos sofisticados para compartir estructuras, las sustituciones pueden causar una explosión de tamaño y, por lo tanto, en la práctica, las sustituciones se retrasan y se registran explícitamente. Esto hace que la correspondencia entre la teoría y la implementación no sea trivial y que la exactitud de las implementaciones pueda ser difícil de establecer. Una solución es hacer que las sustituciones formen parte del cálculo, es decir, tener un cálculo de sustituciones explícitas.
Sin embargo, una vez que la sustitución se ha hecho explícita, las propiedades básicas de la sustitución pasan de ser propiedades semánticas a propiedades sintácticas. Un ejemplo más importante es el "lema de sustitución", que con la notación de λx se convierte en
Un contraejemplo sorprendente, debido a Melliès, [5] muestra que la forma en que esta regla está codificada en el cálculo original de sustituciones explícitas no es fuertemente normalizadora . A continuación, se describieron una multitud de cálculos que intentaban ofrecer el mejor compromiso entre las propiedades sintácticas de los cálculos de sustitución explícitos. [6] [7] [8]