En lógica matemática , el índice de Bruijn es una herramienta inventada por el matemático holandés Nicolaas Govert de Bruijn para representar términos del cálculo lambda sin nombrar las variables ligadas. [1] Los términos escritos utilizando 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 Bruijn es un número natural que representa una aparición de una variable en un término λ y denota el número de carpetas que están dentro del alcance entre esa ocurrencia y su carpeta correspondiente. Los siguientes son algunos ejemplos:
Los índices de De Bruijn se utilizan comúnmente en sistemas de razonamiento de orden superior, como los demostradores de teoremas automatizados y los sistemas de programación lógica . [2]
Formalmente, los términos λ ( M , N , ...) escritos utilizando índices de De Bruijn tienen la siguiente sintaxis (los paréntesis se permiten libremente):
donde n ( números naturales mayores que 0) son las variables. Una variable n está vinculada si está en el alcance de al menos n vinculantes (λ); de lo contrario es gratis . El sitio de unión para una variable n es el enésimo enlazador en el que se encuentra dentro del alcance , comenzando desde el enlazador más interno.
La operación más primitiva en términos λ es la sustitución : reemplazar variables libres en un término por otros términos. En la reducción β (λ M ) N , por ejemplo, debemos
Para ilustrar, considere la aplicación
que podría corresponder al siguiente término escrito en la notación habitual
Luego del paso 1, obtenemos el término λ 4 □ (λ 1 □), donde las variables que están destinadas a la sustitución se reemplazan por cajas. El paso 2 disminuye las variables libres, dando λ 3 □ (λ 1 □). Finalmente, en el paso 3, reemplazamos los cuadros con el argumento, a saber, λ 5 1; el primer cuadro está debajo de una carpeta, por lo que lo reemplazamos con λ 6 1 (que es λ 5 1 con las variables libres aumentadas en 1); el segundo está bajo dos carpetas, por lo que lo 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 1 . M 2 ..., donde M i es el reemplazo de la i -ésima variable libre. La operación creciente 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 aumentar las variables y se define por
Por ejemplo, ↑ 0 es la sustitución de identidad, lo que deja un término sin cambios. Una lista finita de términos M 1 . M 2 ... M n abrevia la sustitución M 1 . M 2 ... 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 1 y s 2 se escribe s 1 s 2 y se define por
satisfacer la propiedad
y la sustitución se define en los siguientes términos:
Los pasos descritos anteriormente para la reducción β se expresan de manera más concisa como:
Cuando se utiliza la representación estándar "nombrada" de términos λ, donde las variables se tratan como etiquetas o cadenas, se debe manejar explícitamente la conversión α al definir cualquier operación en los términos. En la práctica, esto resulta engorroso, ineficiente y, a menudo, propenso a errores. Por tanto, ha llevado a la búsqueda de diferentes representaciones de dichos términos. Por otro lado, la representación con nombre de los términos λ es más generalizada y puede ser más inmediatamente comprensible para otros porque a las variables se les pueden dar nombres descriptivos. Por lo tanto, incluso si un sistema utiliza índices de Bruijn internamente, presentará una interfaz de usuario con nombres.
Una forma alternativa de ver los índices de Bruijn es como niveles de Bruijn, que indexan las variables desde la parte inferior de la pila en lugar de desde la parte superior. Esto elimina la necesidad de reindexar variables libres, por ejemplo, cuando se debilita el contexto, mientras que los índices de Bruijn eliminan la necesidad de reindexar variables ligadas, por ejemplo, cuando se sustituye una expresión cerrada en otro contexto. [3]
Los índices de De Bruijn no son la única representación de términos λ que obvia el problema de la conversión α. Entre las representaciones con nombre, las técnicas nominales de Pitts y Gabbay son 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 mediante permutaciones variables. [4] Este enfoque lo adopta el paquete de tipo de datos nominal de Isabelle/HOL . [5]
Otra alternativa común es apelar a representaciones de orden superior donde el aglutinante λ se trata como una función verdadera. En tales representaciones, las cuestiones 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 prueba , a veces es deseable limitarse a representaciones de primer orden y tener la capacidad de nombrar o cambiar el nombre de 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 convención de variables de Barendregt [8] es una convención comúnmente utilizada en pruebas y definiciones donde se supone que:
En el contexto general de una definición inductiva, no es posible aplicar la conversión α según sea necesario para convertir una definición inductiva que usa la convención a una en la que no se usa la convención, porque una variable puede aparecer tanto en una posición vinculante como en una posición no vinculante. -posición vinculante en la norma. El principio de inducción se cumple si toda regla satisface las dos condiciones siguientes: [9]
![{\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}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0e2203824aea163db3b761d51dbb2cb2ccec6912)