Índice de De Bruijn

En lógica matemática , el índice de De Bruijn es una herramienta inventada por el matemático neerlandés Nicolaas Govert de Bruijn para representar términos del cálculo lambda sin nombrar las variables ligadas. ^{[ 1 ]} Los términos escritos usando estos índices son invariantes con respecto a la α-conversión , por lo que la verificación de la α-equivalencia es la misma que la de la igualdad sintáctica. Cada índice de De Bruijn es un número natural que representa una ocurrencia de una variable en un λ-término, y denota el número de ligadores que están en el ámbito entre esa ocurrencia y su ligador correspondiente. Los siguientes son algunos ejemplos:

• El término λ x . λ y . x , a veces llamado combinador K , se escribe como λ λ 2 con índices de De Bruijn. El ligador para la ocurrencia x es el segundo λ en el ámbito.
• El término λ x . λ y . λ z . x z ( y z ) (el combinador S ), con índices de De Bruijn, es λ λ λ 3 1 (2 1).
• El término λ z . (λ y . y (λ x . x )) (λ x . z x ) es λ (λ 1 (λ 1)) (λ 2 1). Véase la siguiente ilustración, donde los archivos están coloreados y las referencias se muestran con flechas.

Los índices de De Bruijn se utilizan comúnmente en sistemas de razonamiento de orden superior , como demostradores automáticos de teoremas y sistemas de programación lógica . ^{[ 2 ]}

Formalmente, los términos λ ( M , N , ...) escritos utilizando índices de De Bruijn tienen la siguiente sintaxis (se permiten paréntesis libremente):

M , N , ...  ::= n | M N | λ M

donde n —números naturales mayores que 0— son las variables. Una variable n está ligada si se encuentra dentro del ámbito de al menos n ligadores (λ); de lo contrario, es libre . El sitio de ligadura para una variable n es el n -ésimo ligador dentro de cuyo ámbito se encuentra , comenzando desde el ligador más interno.

La operación más primitiva sobre los términos λ es la sustitución : reemplazar las variables libres en un término con otros términos. En la β-reducción (λ M ) N , por ejemplo, debemos

1. encontrar las instancias de las variables n ₁ , n ₂ , ..., n _k en M que están acotadas por el λ en λ M ,
2. disminuir las variables libres de M para que coincidan con la eliminación del ligando λ externo, y
3. Reemplazar n ₁ , n ₂ , ..., n _k con N , incrementando adecuadamente las variables libres que aparecen en N cada vez, para que coincidan con el número de ligandos λ, bajo los cuales aparece la variable correspondiente cuando N sustituye a uno de los n _i .

Para ilustrarlo, consideremos la aplicación.

(λ λ 4 2 (λ 1 3)) (λ 5 1)

que podría corresponder al siguiente término escrito en la notación habitual

(λ x . λ y . z x (λ u . u x )) (λ x . w x ).

Después del paso 1, obtenemos el término λ 4 □ (λ 1 □), donde las ocurrencias de la variable que se está sustituyendo se reemplazan con casillas. El paso 2 decrementa las variables libres, dando λ 3 □ (λ 1 □). Finalmente, en el paso 3, reemplazamos las casillas con el argumento, es decir, λ 5 1; la primera casilla está bajo un ligador, así que la reemplazamos con λ 6 1 (que es λ 5 1 con las variables libres incrementadas en 1); la segunda está bajo dos ligadores, así que la reemplazamos con λ 7 1. El resultado final es λ 3 (λ 6 1) (λ 1 (λ 7 1)).

Formalmente, una sustitución es una lista ilimitada de términos, escrita M ₁ . M ₂ ..., donde M _i es el reemplazo para la i -ésima variable libre. La operación de incremento en el paso 3 a veces se llama desplazamiento y se escribe ↑ ^k donde k es un número natural que indica la cantidad a incrementar las variables, y se define por

${\displaystyle \uparrow ^{k}=(k+1).(k+2)....}$

Por ejemplo, ↑ ⁰ es la sustitución identidad, dejando un término sin cambios. Una lista finita de términos M ₁ . M ₂ ... M _n abrevia la sustitución M ₁ . M ₂ ... M _n .(n+1).(n+2)... dejando todas las variables mayores que n sin cambios. La aplicación de una sustitución s a un término M se escribe M [ s ]. La composición de dos sustituciones s ₁ y s ₂ se escribe s ₁ s ₂ y se define por

( M ₁ . M ₂ ...) s = M ₁ [ s ]. M ₂ [ s ]...

satisfaciendo la propiedad

M [ s ₁ s ₂ ] = ( M [ s ₁ ]) [ s ₂ ],

y la sustitución se define en los siguientes términos:

${\displaystyle {\begin{aligned}n[N_{1}\ldots N_{n}\ldots ]=&N_{n}\\(M_{1}\;M_{2})[s]=&(M_{1}[s])(M_{2}[s])\\(\lambda \;M)[s]=&\lambda \;(M[1.s'])\\&{\text{donde }}s'=s\uparrow ^{1}\end{aligned}}}$

Los pasos descritos anteriormente para la β-reducción se expresan, por lo tanto, de forma más concisa como:

(λ M ) N → _β M [ N .1.2.3...].

Al utilizar la representación estándar con nombre de los términos λ, donde las variables se tratan como etiquetas o cadenas, es necesario gestionar explícitamente la conversión α al definir cualquier operación sobre los términos. En la práctica, esto resulta engorroso, ineficiente y propenso a errores. Por consiguiente, se ha buscado una representación diferente de dichos términos. Por otro lado, la representación con nombre de los términos λ es más común y comprensible para otros usuarios, ya que las variables pueden tener nombres descriptivos. Así, incluso si un sistema utiliza internamente índices de De Bruijn, normalmente presentará una interfaz de usuario con nombres.

Una forma alternativa de ver los índices de De Bruijn es como niveles de De Bruijn, que indexan las variables desde la parte inferior de la pila en lugar de desde la superior. Esto elimina la necesidad de reindexar variables libres, por ejemplo, al debilitar el contexto, mientras que los índices de De Bruijn eliminan la necesidad de reindexar variables ligadas, por ejemplo, al sustituir una expresión cerrada en otro contexto. ^{[ 3 ]}

Los índices de De Bruijn no son la única representación de términos λ que evita el problema de la conversión α. Entre las representaciones con nombre, las técnicas nominales de Pitts y Gabbay constituyen un enfoque, donde la representación de un término λ se trata como una clase de equivalencia de todos los términos que se pueden reescribir a él mediante permutaciones de variables. ^{[ 4 ]} Este enfoque es adoptado por el paquete de tipos de datos nominales de Isabelle/HOL . ^{[ 5 ]}

Otra alternativa común es recurrir a representaciones de orden superior donde el ligador λ se trata como una función verdadera. En tales representaciones, los problemas de α-equivalencia, sustitución, etc., se identifican con las mismas operaciones en una metalógica .

Al razonar sobre las propiedades metateóricas de un sistema deductivo en un asistente de demostración , a veces es deseable limitarse a representaciones de primer orden y tener la capacidad de nombrar o renombrar supuestos. El enfoque localmente sin nombre utiliza una representación mixta de variables —índices de De Bruijn para variables ligadas y nombres para variables libres— que puede beneficiarse de la forma α-canónica de los términos indexados de De Bruijn cuando sea apropiado. ^{[ 6 ] [ 7 ]}

• La notación de De Bruijn para términos λ.
• La lógica combinatoria , una forma más esencial de eliminar los nombres de las variables.