Sustitución explícita

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 notoria fuente de errores. ^[1] El concepto ha aparecido en una gran cantidad de artículos publicados en campos muy diferentes, como en máquinas abstractas , lógica de predicados y computación simbólica .

Visión general

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 dice "M donde x será sustituida por N" . (El significado del nuevo término es el mismo que el lenguaje común let x: = N en M de muchos lenguajes de programación). Λx se puede escribir con las siguientes reglas de reescritura :

1. (λx.M) N → M⟨x: = N⟩
2. x⟨x: = N⟩ → N
3. x⟨y: = N⟩ → x (x ≠ y)
4. (M ₁ M ₂ ) ⟨x: = N⟩ → (M ₁ ⟨x: = N⟩) (M ₂ ⟨x: = N⟩)
5. (λx.M) ⟨y: = N⟩ → λx. (M⟨y: = N⟩) (x ≠ y yx no están libres en N)

Si bien hace que la sustitución sea explícita, esta formulación aún conserva la complejidad del cálculo lambda "convención de variables", que requiere un cambio de nombre arbitrario de las variables durante la reducción para garantizar que la condición "(x ≠ yyx no está libre en N)" en la última regla es siempre satisfecho antes de aplicar la regla. Por lo tanto, muchos cálculos de sustitución explícita evitan los nombres de variables por completo utilizando la denominada notación de índice de De Bruijn "sin nombre" .

Historia

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 la 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 le 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 lambdaDebe tener mucho cuidado 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 la corrección de las implementaciones puede 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 semánticas a propiedades sintácticas. Un ejemplo muy importante es el "lema de sustitución", que con la notación de λx se convierte en

• (M⟨x: = N⟩) ⟨y: = P⟩ = (M⟨y: = P⟩) ⟨x: = (N⟨y: = P⟩)⟩ (donde x ≠ y yx no están libres en P )

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 se normaliza fuertemente . 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]}

Ver también

• Lógica combinatoria
• Instancia de sustitución

Referencias

1. Clouston, Ranald; Bizjak, Aleš; Grathwohl, Hans; Birkedal, Lars (27 de abril de 2017). "El cálculo lambda protegido: programación y razonamiento con recursividad protegida para tipos coinductivos" (PDF) . Métodos lógicos en informática . 12 (3): 36. arXiv : 1606.09455 . doi : 10.2168 / LMCS-12 (3: 7) 2016 .
2. Curry, Haskell; Feys, Robert (1958). La lógica combinatoria Volumen I . Amsterdam: Compañía editorial de Holanda Septentrional.
3. NG de Bruijn: Un cálculo lambda sin nombre con facilidades para la definición interna de expresiones y segmentos. Universidad Tecnológica de Eindhoven, Países Bajos, Departamento de Matemáticas, (1978), (Informe TH), Número 78-WSK-03.
4. M. Abadi, L. Cardelli, PL. Curien y JJ. Levy, sustituciones explícitas, Journal of Functional Programming 1, 4 (octubre de 1991), 375–416.
5. PA. Melliès: Los cálculos lambda escritos con sustituciones explícitas no pueden terminar. TLCA 1995: 328–334
6. P. Lescanne, De λσ a λυ: un viaje a través de cálculos de sustituciones explícitas, POPL 1994, págs. 60–69.
7. KH Rose, Sustitución explícita - Tutorial y encuesta, BRICS LS-96-3, septiembre de 1996 ( ps.gz ).
8. Delia Kesner: una teoría de sustituciones explícitas con composición segura y completa. Métodos lógicos en informática 5 (3) (2009)