Abstrakt syntax av högre ordning

Inom datavetenskap är abstrakt syntax av högre ordning (förkortat HOAS ) en teknik för representation av abstrakta syntaxträd för språk med variabla bindare .

Relation till första ordningens abstrakta syntax

En abstrakt syntax är abstrakt eftersom den representeras av matematiska objekt som har en viss struktur till sin natur. Till exempel, i första ordningens abstrakta syntax- träd ( FOAS ), som vanligtvis används i kompilatorer , innebär trädstrukturen subexpressionsrelationen, vilket betyder att inga parenteser krävs för att disambiguera program (som de är, i den konkreta syntaxen ). HOAS exponerar ytterligare struktur: förhållandet mellan variabler och deras bindningsställen. I FOAS-representationer representeras en variabel typiskt med en identifierare, där förhållandet mellan bindningsställe och användning indikeras genom att använda samma identifierare . Med HOAS finns det inget namn på variabeln; varje användning av variabeln hänvisar direkt till bindningsstället.

Det finns ett antal anledningar till varför denna teknik är användbar. För det första gör det den bindande strukturen för ett program explicit: precis som det inte finns något behov av att förklara operatörernas företräde i en FOAS-representation, finns det inget behov av att ha reglerna för bindning och omfattning till hands för att tolka en HOAS-representation. För det andra har program som är alfaekvivalenta (som bara skiljer sig i namnen på bundna variabler) identiska representationer i HOAS, vilket kan göra likvärdighetskontrollen mer effektiv.

Genomförande

Ett matematiskt objekt som skulle kunna användas för att implementera HOAS är en graf där variabler associeras med deras bindningsställen via kanter . Ett annat populärt sätt att implementera HOAS (i ​​till exempel kompilatorer) är med de Bruijn-index .

Använd i logisk programmering

Det första programmeringsspråket som direkt stödde λ-bindningar i syntax var det högre ordningens logiska programmeringsspråket λProlog . Papperet som introducerade termen HOAS använde λProlog-kod för att illustrera det. Tyvärr, när man överför termen HOAS från den logiska programmeringen till den funktionella programmeringsinställningen, innebär den termen identifiering av bindningar i syntax med funktioner över uttryck. I den senare inställningen har HOAS en annan och problematisk känsla. Termen λ-trädsyntax har introducerats för att specifikt referera till representationsstilen som är tillgänglig i logikprogrammeringsinställningen. Även om det är olika i detalj, liknar behandlingen av bindningar i λProlog deras behandling i logiska ramar, som utvecklas i nästa avsnitt.

Använd i logiska ramar

I domänen av logiska ramverk används termen abstrakt syntax av högre ordning vanligtvis för att hänvisa till en specifik representation som använder bindemedel för metaspråket för att koda den bindande strukturen för objektspråket.

Till exempel har det logiska ramverket LF en λ-konstruktion, som har piltyp (→). Som ett exempel, tänk på att vi ville formalisera ett mycket primitivt språk med otypade uttryck, en inbyggd uppsättning variabler och en let-konstruktion ( låt <var> = <exp> i <exp'> ), som gör det möjligt att binda variabler var med definition exp i uttryck exp' . I tolvsyntax kan vi göra enligt följande: 

   
   
     
          exp  :  typ  .  var  :  typ  .  v  :  var  ->  exp  .  låt  :  var  ->  exp  ->  exp  ->  exp  .

Här är exp typen av alla uttryck och var typen av alla inbyggda variabler (implementerade kanske som naturliga tal, vilket inte visas). Konstanten v fungerar som en gjutningsfunktion och vittnar om att variabler är uttryck. Slutligen representerar konstanten let let-konstruktioner av formen let <var> = <exp> i <exp> : den accepterar en variabel, ett uttryck (som är bundet av variabeln) och ett annat uttryck (som variabeln är bunden inom) .

Den kanoniska HOAS-representationen av samma objektspråk skulle vara: 

   
          exp  :  typ  .  låt  :  exp  ->  (  exp  ->  exp  )  ->  exp  .

I den här representationen visas inte objektnivåvariabler explicit. Konstanten let tar ett uttryck (det vill säga att bindas) och en funktion på metanivå exp → exp (letens kropp). Denna funktion är den högre ordningen : ett uttryck med en fri variabel representeras som ett uttryck med hål som fylls i av metanivåfunktionen när den tillämpas. Som ett konkret exempel skulle vi konstruera uttrycket på objektnivå 

      
     låt  x  =  1  +  2  i  x  +  3

(förutsatt att de naturliga konstruktörerna för tal och addition) använder HOAS-signaturen ovan som

         låt  (  plus  1  2  )  ( [  y  ]  plus  y  3  )

där [y] e är Twelfs syntax för funktionen .

Denna specifika representation har fördelar utöver de ovan: för det första, genom att återanvända begreppet bindning på metanivå, åtnjuter kodningen egenskaper som typbevarande substitution utan att behöva definiera/bevisa dem. På detta sätt kan användningen av HOAS drastiskt minska mängden boilerplate-kod som har att göra med bindning i en kodning.

Abstrakt syntax av högre ordning är i allmänhet endast tillämplig när objektspråkvariabler kan förstås som variabler i matematisk mening (det vill säga som stand-ins för godtyckliga medlemmar av någon domän). Detta är ofta, men inte alltid, fallet: till exempel finns det inga fördelar att vinna med en HOAS-kodning av dynamiskt omfattning som det ser ut i vissa dialekter av Lisp eftersom dynamiskt omfångade variabler inte fungerar som matematiska variabler.

Se även

Vidare läsning

Hämtad från " https://en.wikipedia.org/w/index.php?title=Higher-order_abstract_syntax&oldid=1134855891 "