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 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 la ocurrencia de una variable en un término λ y denota el número de ligantes que están dentro del alcance. entre esa ocurrencia y su correspondiente aglutinante. Los siguientes son algunos ejemplos:
- El término λ x . λ y . x , a veces llamado el combinador K , se escribe como λ λ 2 con índices de De Bruijn. El aglutinante para la ocurrencia x es el segundo λ en el alcance.
- 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). Consulte la siguiente ilustración, donde las carpetas están coloreadas y las referencias se muestran con flechas.
Los índices de De Bruijn se utilizan comúnmente en sistemas de razonamiento de orden superior , como probadores de teoremas automatizados y sistemas de programación lógica . [2]
Definicion formal
Formalmente, los términos λ ( M , N , ...) escritos usando í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 está en el alcance de al menos n ligantes (λ); de lo contrario, es gratis . El sitio de unión para una variable n es el n º aglutinante está en el alcance de, a partir del aglutinante más interna.
La operación más primitiva en términos de λ es la sustitución: reemplazar variables libres en un término con otros términos. En la β-reducción (λ M ) N , por ejemplo, debemos
- encuentre las instancias de las variables n 1 , n 2 , ..., n k en M que están limitadas por λ en λ M ,
- disminuir las variables libres de M para igualar la eliminación del aglutinante λ externo, y
- reemplace n 1 , n 2 , ..., n k con N , incrementando adecuadamente las variables libres que ocurren en N cada vez, para que coincida con el número de ligantes λ, bajo el cual la variable correspondiente ocurre cuando N sustituye a una de las n yo .
Para ilustrar, considere 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 variables que están destinadas a la sustitución se reemplazan con casillas. 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á debajo de dos aglutinantes, 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 reemplazos de términos para las variables libres, escrito M 1 . M 2 ..., donde M i es el reemplazo de la i- ésima variable libre. La operación de aumento en el paso 3 a veces se denomina desplazamiento y se escribe ↑ k donde k es un número natural que indica la cantidad para aumentar las variables; por ejemplo, ↑ 0 es la sustitución de identidad, dejando un término sin cambios.
La aplicación de una sustitución sa 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
- M [ s 1 s 2 ] = ( M [ s 1 ]) [ s 2 ].
Las reglas de aplicación son las siguientes:
Por lo tanto, los pasos descritos para la reducción β anterior se expresan de manera más concisa como:
- (λ M ) N → β M [ N .1.2.3 ...].
Alternativas a los índices de De Bruijn
Cuando se usa la representación estándar "nombrada" 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 en los términos. El convenio variable estándar [3] de Barendregt es uno de esos enfoques en el que se aplica la conversión α según sea necesario para garantizar que:
- las variables ligadas son distintas de las variables libres, y
- todos los vinculadores vinculan variables que aún no están en el alcance.
En la práctica, esto es engorroso, ineficaz 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 nombrada de los términos λ es más omnipresente y puede ser comprensible de manera más inmediata por otros porque las variables pueden recibir nombres descriptivos. Por lo tanto, incluso si un sistema usa índices De Bruijn internamente, presentará una interfaz de usuario con nombres.
Los índices de De Bruijn no son la única representación de los 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 reescribibles en él usando permutaciones variables. [4] Este enfoque es adoptado por el paquete de tipos de datos nominales de Isabelle / HOL . [5]
Otra alternativa común es apelar a representaciones de orden superior en las que 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 meta-ló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 cambiar el nombre de los 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 términos indexados de De Bruijn cuando sea apropiado. [6] [7]
Ver también
- La notación de De Bruijn para términos λ.
- Lógica combinatoria , una forma más esencial de eliminar nombres de variables.
Referencias
- ↑ de Bruijn, Nicolaas Govert (1972). "Notación de cálculo lambda con maniquíes sin nombre: una herramienta para la manipulación automática de fórmulas, con aplicación al teorema de Church-Rosser" (PDF) . Indagationes Mathematicae . 34 : 381–392. ISSN 0019-3577 .
- ^ Gabbay, Murdoch J .; Pitts, Andy M. (1999). "Un nuevo enfoque de la sintaxis abstracta que involucra a los aglutinantes". 14º Simposio Anual de IEEE sobre Lógica en Ciencias de la Computación . págs. 214–224. doi : 10.1109 / LICS.1999.782617 .
- ^ Barendregt, Henk P. (1984). El cálculo lambda: su sintaxis y semántica . Holanda Septentrional . ISBN 978-0-444-87508-2.
- ^ Pitts, Andy M. (2003). "Lógica nominal: una teoría de primer orden de nombres y vinculación". Información y Computación . 186 (2): 165-193. doi : 10.1016 / S0890-5401 (03) 00138-X . ISSN 0890-5401 .
- ^ "Sitio web de Nominal Isabelle" . Consultado el 28 de marzo de 2007 .
- ^ McBride, McKinna. No soy un número; Soy una variable libre (PDF) .
- ^ Aydemir, Chargueraud, Pierce, Pollack, Weirich. Metateoría formal de ingeniería .CS1 maint: varios nombres: lista de autores ( enlace )