Notación de De Bruijn

En lógica matemática , la notación De Bruijn es una sintaxis para términos en el 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 enlace correspondiente en la función en lugar de después del cuerpo de este último.

Definición formal

Los términos ( ) en la notación de De Bruijn son variables ( ), o tienen uno de los dos prefijos wagon . El abstractor wagon , escrito , corresponde al λ-ligante habitual del cálculo λ , y el aplicador wagon , escrito , corresponde al argumento en una aplicación en el cálculo λ . ${\displaystyle M,N,\ldots }$ ${\displaystyle v}$ ${\displaystyle [v]}$ ${\displaystyle (M)}$

${\displaystyle M,N,...::=\ v\ |\ [v]\;M\ |\ (M)\;N}$

Los términos de la sintaxis tradicional se pueden convertir a la notación De Bruijn definiendo una función inductiva para la cual: ${\displaystyle {\mathcal {I}}}$

${\displaystyle {\begin{aligned}{\mathcal {I}}(v)&=v\\{\mathcal {I}}(\lambda v.\ M)&=[v]\;{\mathcal {I}}(M)\\{\mathcal {I}}(M\;N)&=({\mathcal {I}}(N)){\mathcal {I}}(M).\end{aligned}}}$

Todas las operaciones sobre términos λ conmutan con respecto a la traslación. Por ejemplo, la β-reducción habitual, ${\displaystyle {\mathcal {I}}}$

${\displaystyle (\lambda v.\ M)\;N\ \ \longrightarrow _{\beta }\ \ M[v:=N]}$

en la notación de De Bruijn es, como era de esperar,

${\displaystyle (N)\;[v]\;M\ \ \longrightarrow _{\beta }\ \ M[v:=N].}$

Una característica de esta notación es que los carros de abstracción y aplicación de β-redexes están emparejados como paréntesis. Por ejemplo, considere las etapas en la β-reducción del término , donde los rédex están subrayados: ^[2] ${\displaystyle (M)\;(N)\;[u]\;(P)\;[v]\;[w]\;(Q)\;z}$

${\displaystyle {\begin{aligned}(M)\;{\underline {(N)\;[u]}}\;(P)\;[v]\;[w]\;(Q)\;z&{\ \longrightarrow _{\beta }\ }(M)\;{\underline {(P[u:=N])\;[v]}}\;[w]\;(Q[u:=N])\;z\\&{\ \longrightarrow _{\beta }\ }{\underline {(M)\;[w]}}\;(Q[u:=N,v:=P[u:=N]])\;z\\&{\ \longrightarrow _{\beta }\ }(Q[u:=N,v:=P[u:=N],w:=M])\;z.\end{aligned}}}$

Por lo tanto, si se considera al aplicador como un paréntesis abierto (' (') y al abstractor como un corchete cerrado (' ]'), entonces el patrón en el término anterior es ' ((](]]'. De Bruijn llamó a un aplicador y a su abstractor correspondiente en esta interpretación socios , y a los 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, siempre que no se destruya la paridad, el significado del término permanece igual. Por ejemplo, en el ejemplo anterior, el aplicador puede llevarse a su abstractor , o el abstractor al aplicador. De hecho, todas las conversiones conmutativas y permutativas en términos lambda pueden describirse simplemente en términos de reordenamientos que preservan la paridad de los vagones asociados. De este modo, se obtiene una primitiva de conversión generalizada para términos λ en la notación de De Bruijn. ${\displaystyle (M)}$ ${\displaystyle [w]}$

Varias propiedades de los términos λ que son difíciles de enunciar y demostrar utilizando la notación tradicional se expresan fácilmente en la notación de De Bruijn. Por ejemplo, en un entorno de teoría de tipos , se puede calcular fácilmente la clase canónica de tipos para un término en un contexto de tipificación y reformular el problema de verificación de tipos como uno de verificación de que el tipo verificado es un miembro de esta clase. ^[3] También se ha demostrado que la notación de De Bruijn es útil en los cálculos para la sustitución explícita en sistemas de tipos puros . ^[4]

Véase también

• Notación matemática

Referencias

1. De Bruijn, Nicolaas Govert (1980). "Un estudio del proyecto AUTOMATH". En Hindley JR y Seldin JP (ed.). Para HB Curry: Ensayos sobre lógica combinatoria, cálculo lambda y formalismo . Academic Press . págs. 29–61. ISBN 978-0-12-349050-6.OCLC 6305265  .
2. Kamareddine, Fairouz (2001). "Revisión de la notación clásica y de De Bruijn para el cálculo λ y los sistemas de tipos puros". 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.
3. Kamareddine, Fairouz; Nederpelt, Rob (1996). "Una notación λ útil". Ciencias Informáticas Teóricas . 155 : 85–109. doi : 10.1016/0304-3975(95)00101-8 . ISSN  0304-3975.
4. De Leuw, B.-J. (1995). Generalizaciones en el cálculo λ y su teoría de tipos (tesis de maestría). Universidad de Glasgow ..