En lógica matemática , el índice de De Bruijn es una herramienta inventada por el matemático holandés Nicolaas Govert de Bruijn para representar términos de 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 comprobación de 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 ligaduras que están en el alcance entre esa ocurrencia y su ligadura correspondiente. Los siguientes son algunos ejemplos:
Los índices de De Bruijn se utilizan comúnmente en sistemas de razonamiento de orden superior, como demostradores de teoremas automatizados y 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á ligada si está en el ámbito de al menos n ligantes (λ); de lo contrario, es libre . El sitio de enlace para una variable n es el n -ésimo ligante en cuyo ámbito está , comenzando por el ligante más interno.
La operación más primitiva sobre 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 ilustrarlo, consideremos la aplicación
que podría corresponder al siguiente término escrito en la notación habitual
Después del paso 1, obtenemos el término λ 4 □ (λ 1 □), donde las variables destinadas a la sustitución se reemplazan con cajas. El paso 2 decrementa las variables libres, dando λ 3 □ (λ 1 □). Finalmente, en el paso 3, reemplazamos las cajas con el argumento, es decir, λ 5 1; la primera caja está debajo de un binder, por lo que la reemplazamos con λ 6 1 (que es λ 5 1 con las variables libres aumentadas en 1); la segunda está debajo de dos binders, por lo 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 1 . M 2 ..., donde M i es el reemplazo de la i ésima variable libre. La operación de incremento en el paso 3 a veces se denomina desplazamiento y se escribe ↑ k donde k es un número natural que indica la cantidad a incrementar en las variables, y se define por
Por ejemplo, ↑ 0 es la sustitución de identidad, 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 términos siguientes:
Los pasos descritos anteriormente para la β-reducción se expresan de forma más concisa como:
Cuando se utiliza la representación estándar "con nombre" de los términos λ, donde las variables se tratan como etiquetas o cadenas, se debe manejar explícitamente la conversión α al definir cualquier operación sobre los términos. En la práctica, esto es complicado, ineficiente y, a menudo, propenso a errores. Por lo 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 las variables pueden recibir nombres descriptivos. Por lo tanto, incluso si un sistema utiliza índices de De Bruijn internamente, 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 parte superior. Esto elimina la necesidad de reindexar las variables libres, por ejemplo, cuando se debilita el contexto, mientras que los índices de De Bruijn eliminan la necesidad de reindexar las 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 evita el problema de la conversión α. Entre las representaciones nombradas, 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 reescribibles en él utilizando 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 en las que el λ-ligante 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 pruebas , a veces es deseable limitarse a representaciones de primer orden y tener la capacidad de nombrar o renombrar supuestos. El enfoque sin nombre local 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 α necesaria para convertir una definición inductiva que utiliza la convención en una en la que no se utiliza la convención, porque una variable puede aparecer tanto en una posición vinculante como en una posición no vinculante en la regla. El principio de inducción se cumple si cada 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)