En lógica matemática , la notación De Bruijn es una sintaxis para términos del cálculo λ inventada por el matemático holandés Nicolaas Govert de Bruijn . [1] Puede verse como una inversión de la sintaxis habitual para el cálculo λ donde el argumento en una aplicación se coloca al lado de su enlazador correspondiente en la función en lugar de después del cuerpo de esta última.
Definicion formal
Términos () en la notación de De Bruijn son variables (), o tener uno de los dos prefijos de vagón . El vagón abstractor , escrito, corresponde al aglutinante λ habitual del cálculo λ , y el carro aplicador , escrito, corresponde al argumento en una aplicación en el cálculo λ.
Los términos en la sintaxis tradicional se pueden convertir a la notación de De Bruijn definiendo una función inductiva para cual:
Todas las operaciones en términos λ se conmutan con respecto al traducción. Por ejemplo, la reducción β habitual,
en la notación de De Bruijn es, como era de esperar,
Una característica de esta notación es que los vagones de abstracción y aplicación de β-redexes están emparejados como paréntesis. Por ejemplo, considere las etapas de la reducción β del término, donde los redex están subrayados: [2]
Por lo tanto, si uno ve el aplicador como un par abierto (' (
') y el abstractor como un paréntesis cerrado (' ]
'), entonces el patrón en el término anterior es ' ((](]]
'. De Bruijn llamó a un aplicador y su correspondiente abstractor en esta interpretación socios , y vagones sin socios solteros . Una secuencia de vagones, a la que llamó segmento , está bien equilibrada si todos sus vagones están asociados.
Ventajas de la notación de De Bruijn
En un segmento bien equilibrado, los vagones asociados pueden moverse arbitrariamente y, mientras no se destruya la paridad, el significado del término permanece igual. Por ejemplo, en el ejemplo anterior, el aplicador se puede llevar a su abstractor , o del abstractor al aplicador. De hecho, todas las conversiones conmutativas y permutativas en términos lambda pueden describirse simplemente en términos de reordenamientos de vagones asociados que preservan la paridad. Se obtiene así una primitiva de conversión generalizada para términos λ en la notación de De Bruijn.
Varias propiedades de los términos λ que son difíciles de enunciar y probar usando la notación tradicional se expresan fácilmente en la notación de De Bruijn. Por ejemplo, en un tipo de teoría de ajuste, se puede calcular fácilmente la clase canónica de tipos para un término en un contexto mecanografía, y repetir la comprobación de tipos problema a uno de la verificación de que el tipo comprobado es un miembro de esta clase. [3] También se ha demostrado que la notación de De Bruijn es útil en cálculos para la sustitución explícita en sistemas de tipos puros . [4]
Ver también
Referencias
- ^ De Bruijn, Nicolaas Govert (1980). "Una encuesta del proyecto AUTOMATH". En Hindley JR y Seldin JP (ed.). Para HB Curry: Ensayos sobre lógica combinatoria, cálculo lambda y formalismo . Prensa académica . págs. 29–61. ISBN 978-0-12-349050-6. OCLC 6305265 .
- ^ Kamareddine, Fairouz (2001). "Revisión de la notación clásica y de De Bruijn para sistemas de tipo puro y cálculo λ". Lógica y Computación . 11 (3): 363–394. CiteSeerX 10.1.1.29.3756 . doi : 10.1093 / logcom / 11.3.363 . ISSN 0955-792X . El ejemplo es de la página 384.
- ^ Kamareddine, Fairouz; Nederpelt, Rob (1996). "Una notación λ útil". Informática Teórica . 155 : 85-109. doi : 10.1016 / 0304-3975 (95) 00101-8 . ISSN 0304-3975 .
- ^ De Leuw, B.-J. (1995). "Generalizaciones en el cálculo λ y su teoría de tipos". Tesis de Maestría, Universidad de Glasgow . Cite journal requiere
|journal=
( ayuda ).