De Bruijn notation

Inom matematisk logik är De Bruijn-notationen en syntax för termer i λ-kalkylen som uppfanns av den holländska matematikern Nicolaas Govert de Bruijn . Det kan ses som en omkastning av den vanliga syntaxen för λ-kalkylen där argumentet i en applikation placeras bredvid dess motsvarande binder i funktionen istället för efter den senares kropp.

Formell definition

Termer ( $M,N,\ldots$ ) i De Bruijn-notationen är antingen variabler ( $v$ ), eller har ett av två vagnprefix . Abstraktionsvagnen , skriven $[v]$ , motsvarar det vanliga λ-bindemedlet i λ-kalkylen , och applikatorvagnen , skrivet $(M)$ , motsvarar argumentet i en tillämpning i λ-kalkylen.

M,N,...::=\ v\ |\ [v]\;M\ |\ (M)\;N

Termer i den traditionella syntaxen kan konverteras till De Bruijn-notationen genom att definiera en induktiv funktion ${\mathcal {I}}$ för vilken:

${\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 }}$

Alla operationer på λ-termer pendlar med avseende på ${\displaystyle {\mathcal {I}}}-$ översättningen. Till exempel, den vanliga β-reduktionen,

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

i De Bruijn-notationen är, förutsägbart,

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

En egenskap hos denna notation är att abstraktor- och applikatorvagnar av β-redex är parade som parenteser. Betrakta till exempel stadierna i β-reduktionen av termen ${\displaystyle (M)\;(N)\;[ u]\;(P)\;[v]\;[w]\;(Q)\;z} ,$ där redexerna är understrukna:

${\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}}$

Således, om man ser applikatorn som en öppen parenter (' ( ') och abstraktorn som en parentes (' ] '), så är mönstret i termen ovan ' (( ](]] '. De Bruijn kallade en applikator och dess motsvarande abstraktor i denna tolkning partner och vagnar utan partners ungkarlar En sekvens av vagnar, som han kallade ett segment , är välbalanserad om alla dess vagnar är partner.

Fördelar med De Bruijn-notationen

I ett välbalanserat segment kan de samarbetade vagnarna flyttas runt godtyckligt och så länge pariteten inte förstörs förblir innebörden av termen densamma. Till exempel, i exemplet ovan kan applikatorn $(M)$ föras till sin abstraktor $[w]$ , eller abstraktorn till applikatorn. Faktum är att alla kommutativa och permutativa omvandlingar på lambda-villkor kan enkelt beskrivas i termer av paritetsbevarande omordningar av samarbetade vagnar. Man får alltså en generaliserad konverteringsprimitiv för λ-termer i De Bruijn-notationen.

Flera egenskaper hos λ-termer som är svåra att ange och bevisa med den traditionella notationen uttrycks lätt i De Bruijn-notationen. Till exempel, i en typteoretisk miljö, kan man enkelt beräkna den kanoniska klassen av typer för en term i ett typningssammanhang, och återställa typkontrollproblemet till en att verifiera att den kontrollerade typen är en medlem av denna klass. De Bruijn notation har också visat sig vara användbar i calculi för explicit substitution i ren typ system .

Se även

Matematisk notation