Sustitución explícita
Un cálculo de sustituciones explícitas es una extensión del cálculo lambda en el que la sustitución se integra en el cálculo de la misma forma que la abstracción o la aplicación, mientras que en el cálculo lambda la sustitución es parte de la metateoría , que es decir, se define fuera de la teoría del cálculo lambda.
Principio
La idea que lleva a explicar las sustituciones surge del deseo de tratar la sustitución como una operación por derecho propio integrándola en la sintaxis y añadiendo un cierto número de reglas que distribuyen y aplican la sustitución y que forman parte de ella. del cálculo al igual que la reducción β es parte del cálculo lambda. El interés de integrar la sustitución en el cálculo es poder hablar de la sustitución tanto en términos de implantación, complejidad, eficiencia o estrategia de evaluación como en su relación con la β-reducción . Esto puede explicar el intercambio , la evaluación retrasada o perezosa o la evaluación inmediata. Una sustitución que aparece en un término se puede evaluar de inmediato o se puede posponer su evaluación, cuando sea necesario. Además, la evaluación de una sustitución se puede utilizar en varios lugares y solo requiere un cálculo ( compartir ).
Sintaxis rica
Para que el sistema formal pueda hablar al mismo tiempo de abstracción y aplicación, así como de sustitución, es necesario enriquecer la sintaxis del cálculo lambda con un operador de sustitución explícito. Hay dos formas de hacer esto, dependiendo de si está trabajando con variables explícitas o con índices de Bruijn .
- Si las variables son explícitas, agregamos un operador 〈x: = N〉 . En este caso, la notación P <x: = N> designa el operador de sustitución explícita aplica a P y medios que desea reemplazar x por N en P . Tenga en cuenta que en la expresión P <x: = N> , <x: = N> es un enlazador para x en P de la misma manera que λ es un enlazador para x en λx.P . Por supuesto, esto tiene un impacto en la noción de variable libre que debe ser libre para λ pero también para 〈x: = N〉 .
- Si se utilizan índices de Bruijn para codificar las variables, agregamos un operador [s] donde s es una sustitución. La notación M [s] significa que M es modificado por la sustitución s . En este caso, las sustituciones forman otro tipo de objeto. Son generados por operadores específicos /, ⇑ , ↑ , que se describen más adelante en este artículo.
Propiedades requeridas
Aquí hay algunas propiedades que queremos ver satisfechas por un sistema de sustituciones explícitas. En primer lugar, hay propiedades obligatorias.
- El sistema debe ser confluente en los términos cerrados , es decir, en los términos que no contienen variables libres.
- El sistema debe simular cada paso de la reducción β .
- El sistema restringido a sustituciones solas debe ser altamente normalizable , es decir, todas las reducciones que no contienen eliminación de β-redex deben terminar.
También hay propiedades opcionales que uno puede desear.
- Para definir las reglas introducimos variables ad hoc (distintas de las variables internas del sistema y del cálculo lambda), que pueden ser reemplazadas por cualquier término y que se denominan metavariables , formando así meta-términos . El sistema debe ser confluente en términos de meta .
- El sistema de sustituciones explícitas debería permitir componer sustituciones .
- El sistema de sustituciones explícitas debe preservar la fuerte estandarización . Esto significa que cualquier término fuertemente normalizable del cálculo lambda debería permanecer fuertemente normalizable cuando se sumerge en el cálculo de sustituciones explícitas.
-
El sistema de tipos de cálculo lambda se extiende y conserva sus características, como la fuerte normalización de los términos tipificables.
- El sistema debe ser simple , tanto en términos de número de operadores como de reglas, su complejidad y sus condiciones auxiliares.
Variantes
Hay varios cálculos de sustituciones explícitas. Esto se puede explicar de dos formas:
- Hay diferentes tipos de sintaxis : con variables explícitas o implícitas, con diferentes operadores,
- algunas propiedades mencionadas anteriormente son satisfechas por un sistema y no por otro. Un sistema de sustituciones explícitas hace un compromiso entre estas propiedades.
En general, los sistemas que confluyen en términos de meta no conservan una normalización fuerte y viceversa. Aquellos que satisfacen estas dos propiedades no son simples.
El cálculo de λx
El sistema λx usa nombres de variables explícitos y tiene cuatro reglas para el sistema de sustitución, además de una regla para eliminar β-redex y así simular β-reducción.
(b) : (λx.M) N → M⟨x: = N⟩
(xvI) : x⟨x: = P⟩ → P
(xvK) : x⟨y: = P⟩ → x (x ≠ y)
(xap) : (MN) ⟨x: = P⟩ → (M⟨x: = P⟩) (N⟨x: = P⟩)
(xab) : (λx.M) ⟨y: = P⟩ → λx. (M⟨y: = P⟩) (x ≠ y)
El sistema λx conserva la fuerte normalización . Podemos agregar la siguiente regla que generaliza y por lo tanto reemplaza la regla (xvK) .
(xgc) : M⟨x: = P⟩ → M (x∉var (M))
Resumen de reglas
- La regla (b) elimina un β-redex e introduce una sustitución explícita.
- En la regla (xvI) , el miembro de la izquierda se forma a partir de una sustitución asignada a una variable. Dado que la variable en cuestión es la misma que la variable de sustitución, la sustitución se elimina devolviendo el cuerpo de la misma.
- La regla (xvK) también tiene un miembro izquierdo formado a partir de una sustitución asignada a una variable, pero como las variables son diferentes, devolvemos la variable.
- La regla (xap) envía una sustitución en una aplicación. Una buena implantación debería hacer un intercambio.
- La regla (xab) introduce una sustitución en una abstracción.
- La regla (xvgc) evoca la espigan de las células , por lo tanto, las dos letras g y c . Aquí también el miembro de la izquierda está formado por una sustitución asignada a un término que no contiene la variable. La sustitución se elimina eliminándola, lo que hace desaparecer el cuerpo de sustitución y equivale a la recuperación de la memoria, es decir, a la recolección de células.
El cálculo λυ
El cálculo λυ utiliza índices de Bruijn. Por lo tanto, no hay más variables, sino solo metavariables. Ya no contiene variables ligadas, λυ es un sistema de reescritura de primer orden . Las adiciones sintácticas son las siguientes.
- La sustitución [N /] dice que en el término al que está asignado, el índice 0 debe ser reemplazado por N (regla (FVar) ). Pero dado que luego eliminamos el 0 , también debemos disminuir los otros índices (regla (RVar) ).
- El operador de elevación ( Lift en inglés), señaló ⇑ modifica una sustitución. Tiene en cuenta el hecho de que la sustitución aparece bajo λ. Por lo tanto, deja el índice 0 sin cambios (regla (FVarLift) ) y adjunta a cada índice un término cuyos índices contiene se incrementan mediante la sustitución de compensación (regla (RVarLift) ). En los índices funciona de la siguiente manera:
⇑ (s): 0 ↦ 0
1 ↦ s (0) [ ↑ ]
2 ↦ s (1) [ ↑ ]
⁞
n + 1 ↦ s (n) [ ↑ ]
⁞
- El cambio de sustitución ( Shift en inglés), escrito ↑ , incrementa los índices de un término (regla (VarShift) ).
(B) : (λ M) N → M [N /]
(Aplicación) : (MN) [s] → M [s] N [s]
(Lambda) : (λ M) [s] → λ (M [ ⇑ (s)])
(FVar) : 0 [M /] → M
(RVar) : n + 1 [M /] → n
(FVarLift) : 0 [ ⇑ (s)] → 0
(RVarLift) : n + 1 [ ⇑ (s)] → n [s] [ ↑ ]
(VarShift) : n [ ↑ ] → n + 1
El cálculo λυ conserva la fuerte normalización .
Resumen de reglas
Las primeras tres reglas corresponden a las reglas equivalentes de lambda-x, por ejemplo, la regla (B) elimina un beta-redex e introduce una sustitución explícita.
- La regla (FVAR) tiene el término el índice 0 y la sustitución de parte M / ella vuelve M .
- La regla (rvar) tiene el término el índice n + 1 y en parte sustituyendo M / , se decrementa el índice y se olvida M . Para justificar esta regla, debemos recordar que n + 1 proviene de debajo de una lambda que ha desaparecido.
- La regla (FVarLift) coloca un índice 0 y una operación de elevación frente a frente . 0 no cambia por el polipasto.
- La regla (RVarLift) tiene en cuenta el siguiente hecho: si aplicamos el levantamiento de una sustitución a un índice estrictamente positivo obtenemos un término resultante de la aplicación de la sustitución al índice anterior en el que todos los índices internos están escalonados, que es decir incrementado. Tenga en cuenta que en el lado derecho de este término hay dos aplicaciones sucesivas de sustituciones: a saber, la sustitución izada y el cambio.
- La regla (VarShift) realiza el cambio o incremento.
El cálculo de λσ
El cálculo de λσ es el cálculo original de Abadi, Cardelli, Curien y Lévy. Además de los operadores del cálculo λυ, este cálculo tiene
- una identificación constante para denotar la sustitución de identidad,
- un operador para agregar un término al comienzo de una sustitución y
- un operador de composición ∘ .
No hay operador ⇑, ni sustitución M / .
El cálculo de λσ
|
(Beta)
|
(λ M) N → M [N · id]
|
|---|
|
(Aplicación)
|
(MN) [s] → M [s] N [s]
|
|---|
|
(Abdominales)
|
(λ M) [s] → λ (M [0 · (s ∘ ↑)])
|
|---|
|
(Cerrado)
|
M [s] [t] → M [s ∘ t]
|
|---|
|
(VarId)
|
0 [Id] → 0
|
|---|
|
(VarCons)
|
0 [Sra.] → M
|
|---|
|
(IdL)
|
id ∘ s → s
|
|---|
|
(ShiftId)
|
↑ ∘ id → ↑
|
|---|
|
(ShiftCons)
|
↑ ∘ (M. S) → s
|
|---|
|
(AssEnv)
|
(s ∘ t) ∘ u → s ∘ (t ∘ u)
|
|---|
|
(MapEnv)
|
(M. S) ∘ t → M [t]. (s ∘ t)
|
|---|
Mientras que las sustituciones de λυ dicen qué asignar al índice 0 y sus avatares cuando se hunde en λ y cómo desplazar los índices distintos de 0, las sustituciones de λσ agrupan en una sola sustitución las asignaciones a todos los índices y para eso incluyen un operador de composición.
Historia
La idea de sustitución explícita se esboza en el prefacio del libro de Curry y Feys sobre lógica combinatoria , pero adquiere el estatus de un sistema real de reescritura de términos en el trabajo realizado por Bruijn en conexión con el sistema Automath . Por el contrario, el concepto y la terminología suelen atribuirse a Martín Abadi , Luca Cardelli , Curien y Lévy . En un artículo que será el primero de una larga lista, los autores introducen el cálculo λσ y muestran que el cálculo lambda debe estudiarse con mucha atención con respecto a la sustitución. Sin mecanismos sofisticados para compartir estructuras, las sustituciones pueden aumentar enormemente.
Notas y referencias
-
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)
-
M. Abadi, L. Cardelli, PL. Curien y JJ. Levy, sustituciones explícitas, Journal of Functional Programming 1, 4 (octubre de 1991), 375–416.
-
(en) Haskell Curry y Robert Feys , Combinatory Logic Volume I , Amsterdam, North-Holland Publishing Company,1958
-
NG de Bruijn: Un cálculo lambda libre de nombres 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.
Bibliografía
- Kristoffer Høgsbro Rose, Roel Bloo, Frédéric Lang: Sobre la sustitución explícita por nombres. J. Autom. Razonamiento 49 (2): 275-300 (2012)
- NG de Bruijn: Un cálculo lambda libre de nombres 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.
- Martín Abadi, Luca Cardelli, Pierre-Louis Curien y Jean-Jacques Lévy, “ Sustituciones explícitas ”, J. Funct. Programa , vol. 1, n o 4,1991, p. 375-416
- 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)
- Zine-El-Abidine Benaissa, Daniel Briaud, Pierre Lescanne, Jocelyne Rouyer-Degli: λυ, Un cálculo de sustituciones explícitas que conserva una fuerte normalización. J. Funct. Programa. 6 (5): 699 - 722 (1996); Versión online .
-
Pierre Lescanne : de Lambda-sigma a Lambda-upsilon un viaje a través de cálculos de sustituciones explícitas. POPL 1994: 60-69
Ver también