Co stanowi semantykę denotacyjną?

W innym wątku Andrej Bauer zdefiniował semantykę denotacyjną jako:

znaczenie programu jest funkcją znaczeń jego części.

Niepokoi mnie to, że ta definicja nie wyróżnia tego, co powszechnie uważa się za semantykę denotacyjną, z tego, co jest powszechnie uważane za semantykę niedenotacyjną, a mianowicie strukturalną semantykę operacyjną .

Mówiąc dokładniej, kluczowym składnikiem jest tutaj modułowość lub składowość semantyki, lub inaczej mówiąc, fakt, że są one zdefiniowane zgodnie z abstrakcyjną strukturą programu.

Ponieważ większość (wszystkich?) Formalnych semantyków ma obecnie charakter strukturalny, czy jest to wymagana definicja?

Moje pytanie brzmi: czym jest semantyka denotacyjna?

Rozróżnienie, które osobiście dokonuję między semantyką denotacyjną i operacyjną, wygląda mniej więcej tak:

• semantyka denotacyjna jest matematyczna i równikowa. Szczegóły redukcji mają znaczenie mniejsze niż wynik końcowy, który jest ponadczasową wartością w jakiejś przestrzeni matematycznej.
• semantyka operacyjna jest algorytmiczna. Rozwija się na poszczególnych etapach w czasie. Proces ten jest częścią znaczenia, a wynik końcowy jest tylko wyróżniającym się krokiem w tym procesie.

Różnica może być czasami subtelna i trudno jest stwierdzić, czy jest to tylko różnica w stylu, czy w treści.

Widzimy jednak, jak definicja kompozycyjna Andreja w bardziej naturalny sposób wynika z definicji denotacyjnej, a także możemy łatwo wyobrazić sobie niespójną, nie-kompozycyjną semantykę, która nadal spełnia definicję operacyjną.

Gdybym odgadł, co powiedziałaby Dana Scott, prawdopodobnie powiedziałby, że semantyka denotacyjna jest kompozycyjna (jak to, co twierdziłem) i że znaczenie programu musi być prawdziwym obiektem matematycznym, a nie jakąś składnią lub formalistą. Oczywiście taki pogląd wymaga rozróżnienia między formalną manipulacją składnią a „prawdziwą” matematyką. Jest to niekoniecznie matematyczne rozróżnienie.

W następstwie należy przypuszczać, że znaczenie to powinno być odpowiednie w tym sensie, że dwa różne obserwacyjne programy nie mają tego samego znaczenia. Oczywiście adekwatność tego rodzaju zależy od tego, co uznaje się za „obserwację”.

Zgodnie z tym poglądem można argumentować, że strukturalna semantyka operacyjna nie jest semantyką denotacyjną, ponieważ zrównuje znaczenie bytu syntaktycznego z innym bytem syntaktycznym (wartością lub sekwencją redukcji).

Zgadzam się, że identyfikacja semantyki denotacyjnej z kompozycyjnością przez A. Bauera (w książkach na temat semantyki języka programowania ) nie bardzo dobrze charakteryzuje to, co tradycyjnie rozumie się przez semantykę denotacyjną, ponieważ semantyka wyraźnie operacyjna oraz logika programu (semantyka aksjomatyczna) są kompozycyjne .

Sugerowałbym, aby termin ten był najlepiej rozumiany społeczno-historycznie, ponieważ odnosi się luźno do pewnej tradycji teorii (zapoczątkowanej na poważnie, gdy Scott opracował model teoretyczny sieci nieopartego rachunku lambda) z pewnymi preferowanymi narzędziami (teoria porządku, twierdzenia o punkcie stałym) , topologia, teoria kategorii) i preferowane języki docelowe (czysto funkcjonalne i sekwencyjne). Wyobrażam sobie, że - poza czystym interesem intelektualnym - semantyka denotacyjna została w większości wymyślona, ​​ponieważ:

1. Kiedyś trudno było uzasadnić semantykę operacyjną.

2. Kiedyś trudno było nadać semantykę aksjomatyczną niebanalnym językom.

$\pi$

Podsumowując, twierdzę, że termin „semantyka denotacyjna” stał się mniej precyzyjny, a przez to mniej użyteczny. Społeczność semantyki może pomóc w lepszej terminologii.

Jestem zadowolony z odpowiedzi Adreja, ale chciałbym zgłębić sprawę.

Na początek semantyka denotacyjna chce powiedzieć coś w stylu „znaczenie tego zapisu jest takie”. Prawdziwy semantysta chciałby wyobrazić sobie, że znaczenia są tym, co istnieje w naszym umyśle, a zapisy są tylko sposobem wyrażenia tych znaczeń. Wynika z tego wymóg, że semantyka denotacyjna powinna być złożona. Jeśli znaczenia są pierwotne, a oznaczenia wtórne, nie mamy innego wyboru, jak zdefiniować znaczenie większych zapisów jako funkcje znaczeń ich składników.

Jeśli zaakceptujemy ten punkt widzenia, dobra semantyka denotacyjna musi uchwycić znaczenia, które, jak zakładamy, mamy w głowie. Każda semantyka kompozycji niekoniecznie pasowałaby do rachunku. Jeśli wymyślę kompozycyjną definicję semantyczną i nikt nie zgadza się z tym, że zawiera ona jakiekolwiek znaczenia, które mają w ich głowie, to jest to mało przydatne. W tej sytuacji znajduje się semantyka gier. Jest to definicja kompozycyjna i technicznie dość mocna, ale bardzo niewiele osób zgadza się, że ma to coś wspólnego ze znaczeniami, które mają na myśli.

To powiedziawszy, każda definicja składu ma różne zalety techniczne. Możemy go użyć do weryfikacji równoważności lub innych właściwości poprzez indukcję składni terminów. Możemy go użyć do zweryfikowania poprawności systemów dowodowych, ponownie poprzez indukcję składni terminów. Możemy zweryfikować poprawność kompilatorów lub technik analizy programów (które ze swej natury są zdefiniowane przez indukcję składni). W pełni abstrakcyjna definicja semantyczna ma jeszcze więcej zalet technicznych. Możesz go użyć, aby pokazać, że dwa programy nie są równoważne, czego nie można zrobić z dowolną semantyką kompozycji. W pełni definiowalna definicja semantyczna jest jeszcze lepsza. Tutaj domeny semantyczne mają dokładnie to, co możesz wyrazić w języku programowania (z pewnymi zastrzeżeniami). Możesz więc wyliczyć wartości w domenach, aby zobaczyć, jakie są wartości, co byłoby trudne do zrobienia z notacjami składniowymi. Z tych wszystkich względów semantyka gier osiąga znakomite wyniki.

Jednak z biegiem lat kompozycyjne definicje semantyczne traciły na znaczeniu. Robin Milner i Andy Pitts opracowali szereg technik „ rozumowania operacyjnego ”, które działają wyłącznie na składni, ale używają semantyki operacyjnej wszędzie tam, gdzie jest to potrzebne do mówienia o zachowaniu. Te operacyjne techniki wnioskowania są mało zaawansowane. Bez wymyślnej matematyki. Żadnych nieskończonych obiektów. Możemy nauczyć ich studentów i każdy może ich używać. Tak więc wiele osób zadaje pytanie, dlaczego w ogóle potrzebujemy semantyki denotacyjnej. (Martin Berger jest prawdopodobnie w tym obozie).

Osobiście nie mam problemu z posiadaniem wielu narzędzi w moim zestawie narzędzi. Techniki denotacyjne mogą uzyskać lepsze wyniki w przypadku niektórych problemów, a techniki operacyjne w przypadku innych. Badacze, którzy opracują teorię, mogą być lepiej przystosowani do jednego lub drugiego podejścia. Dość często możemy rozwijać spostrzeżenia w jednym podejściu i przenosić je w drugim podejściu. (Wiele prac Andy'ego Pittsa jest tego rodzaju. Parametryzacja relacyjna została opracowana w układzie denotacyjnym, ale jest on w stanie dowiedzieć się, jak przekształcić ją jako rozumowanie operacyjne. Kiedy patrzę na to, mówię „wow, nigdy bym nie myślałem, że to możliwe. ”Logika separacji również idzie w tym kierunku. Steve Brookes podał 60-stronicowy dowód na poprawność logiki równoczesnej separacji przy użyciu semantyki denotacyjnej.

Podejścia operacyjne oceniają również znakomicie, gdy języki programowania stają się bardzo fantazyjne, z wszelkiego rodzaju zapętlonymi typami wyższego rzędu. Możemy nie mieć pojęcia, jak modelować takie rzeczy matematycznie. Lub standardowe modele matematyczne mogą okazać się niespójne pod wpływem pętli. (Na przykład, zobacz „Reynolds nie określa teorii polimorfizmu”). Podejścia operacyjne, które działają wyłącznie na składni, mogą zgodzić się na wszystkie te problemy matematyczne.

Innym podejściem pośrednim między podejściem operacyjnym a denotacyjnym jest wykonalność . Zamiast pracować z terminami składniowymi, tak jak w podejściach operacyjnych, przechodzimy częściowo na denotację, używając innej formy przedstawicieli matematycznych. Przedstawiciele ci mogą nie zostać zakwalifikowani jako prawdziwe „znaczenia” denotacyjne, ale byliby przynajmniej nieco bardziej abstrakcyjni niż terminy składniowe. Na przykład w przypadku polimorficznego rachunku lambda możemy najpierw nadać znaczenie terminom bez typu (w pewnym modelu rachunku lambda bez typu), a następnie użyć ich jako reprezentantów („realizatorów”) w celu wykonania jakiejś formy „rozumowania operacyjnego” w nieco bardziej abstrakcyjny poziom.

Niech więc będzie pewna zdrowa konkurencja między podejściami denotacyjnymi, operacyjnymi i wykonalnościowymi. Nie ma szkody.

Z drugiej strony, między różnymi podejściami może pojawić się również „niezdrowa” konkurencja. Ludzie pracujący z jednym podejściem mogą być do niego tak mocno przywiązani, że mogą nie rozumieć sensu innych podejść. Idealnie powinniśmy wszyscy być świadomi mocnych i słabych stron różnych podejść i rozwijać naukowe podejście do nich, nawet jeśli nie są naszymi indywidualnymi ulubieńcami.

[Jeszcze jedna odpowiedź. Prawdopodobnie nie jest fajne gromadzenie kilku odpowiedzi. Ale hej, to głęboka kwestia.]

Powiedziałem, że zgadzam się z odpowiedzią Andreja, ale wygląda na to, że nie zgadzam się całkowicie. Jest różnica.

Powiedziałem, że semantyka denotacyjna musi powiedzieć „znaczenie tego zapisu jest takie”. Chodziło mi o to, że notacjom należy przypisywać znaczenia, które są pewną formą pojęć , a nie innymi notacjami. W przeciwieństwie do tego Andrej wymagał, parafrazując Scotta, że ​​znaczeniem muszą być przedmioty „matematyczne”. Nie wierzę, że kawałek matematyki jest konieczny.

Na przykład z mojego punktu widzenia idealnie byłoby, gdyby znaczenia notacji były procesami fizycznymi. Po tym, jak wszystkie programy komputerowe uruchamiają hamulce w samochodzie, latają samolotami, zrzucają bomby i co tam jeszcze. Są to procesy fizyczne, a nie elementy w jakiejś przestrzeni matematycznej. Nie możesz zrzucić bomby, sprawdzić, czy kogoś zabije, i cofnąć, jeśli nie. Programy komputerowe nie mogą tego zrobić. Ale funkcje matematyczne mogą. (Są to tak zwane operacje „snapback”). Zatem nie jest wcale jasne, że funkcje matematyczne będą miały dobre znaczenie dla programów komputerowych.

Z drugiej strony tak naprawdę nie wiemy jeszcze, jak abstrakcyjnie mówić o procesach fizycznych. Możemy więc rzeczywiście użyć matematycznego opisu procesów w celu sformułowania naszych pomysłów. Ale te opisy matematyczne byłyby właśnie takimi „opisami”. Nie są znaczeniami. Prawdziwymi znaczeniami byłyby tylko fizyczne procesy, które wyobrażamy sobie koncepcyjnie.

W swoim przemówieniu akceptacyjnym dla nagrody SIGPLAN (która powinna być wkrótce na YouTube) Hoare powiedział, że ACP zastosowało „podejście algebraiczne”, CSP zastosowało „podejście denotacyjne”, a CCS zastosowało „podejście operacyjne” do opisania procesów. Ohad i ja siedzieliśmy razem podczas sesji, spojrzeliśmy na siebie i powiedzieliśmy „to jest naprawdę interesujące”. Jest tu więc dużo przestrzeni konceptualnej, która jest badana. Myślę, że wiele późniejszych prac Scotta, dotyczących systemów sąsiedzkich i systemów informatycznych itp., Rzeczywiście było próbą wyjaśnienia funkcji jako „procesów” jakiejś formy. Geometria interakcji Girarda i semantyka późniejszych gier są również próbami wyjaśnienia funkcji jako procesów. Powiedziałbym, że opracowanie solidnej teorii procesów może być dużym wkładem, jaki Informatyka może wnieść w matematykę XXI wieku. Nie zaakceptowałbym przekonania, że ​​matematyka ma wszystkie odpowiedzi i powinniśmy spróbować zredukować zjawiska obliczeniowe do pojęć matematycznych, aby je zrozumieć.

Zadziwia mnie to, jak pięknie ukrywanie informacji działa w obliczeniach stanowych (programowanie imperatywne oraz rachunki procesów), podczas gdy jest niezdarne i skomplikowane w formalizmach matematycznych / funkcjonalnych. Tak, mamy parametryczną relację, która pozwala nam bardzo dobrze ominąć ograniczenia formalizmów matematycznych. Ale nie pasuje do prostoty i elegancji programowania imperatywnego. Nie wierzę więc, że formalizmy matematyczne są właściwą odpowiedzią, choć przyznam, że są najlepszą odpowiedzią, jaką mamy obecnie. Ale powinniśmy dalej szukać. Istnieje ładna teoria procesów, która pobije tradycyjną matematykę.

[Mam nadzieję, że to moja ostatnia odpowiedź na to pytanie!]

Pierwotne pytanie Ohada dotyczyło tego, jak semantyka denotacyjna różni się od semantyki strukturalnej operacyjnej. Myślał, że oba są kompozycyjne. W rzeczywistości jest to nieprawda. Strukturalna semantyka operacyjna jest podana jako sekwencja kroków. Każdy krok jest wyrażany kompozycyjnie (a Plotkin jest niezwykłym odkryciem, że jest to możliwe!), Ale całe zachowanie nie jest zdefiniowane kompozycyjnie. Oto, co mówi Plotkin we wstępie do artykułu SOS [podkreślenie dodane]:

W semantyce denotacyjnej podąża się za ideałem kompozycyjności, w którym znaczenie wyrażenia złożonego podano jako funkcję znaczenia jego części. W przypadku semantyki operacyjnej rozważa się zachowanie frazy programowej, która jest tylko zbiorem przejść, które może wykonać. To zachowanie nie jest jednak kompozycyjne, gdy jest uważane za funkcję fraz programowych. Jednak reguły dają to strukturalnie, tzn. Prymitywne rekurencyjne, w składni; ...

Fakt, że każdy krok jest wyrażany kompozycyjnie, nie oznacza, że ​​całe zachowanie jest wyrażane kompozycyjnie.

Jest ładny artykuł Carla Guntera zatytułowany Forms of Semantic Specification , w którym różne metody określania semantyki są porównywane i kontrastowane. Znaczna część tego materiału jest również reprodukowana w pierwszym rozdziale jego tekstu „Semantyka języków programowania”. Mam nadzieję, że powinno to wyjaśnić obraz.

Kolejne słowo o „semantyce operacyjnej”. Na początku termin „operacyjny” był używany w odniesieniu do każdej definicji semantycznej odnoszącej się do szczegółowych etapów oceny. Zarówno semantycy denotacyjni, jak i zwolennicy aksjomatyczni patrzyli na semantykę „operacyjną”, uważając ją za niskopoziomową i zorientowaną na maszynę. Myślę, że było to naprawdę oparte na ich przekonaniu, że opisy na wyższym poziomie były możliwe. Przekonania te zostały rozbite, gdy tylko rozważyły ​​współbieżność. Procesy Bakera i Zuckera oraz semantyka denotacyjna współbieżności mają następujące interesujące fragmenty:

Użyjemy metodologii semantyki denotacyjnej . „Denotacyjny” należy tu zestawić z „operacyjnym”: Kluczową ideą tego pierwszego podejścia jest to, że wyrażenia w języku programowania oznaczają wartości w domenach matematycznych wyposażonych w odpowiednią strukturę, podczas gdy w tym drugim operacje określone przez konstrukcje językowe są modelowane etapami wykonanymi przez odpowiednią maszynę abstrakcyjną ....

Model matematyczny zawiera różne pojęcia, które choć denotacyjne w stylu, działają w duchu [podkreślenie dodane]. Należą do nich „historia” pojęcia samego procesu oraz zastosowanie tak zwanych cichych ruchów w radzeniu sobie z synchronizacją i rekurencją.

Tutaj widzimy, jak autorzy zmagają się z dwoma pojęciami „operacyjnymi”, z których jednym jest pojęcie techniczne - zachowanie wyrażone za pomocą manipulacji składniowych, a drugie pojęcie koncepcyjne - na niskim poziomie i szczegółowe. Uznanie w dużej mierze przysługuje Plotkinowi i Milnerowi za rehabilitację semantyki „operacyjnej”, dzięki czemu jest ona na jak najwyższym poziomie i pokazuje, że może być elegancka i wnikliwa.

Mimo to operacyjne pojęcie procesu wciąż różni się od denotacyjnego pojęcia procesu, przy czym ten ostatni opracowali zarówno de Bakker, jak i Hoare i ich zespoły. I myślę, że wiele jest tajemniczych i pięknych kwestii związanych z procesem denotacyjnym, które należy jeszcze zrozumieć.

Ta dodatkowa reakcja ma wzmocnić punkt, w którym denotacyjne modele semantyczne zostały zaprojektowane w celu „wyjaśnienia” zjawisk obliczeniowych. Podam serię przykładów z semantyki imperatywnych języków programowania (zwanych również językami „przypominającymi Algol”).

Najpierw był model semantyczny sformułowany przez Scotta i Stracheya. (Por. Gordon: Denotacyjny opis języków programowania - moja ulubiona książka lub książka Winskela.) Ten model zakłada, że ​​istnieje stan globalny , złożony ze stanu wszystkich lokalizacji przydzielonych przez program. Każde polecenie jest interpretowane jako funkcja od stanów globalnych do stanów globalnych.

Reynolds powiedział, że nie modeluje dyscypliny stosu zmiennych lokalnych. Po wprowadzeniu zakresu lokalnego jego zmienne są przydzielane i są one zwalniane po wyjściu z zakresu. Zasadniczo jest to pytanie: „w jakim sensie zmienne lokalne są lokalne?” Jak semantyka uchwyci lokalizację? Aby to wyjaśnić, wynalazł model kategorii funktorów. (Por. Reynolds: The Essence of Algol and Tennent: Semantyka języków programowania).

Tennent chciał modelować zasady rozumowania sformułowane w Logice specyfikacji Reynoldsa (rozszerzenie Hoare Logic dla procedur wyższego rzędu). Logika ma takie pomysły, jak obliczenia podobne do wyrażeń (tylko do odczytu), brak zakłóceń między obliczeniami podobnymi do poleceń i wyrażeń, a także niektóre zasady rozumowania abstrakcji danych. Udoskonalił model kategorii funktorów Reynoldsa, aby znaleźć nowy. Nazywa się to modelem „SASL”, również opisanym w książce Tennenta.

Meyer i Sieber, a także O'Hearn i Tennent, zauważyli, że żaden z tych modeli nadal nie wychwytuje w pełni lokalizacji zmiennych lokalnych. Gdy dwie implementacje abstrakcyjnego typu danych lub klasy różnią się lokalnymi zmiennymi, ale manipulują nimi w sposób, który zachowuje się tak samo, gdy jest oglądany z zewnątrz, są one obserwowalne równoważne. Semantyka denotacyjna powinna je zrównać. Aby to wymodelować, O'Hearn i Tennent dodali parametryczną relację do wariantu modelu kategorii funktorów Reynoldsa.

Kiedy jednocześnie spojrzałem na problem, nie wierzyłem w podejście do kategorii funktorów. Pomyślałem też, że to zbyt techniczne i wierzyłem, że musi istnieć prostszy model. Doprowadziło mnie to do opracowania modelu „Stan globalny uznany za niepotrzebny”, który jest raczej jak model śledzenia CSP, ale dla języka wyższego rzędu. Jako dodatkowy bonus, model ten uchwycił również nieodwracalność zmiany stanu, która nie występowała we wcześniejszych modelach.

Mój model działał tylko dla dobrze zachowującego się języka Algol, zwanego Syntaktyczną Kontrolą Zakłóceń . Abramsky i McCusker rozszerzyli mój model, używając pomysłów dotyczących semantyki gier, aby mógł on działać dla pełnego Algolu. Ich model wyjaśnia te same zjawiska, co mój, ale w większym języku.

W każdym przypadku jesteśmy w stanie wykazać, że nowe modele wychwytują ekwiwalenty obserwacyjne (lub inne formy wzorów logicznych) wykazujące wspomniane zjawiska obliczeniowe, które nie zostały zatwierdzone przez wcześniejsze modele. Istnieje więc bardzo precyzyjny sens, w którym modele te „wyjaśniają” zjawiska obliczeniowe.

[Całą pracę, o której tu wspomniałem, można znaleźć w tomach „Języki podobne do Algolu”: link i link ]