De Bruijn index

Den här artikeln handlar om en metod för att undvika att namnge bundna variabler i lambda-kalkyl. För en alternativ syntax för lambda-uttryck, se De Bruijn-notation .

Inom matematisk logik är De Bruijn-indexet ett verktyg som uppfanns av den holländska matematikern Nicolaas Govert de Bruijn för att representera termer av lambda-kalkyl utan att namnge de bundna variablerna. Termer skrivna med dessa index är oföränderliga med avseende på α-konvertering , så kontrollen för α-ekvivalens är densamma som den för syntaktisk likhet. Varje De Bruijn-index är ett naturligt tal som representerar en förekomst av en variabel i en λ-term, och anger antalet bindemedel som ligger i omfånget mellan den förekomsten och dess motsvarande bindemedel. Följande är några exempel:

• Termen λ x . λ y . x , ibland kallad K-kombinatorn , skrivs som λ λ 2 med De Bruijn-index. Bindemedlet för förekomsten x är den andra λ i omfattning.
• Termen λ x . λ y . λz . _ xz ( yz ) ( S -kombinatorn ), med De Bruijn-index, är λ λ λ 3 1 (2 1) .
• Termen λ z . (X y . y (X x . x )) (X x . zx ) är X (X 1 (λ 1)) (X 2 1) . Se följande illustration, där pärmarna är färgade och referenserna visas med pilar.

De Bruijn-index används ofta i resonemangssystem av högre ordning som automatiserade satsprovare och logiska programmeringssystem.

Formell definition

Formellt har λ-termer ( M , N , ...) skrivna med De Bruijn-index följande syntax (parenteser tillåtna fritt):

M , N , ... ::= n | M N | λ M

där n — naturliga tal större än 0 — är variablerna. En variabel n är bunden om den är inom ramen för minst n bindare (λ); annars är det gratis . Bindningsstället för en variabel n är det n :te bindemedlet som det är inom ramen för , utgående från det innersta bindemedlet.

Den mest primitiva operationen på λ-termer är substitution : att ersätta fria variabler i en term med andra termer. I β-reduktionen (λ M ) N måste vi till exempel

1. hitta instanserna av variablerna n ₁ , n ₂ , ..., n _k i M som är bundna av λ i λ M ,
2. minska de fria variablerna för M för att matcha avlägsnandet av det yttre λ-bindemedlet, och
3. ersätt n ₁ , n ₂ , ..., n _k med N , lämpligt öka de fria variablerna som förekommer i N varje gång, för att matcha antalet λ-bindare, under vilka den motsvarande variabeln uppträder när N ersätter en av n _jag .

För att illustrera, överväg ansökan

(λ λ 4 2 (λ 1 3)) (λ 5 1)

som kan motsvara följande term skriven i den vanliga notationen

( Ax . Xy.zx ( Au.ux ) ) ( Xx.wx ) . _ _ _ _ _ _

Efter steg 1 får vi termen λ 4 □ (λ 1 □), där de variabler som är avsedda för substitution ersätts med rutor. Steg 2 minskar de fria variablerna, vilket ger λ 3 □ (λ 1 □). Slutligen, i steg 3, ersätter vi rutorna med argumentet, nämligen λ 5 1; den första rutan är under en bindemedel, så vi ersätter den med λ 6 1 (vilket är λ 5 1 med de fria variablerna ökade med 1); den andra är under två bindemedel, så vi ersätter den med λ 7 1. Slutresultatet är λ 3 (λ 6 1) (λ 1 (λ 7 1)).

Formellt är en substitution en obegränsad lista med termer, skriven M ₁ . M ₂ ..., där M _i är ersättningen för den i :te fria variabeln. Den ökande operationen i steg 3 kallas ibland shift och skrivs ↑ ^k där k är ett naturligt tal som anger mängden för att öka variablerna, och definieras av

$\uparrow ^{k}=(k+1).(k+2)....$

⁰ Till exempel är ↑ identitetssubstitutionen, vilket lämnar en term oförändrad. En ändlig lista med termer M ₁ . M ₂ ... M _n förkortar substitutionen M ₁ . M ₂ ... M _n .(n+1).(n+2)... lämnar alla variabler större än n oförändrade. Tillämpningen av en substitution s på en term M skrivs M [ s ]. Sammansättningen av två substitutioner s ₁ och s ₂ skrivs s ₁ s ₂ och definieras av

( Mi. M2 ... ) s = Mi _[ s ] _{. _} _ M ₂ [ s ]...

tillfredsställer fastigheten

M [ s ₁ s ₂ ] = ( M [ s ₁ ]) [ s ₂ ],

och substitution definieras på följande villkor:

${\begin{aligned}n[N_{1}\ldots N_{n}\ldots ]=&N_{n}\\(M_{1}\;M_ {2})[s]=&(M_{1}[s])(M_{2}[s])\\(\lambda \;M)[s]=&\lambda \;(M[1. s'])\\&{\text{där }}s'=s\uparrow ^{1}\end{aligned}}$

De steg som beskrivs för β-reduktionen ovan är alltså mer kortfattat uttryckta som:

( AM ) N → _pM [ N ] .

Alternativ till De Bruijn-index

När man använder standardrepresentationen "namngiven" av λ-termer, där variabler behandlas som etiketter eller strängar, måste man explicit hantera α-konvertering när man definierar en operation på termerna. I praktiken är detta besvärligt, ineffektivt och ofta felbenäget. Det har därför lett till sökandet efter olika representationer av sådana termer. Å andra sidan är den namngivna representationen av λ-termer mer genomgripande och kan vara mer omedelbart förståelig av andra eftersom variablerna kan ges beskrivande namn. Således, även om ett system använder De Bruijn-index internt, kommer det att presentera ett användargränssnitt med namn.

Ett alternativt sätt att se De Bruijn-index är som De Bruijn-nivåer, som indexerar variabler från botten av stapeln snarare än från toppen. Detta eliminerar behovet av att omindexera fria variabler, till exempel när man försvagar sammanhanget, medan De Bruijn-index eliminerar behovet av att omindexera bundna variabler, till exempel när ett slutet uttryck ersätts i ett annat sammanhang.

De Bruijn-index är inte den enda representationen av λ-termer som undanröjer problemet med α-omvandling. Bland namngivna representationer är de nominella teknikerna för Pitts och Gabbay ett tillvägagångssätt, där representationen av en λ-term behandlas som en ekvivalensklass av alla termer som kan skrivas om till den med hjälp av variabla permutationer. Detta tillvägagångssätt används av Isabelle/HOL: s Nominella datatyppaket .

Ett annat vanligt alternativ är en vädjan till högre ordningens representationer där λ-bindemedlet behandlas som en sann funktion. I sådana representationer identifieras frågorna om α-ekvivalens, substitution etc. med samma operationer i en metalogik .

När man resonerar kring de metateoretiska egenskaperna hos ett deduktivt system i en korrekturassistent är det ibland önskvärt att begränsa sig till första ordningens representationer och ha förmågan att namnge eller byta namn på antaganden. Den lokalt namnlösa metoden använder en blandad representation av variabler – De Bruijn-index för bundna variabler och namn för fria variabler – som kan dra nytta av den α-kanoniska formen av De Bruijn-indexerade termer när så är lämpligt.

Barendregts variabla konvention

Barendregts variabla konvention är en konvention som ofta används i bevis och definitioner där det antas att:

• bundna variabler skiljer sig från fria variabler, och
• alla bindemedel binder variabler som inte redan är inom räckvidden.

I det allmänna sammanhanget för en induktiv definition är det inte möjligt att tillämpa α-omvandling efter behov för att konvertera en induktiv definition med hjälp av konventionen till en där konventionen inte används, eftersom en variabel kan förekomma i både en bindande position och en icke -bindande ställning i regeln. Induktionsprincipen gäller om varje regel uppfyller följande två villkor:

• regeln är ekvivariant i betydelsen nominell logik, det vill säga att dess giltighet är oförändrad genom att ändra namn på variabler
• om man antar regelns premisser är variablerna i bindande positioner i regeln distinkta och är fria i slutsatsen

Se även

• De Bruijn-notationen för λ-termer.
• Kombinationslogik , ett viktigare sätt att eliminera variabelnamn.