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 con estos índices son invariantes con respecto a la conversión α , por lo que la comprobació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 la cantidad de aglutinantes que están dentro del alcance . entre esa ocurrencia y su ligante correspondiente. Los siguientes son algunos ejemplos:
Los índices de De Bruijn se usan comúnmente en sistemas de razonamiento de orden superior , como probadores de teoremas automatizados y sistemas de programación lógica . [2]
Formalmente, los términos λ ( M , N , ...) escritos con í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á dentro del alcance de al menos n ligantes (λ); de lo contrario es gratis . El sitio de enlace para una variable n es el enésimo enlazador que está 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 con otros términos. En la β-reducción (λ M ) N , por ejemplo, debemos
Después del paso 1, obtenemos el término λ 4 □ (λ 1 □), donde las variables que están destinadas a la sustitución 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, a saber, λ 5 1; el primer cuadro está debajo de un aglutinante, por lo que lo reemplazamos con λ 6 1 (que es λ 5 1 con las variables libres aumentadas en 1); el segundo está bajo dos ligantes, así que lo reemplazamos con λ 7 1. El resultado final es λ 3 (λ 6 1) (λ 1 (λ 7 1)).