Składnia abstrakcyjna wyższego rzędu

W informatyce składnia abstrakcyjna wyższego rzędu (w skrócie HOAS ) to technika reprezentacji abstrakcyjnych drzew składniowych dla języków ze zmiennymi spoiwami .

Relacja do składni abstrakcyjnej pierwszego rzędu

Składnia abstrakcyjna jest abstrakcyjna , ponieważ jest reprezentowana przez obiekty matematyczne , które ze swej natury mają określoną strukturę. Na przykład w składni abstrakcyjnej pierwszego rzędu ( FOAS ), powszechnie stosowanych w kompilatorach , struktura drzewa implikuje relację podwyrażenia, co oznacza, że ​​żadne nawiasy nie są wymagane do ujednoznacznienia programów (tak jak to jest w konkretnej składni ). HOAS ujawnia dodatkową strukturę: związek między zmiennymi a ich miejscami wiązania. W reprezentacjach FOAS zmienna jest zwykle reprezentowana za pomocą identyfikatora, przy czym związek między miejscem wiązania a zastosowaniem jest wskazywany za pomocą tego samego identyfikatora. W przypadku HOAS zmienna nie ma nazwy; każde użycie zmiennej odnosi się bezpośrednio do miejsca wiązania.

Istnieje wiele powodów, dla których ta technika jest przydatna. Po pierwsze, wyraźnie wyjaśnia strukturę powiązań programu: tak jak nie ma potrzeby wyjaśniania pierwszeństwa operatorów w reprezentacji FOAS, nie ma potrzeby posiadania pod ręką reguł powiązań i zakresu, aby interpretować reprezentację HOAS. Po drugie, programy, które są równoważne alfa (różniące się tylko nazwami powiązanych zmiennych) mają identyczne reprezentacje w HOAS, co może sprawić, że sprawdzanie równoważności będzie bardziej wydajne.

Realizacja

Jednym z obiektów matematycznych, który można wykorzystać do wdrożenia HOAS, jest wykres , w którym zmienne są powiązane z ich miejscami wiązania za pomocą krawędzi . Innym popularnym sposobem implementacji HOAS (na przykład w kompilatorach) są indeksy de Bruijna .

Zastosowanie w programowaniu logiki

Pierwszym językiem programowania, który bezpośrednio obsługiwał powiązania λ w składni, był język programowania logiki wyższego rzędu λProlog . Artykuł, który wprowadził termin HOAS, wykorzystał kod λProlog do jego zilustrowania. Niestety, kiedy przenosi się termin HOAS z programowania logicznego do programowania funkcjonalnego, termin ten implikuje identyfikację powiązań w składni z funkcjami nad wyrażeniami. W tym ostatnim ustawieniu HOAS ma inny i problematyczny sens. Termin składnia drzewa λ został wprowadzony, aby odnosić się konkretnie do stylu reprezentacji dostępnego w ustawieniach programowania logicznego. Chociaż różni się w szczegółach, traktowanie powiązań w λProlog jest podobne do ich traktowania w ramach logicznych, omówionych w następnej sekcji.

Użyj w ramach logicznych

W domenie struktur logicznych termin abstrakcyjna składnia wyższego rzędu jest zwykle używany w odniesieniu do określonej reprezentacji, która wykorzystuje wiązania metajęzyka do kodowania struktury powiązań języka obiektowego.

Na przykład struktura logiczna LF ma konstrukcję λ, która ma typ strzałki (→). Weźmy na przykład pod uwagę, że chcieliśmy sformalizować bardzo prymitywny język z wyrażeniami bez typów, wbudowanym zestawem zmiennych i konstrukcją let ( let <var> = <exp> in <exp'> ), która pozwala wiązać zmienne var z definicją exp w wyrażeniach exp' . W Dwunastu moglibyśmy zrobić tak: 

   
   
     
          exp  :  typ  .  var  :  typ  .  v  :  var  ->  exp  .  niech  :  var  ->  exp  ->  exp  ->  exp  .

Tutaj exp jest typem wszystkich wyrażeń, a var typem wszystkich wbudowanych zmiennych (zaimplementowanych być może jako liczby naturalne, czego nie pokazano). Stała v działa jak funkcja rzutująca i świadczy o tym, że zmienne są wyrażeniami. Wreszcie, stała let reprezentuje konstrukcje let w postaci let <var> = <exp> in <exp> : akceptuje zmienną, wyrażenie (powiązane przez zmienną) i inne wyrażenie (w którym zmienna jest powiązana) .

Kanoniczna reprezentacja HOAS tego samego języka obiektowego byłaby następująca : 

   
          exp  :  typ  .  niech  :  exp  ->  (  exp  ->  exp  )  ->  exp  .

W tej reprezentacji zmienne na poziomie obiektu nie pojawiają się jawnie. Stała let przyjmuje wyrażenie (czyli wiązanie) i funkcję meta-poziomową exp → exp (ciało let). Ta funkcja jest wyższego rzędu : wyrażenie ze zmienną wolną jest reprezentowane jako wyrażenie z lukami , które po zastosowaniu są wypełniane przez funkcję meta-poziomu. Jako konkretny przykład stworzylibyśmy wyrażenie na poziomie obiektu 

      
     niech  x  =  1  +  2  w  x  +  3

(zakładając naturalne konstruktory liczb i dodawania) przy użyciu powyższego podpisu HOAS as

         niech  (  plus  1  2  )  ([  y  ]  plus  y  3  )

gdzie [y] e jest składnią Dwunastu dla funkcji .

Ta specyficzna reprezentacja ma zalety wykraczające poza powyższe: po pierwsze, dzięki ponownemu wykorzystaniu pojęcia wiązania na poziomie meta, kodowanie ma właściwości, takie jak podstawienie zachowujące typ bez potrzeby ich definiowania/udowodniania. W ten sposób użycie HOAS może drastycznie zmniejszyć ilość kodu standardowego związanego z wiązaniem w kodowaniu.

Abstrakcyjna składnia wyższego rzędu ma generalnie zastosowanie tylko wtedy, gdy zmienne języka obiektowego można rozumieć jako zmienne w sensie matematycznym (to znaczy jako zamienniki dla dowolnych członków jakiejś domeny). Dzieje się tak często, ale nie zawsze: na przykład nie ma żadnych korzyści z kodowania dynamicznego zakresu HOAS , jakie pojawia się w niektórych dialektach Lispa , ponieważ zmienne o dynamicznym zasięgu nie działają jak zmienne matematyczne.

Zobacz też

Dalsza lektura

Pobrano z „ https://en.wikipedia.org/w/index.php?title=Higher-order_abstract_syntax&oldid=1134855891 ”