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 dentro del 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 en máquinas abstractas , lógica de predicados y computación simbólica .
Un ejemplo simple de un 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 se lee "M donde x será sustituida 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 la sustitución es explícita, 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 libre en N)" de la última regla siempre se cumpla antes de aplicar la regla. Por lo tanto, muchos cálculos de sustitución explícita evitan por completo los nombres de las variables mediante el uso de una notación de índice de De Bruijn denominada "sin nombre" .
Las sustituciones explícitas fueron esbozadas 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 seminal [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 la estructura, 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 sea altamente no trivial y la corrección de las implementaciones puede ser difícil de establecer. Una solución es hacer que las sustituciones sean 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 cambian de ser semánticas a ser sintácticas. Un ejemplo muy importante es el "lema de la 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ícita. [6] [7] [8]