Jaki jest rodzaj semantyki języka programowania?

W rozdziale 1 Praktycznych podstaw języków programowania autor wspomina, że ​​abstrakcyjne drzewa składniowe są powiązane z sortowaniem .

Intuicyjnie, rodzaje są jak typy, ale chciałbym wiedzieć, czy mają precyzyjną definicję. Byłbym zadowolony, gdyby podano również niektóre referencje.

To zależy od tego, jaką semantykę przyjmowalibyśmy dla typów i rodzajów. - Jakkolwiek krótkie - mało nieformalne - definicje mogą być - Sortowanie jest klasami AST, a typy są klasami wartości .

W rzeczywistości istnieje wiele podobieństw między rodzajami składni abstact i typami, jak zwykle rozumie się. Ale rodzaje są formalną koncepcją składniową , a drzewa AS są również składnią, podczas gdy typy są koncepcją semantyczną .

Terminologia pochodzi od terminu algebry (zwane również wolnymi algebrami ) i algebry uniwersalnej . Są to zasadniczo składniowe teorie struktur algebraicznych, analizowane niezależnie od jakichkolwiek interpretacji. Zostały one opracowane w pierwszej połowie XX wieku.

Termin może być postrzegany jako drzewo, w którym węzły są oznaczone skończonym zestawem operatorów, przy czym każdy operator ma ustaloną aranżację, która określa liczbę córek w drzewie. Arity 0 jest dla liści. W algebrach wielosortowanych jest to udoskonalane przez sortowania, dzięki czemu każdy operator należy do sortowania, a arie są zastępowane uporządkowaną listą sortów, która naprawia dla każdej córki rodzaj operatora głównego. Rodzaj operatora wraz z listą rodzajów jego córki nazywany jest podpisem operatora.

W algebrach uniwersalnych jest to dalej udoskonalane poprzez wprowadzenie równościowo zdefiniowanych relacji równoważności między terminami.

Choć wydaje się, że nieco zanikło, koncepcje te były dość popularne i szeroko badane w informatyce pod koniec XX wieku, jako abstrakcyjne algebry, które następnie były postrzegane jako podstawa dla abstrakcyjnych typów danych, które są częściowo prekursorem tego, co jest Klasy nos w programowaniu obiektowym.

Algebry uniwersalne związane są z rozwojem teorii kategorii, która ma również fundamentalne znaczenie w obecnej wizji typów i języków programowania.

Algebry są obiektami składniowymi i mają być używane z interpretacją w niektórych domenach semantycznych odpowiadających typom. Interpretacja jest homomorfizmem, który odwzorowuje sortuje na domeny wartości (typy) , a operatory na funkcje między tymi domenami, aby respektować podpisy, a także równania w przypadku algebry równań. W ten sposób można zastosować wyniki teorii grup do dowolnej domeny za pomocą operacji zgodnej z definicją grupy.

Ta organizacja została uznana za bardzo dogodną przez wczesnych badaczy języków programowania, szczególnie tych zajmujących się formalizacją języków programowania. Miał tę zaletę, że izolował składnię i semantykę oraz był dobrze rozumiany matematycznie.

Innym powodem przyjęcia tej zasady była obawa związana z opracowaniem narzędzia do manipulowania programami w środowisku programistycznym lub w systemach formalnych w celu udowodnienia właściwości programów (które okazały się coraz bardziej podwójnymi problemami).

Doprowadziło to do pojawienia się koncepcji abstrakcyjnego drzewa składni (AST) dla języków programowania, które są w istocie terminami algebry wielosortowej (czasami udoskonalanej przy użyciu uni sortowania w niektórych systemach). AST jest składnią odniesienia dla języka, z którego semantykę można zdefiniować homomorfizmem, jak w semantyce denotacyjnej.

Jest to nie tylko wygodne do studiowania semantyki języków, ale drzewa mają lepszą strukturę niż łańcuchy, a tym samym lepszą podstawę do programowania narzędzi programistycznych i środowisk programistycznych.

Umożliwia izolowanie parsowania, które tradycyjnie było bałaganem, ponieważ ograniczenia technologii parsowania wymuszały stosowanie zniekształconej gramatyki. Uwzględnia również problemy z prezentacją.

Pozwala na wiele konkretnych (łańcuchowych lub graficznych) reprezentacji programów, co czasem może być wygodne (nie ma powodu, dla którego należy wymuszać na ludziach stosowanie interpunkcji zamiast tabulatorów lub odwrotnie w składni programów).

Ułatwia definiowanie wielu interpretacji programów i ich rodzajów w celu analizy poprawności programów za pomocą interpretacji abstrakcyjnych.

Jest wygodny do pisania (pół) automatycznych narzędzi do manipulacji programami, na przykład do automatycznych przekształceń programów lub tłumaczeń między językami.

Czasami rzeczy mogą być nieco bardziej skomplikowane w praktyce, ponieważ niektóre formy składni abstrakcyjnej pozwalają niektórym operatorom budować drzewa (wyrażenia), które należą do kilku rodzajów (nieformalny sposób patrzenia na to). Na przykład może istnieć rodzaj dla konstrukcji składniowych, które reprezentują zmienne (byty możliwe do przypisania), a inny dla wyrażeń. Ale dowolną zmienną można użyć jako wyrażenia, przy czym odwrotność jest fałszywa.

Wczesne artykuły na ten temat dotyczące języków programowania pochodzą z połowy lat siedemdziesiątych. W tym czasie konceptualizacja była przeznaczona do tworzenia środowisk programistycznych świadomych składni (wówczas użyto słowa „ukierunkowany”). Poszukaj Mentora i Centaura w Europie oraz Cornell Program Synthesizer w USA. Były to dwa pierwsze systemy, które faktycznie wykorzystywały takie koncepcje w praktyczny sposób. Później opracowano wiele innych.

Ale abstrakcyjna składnia poprzedza te systemy. Język Lisp (1958) miał abstrakcyjną składnię, co nie jest zaskoczeniem, ponieważ został opracowany przez logika i w celu tworzenia programów, które manipulują programami (patrz także ML i LCF ... które pojawiły się później). Ale Lisp nie został posortowany: wszystko było składniowo listą, a bardziej dopracowana struktura była zasadniczo zależna od semantyki. To spowodowało, że niektórzy uważają, nieco niepoprawnie, że Lisp nie ma składni.

W rozdziale czwartym okazuje się, że sortowanie dotyczy składni, a typy semantyki.

Przykładowa tabela składniowa na stronie 40 dotyczy rodzajów w języku L {num str}. Najwyraźniej sortuje kategorie w składni języka.

W szczególności „plus” ma rodzaj, który jest kategorią składniową jego wyniku. Rodzaj operatora „plus” nosi nazwę „Exp”. To reprezentuje fakt, że składniowo wywołanie operatora „plus” jest wyrażeniem. Wywołanie operatora „plus” może wypełnić pozycję w abstrakcyjnym drzewie składni, gdzie dozwolone jest wyrażenie. Taka jest konstrukcja „plus”. W ten sposób pasuje do struktury tekstu reprezentującego program.

System typów na stronie 41 dotyczy typów w języku L {num str}. Typ operatora „plus”, biorąc pod uwagę, że jego operandy mają typ „num”, to „num”. Ten osąd jest częściowym opisem semantyki operatora „plus”. Oznacza to, że część znaczenia operatora „plus” polega na połączeniu dwóch liczb w celu uzyskania liczby. Oznacza to, że odróżnia „plus” od innych wyrażeń.

Ponadto istnieje sortowanie o nazwie „Typ”, które zawiera dwa typy: „num” i „str”.

Na początku rozdziału 1 Harper daje wskazówkę, co rozumie przez słowo sort :

Składnia języka określa sposób, w jaki różne rodzaje wyrażeń (wyrażeń, poleceń, deklaracji itd.) Mogą być łączone w celu tworzenia programów.

Definiuje słowo frazę jako abstrakcyjne drzewo składniowe, które następnie omawia.