Co stanowi semantykę denotacyjną?

45

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?

Ohad Kammar
źródło
4
Znaczenie można nadać w wielu formach: warunki przed-postowe, działanie abstrakcyjnej maszyny, jednostka matematyczna, strategia gry. We wszystkich współczesnych podejściach znaczenia te są podane jako funkcja znaczenia części.
Ohad Kammar,
1
Pytanie o istnienie zapoczątkowało badanie teorii domen. Wywodzi się z denotacyjnego podejścia, ale go nie definiuje (na przykład w danym języku może nawet nie być przestrzeni funkcyjnych). Jeśli chodzi o modułowość, jak powiedziałem powyżej, w zasadzie każde nowoczesne podejście do semantyki ma kompozycyjność w odpowiednim znaczeniu. [DD]D
Ohad Kammar,
10
Ok, przestańcie rozpowszechniać fałszywą opinię, że zainicjowała lub zmotywowała teorię domen, ponieważ tak się nie stało. Dana Scott chciała, aby teoria domen była teorią matematyczną odpowiednią dla typowanego λ- rachunku. Fakt, że podał także model nieoznaczonego λ- kamienia, był wypadkiem . Wiem, powiedział mi to. [DD]=D λλ
Andrej Bauer,
2
[DD]=DλD[DD]D
1
Nie jestem pewien, czy to pomaga, ale sposób, w jaki widzę „bieżącą” semantykę denotacyjną, to „kompilacja języka w jakąś kategorię” - rzeczywiście można pisać semantykę w kategoriach dobrze znanych obiektów matematycznych bez naciskania na strukturę kategorii, ale to uczciwa charakterystyka konkretnych przykładów, które napotkałem.
gasche

Odpowiedzi:

30

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ą.

Marc Hamann
źródło
Dobrym przykładem różnicy algorytm-vs-matematyka jest leczenie nieterminacji. Oznaczenie pętli jest dolne, ale z powodu problemu zatrzymania nierozstrzygalne jest, czy oznaczenie dowolnego programu jest dolne. Zamiast tego w semantyce małych kroków można obserwować kroki redukcji, ale teoria nie ma wartości „dolnej”. Nierozstrzygalność i nieterminacja przechodzą do metateorii: nierozstrzygalne jest to, czy sekwencja redukcji się kończy. Podobnie w semantyce dużych kroków nierozstrzygalne jest, czy istnieje derywacja.
Blaisorblade
23

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).

Andrej Bauer
źródło
3
Od czasu do czasu mówiono mi, że systemy przejściowe nie są tak matematyczne, jak domeny, sieci lub zamówienia. Ten widok wydaje mi się zaskakujący. Wszystko można wyrazić w teorii zbiorów ZFC.
Martin Berger,
1
Zastanawianie się, jak dokładnie dana semantyka może modelować zjawisko obliczeniowe, jest bardziej interesującym podejściem i rzeczywiście zależy w znacznym stopniu od wybranego pojęcia obserwacji. Jedną z kluczowych zalet semantyki operacyjnej (np. Teorii procesu) jest właśnie to, że naturalne pojęcia obserwacji są znacznie łatwiejsze do zdefiniowania w porównaniu z semantyką teoretyczną.
Martin Berger,
3
@Marc: Zgadzam się z tobą, że metody operacyjne nie modelują obliczeń jako funkcji. Ale nie rozumiem, dlaczego czyni to podejście teoretyczne porządkiem „bardziej matematycznym”. Wpływ matematyki na fizykę, jak równania różniczkowe, modeluje oceny niektórych układów w czasie. Samo podejście wejście-wyjście wykorzystuje podstawową strukturę czasową, a mianowicie to, że wyjście nie jest dostępne przed wejściem.
Martin Berger,
2
@Martin: Matematycy często narzekają, że to, co robią fizycy, nie jest też prawdziwą matematyką. ;-) W tym momencie fizyka jest po prostu nauką bardziej komfortową. TCS jest wciąż stosunkowo nowym dzieckiem na bloku. Myślę, że TCS nie powinna się martwić o to, by uszczęśliwić ludzi z innej dyscypliny (bez względu na to, jak bardzo to lubimy). mamy własne mojo w drodze (tak jak fizycy).
Marc Hamann,
2
@Marc: dowolne śmieci można wyrazić w ZFC, więc nie jest to zbyt duże kryterium, na którym można polegać. Semantyka, w której „funkcje” w języku programowania są interpretowane jako funkcje w sensie matematycznym, ma co najmniej dwie zalety. Po pierwsze, dobrze pasuje do tego, jak ludzie myślą o funkcjach w języku programowania. Po drugie, funkcje są znanymi obiektami matematycznymi, więc istnieje wiele maszyn, z których można korzystać. Oczywiście systemy przejściowe również mają swoje zastosowania.
Andrej Bauer,
19

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.

π

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.

Martin Berger
źródło
1
Podsumowując mój ostatni post, „semantyka denotacyjna” musi powiedzieć „znaczenie tego zapisu jest takie”. Semantyka „operacyjna” i semantyka „aksjomatyczna” nie są tego rodzaju definicjami semantycznymi. Wprowadzanie ich w błąd jest mylące. Należy również zauważyć, że tak zwane „podejście operacyjne” to podejście do rozumowania programów. To nie jest semantyka operacyjna. Podejście operacyjne i podejście aksjomatyczne mogą zastąpić inżynierskie zastosowania semantyki denotacyjnej. Ale nie stają się semantyką denotacyjną.
Uday Reddy
LπL
1
@Jaskółka oknówka. Dlaczego przypisywanie procesów w sposób kompozycyjny nie jest denotacyjne. Może się zdarzyć, jeśli przekonasz nas wszystkich, że procesy są podstawową teorią, podobnie jak teorią zbiorów, i nie należy prosić o jej semantykę. Współczuję poglądowi, że mógłby istnieć podstawowy język modelujący obliczenia stanowe. Być może rachunek procesowy jakiejś formy zostanie kiedyś uznany za taki fundament. Ale nie sądzę, że jeszcze tam jesteśmy.
Uday Reddy
1
@MartinBerger To jedyny, jakiego się nauczyłem, ale trudno mi od razu zapewnić dobre referencje. Na przykład „Wreszcie bez tagów, częściowo ocenione” ( citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.99.9287 ) używa „wstępu”, „składu” i „prymitywnej rekurencyjnej” we wstępie jako oczywistych synonimów (ale nie jest to dużo omawiane w artykule, jest to oczywiste). Viceversa, wydaje się, że jest to punkt debaty w filozofii, jeśli można zaufać Wikipedii tutaj: en.wikipedia.org/wiki/Principle_of_compositionality#Critiques
Blaisorblade
1
@Blaisorblade Kiedy byłem doktorantem, spotkałem się z denotacyjnymi semantami, ponieważ miałem pracować nad semantyką denotacyjną. Zawsze pytałem ich, czym jest semantyka denotacyjna, gdyby mogli podać mi abstrakcyjną definicję, ale dostałem tylko wymijające lub niejasne odpowiedzi, takie jak: „semantyka denotacyjna to semantyka matematyczna”, patrz także wyjaśnienie A. Bauera. Nie sądzę, aby koncepcja była dobrze zdefiniowana. Nie rozumiem też, dlaczego wymaganie np. Prymitywnej rekurencyjności jest wystarczająco ograniczone, ponieważ moc prymitywnej rekurencji zależy od tego, co jeszcze jest dostępne: (ciąg dalszy)
Martin Berger
16

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 nieró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.

Uday Reddy
źródło
Jednym z konstruktywnych podejść do rozwiązania tego problemu może być znalezienie tłumaczeń między różnymi podejściami.
Martin Berger
1
Zauważ, że nie mam problemu z konwencjonalną semantyką denotacyjną jako narzędziem w przyborniku. Po prostu znajduję dorozumiane lub wyraźne sugestie, że są one w jakiś sposób lepsze, aby były problematyczne i pozbawione spójnego uzasadnienia.
Martin Berger
Jako przykład dobrej praktyki opublikowałbym woluminy „Algollike Languages” ( eecs.qmul.ac.uk/~ohearn/Algol/algol.html ) zredagowane przez Petera O'Hearn'a i Boba Tennenta. Obejmują one artykuły na temat „konwencjonalnej semantyki denotacyjnej” (Strachey, Reynolds, Tennent, Meyer i in.), A także „niekonwencjonalnej” semantyki denotacyjnej (moja, Abramsky i McCusker, Brookes) oraz podejść operacyjnych (Andy Pitts, Felleisen). Nawiasem mówiąc, dwa artykuły Reynoldsa w tomach (Logika specyfikacji i Kontrola składniowa zakłóceń) były „aksjomatyczne”, kiedy zostały napisane!
Uday Reddy
1
Jeśli chodzi o zdrową konkurencję, jednym kluczowym problemem jest to, że istnieje tak wiele podejść, formalizmów, badaczy i prac, że trudno jest nadążyć za rozwojem. Jako społeczność badawcza warto poświęcić trochę czasu na syntezę i ujednolicenie istniejących podejść.
Martin Berger
2
@MartinBerger, punktem wyjścia, którego jestem świadomy, jest artykuł Patricka Cousota „Konstruktywny projekt hierarchii semantyki”, który pokazuje, że bardzo szeroki zakres modeli semantycznych, w tym systemy przejściowe, semantyka aksomatyczna, modele denotacyjne, można powiązać za pomocą kombinacji, stąd postrzegane jako różne abstrakcje.
Vijay D
12

[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ę.

Uday Reddy
źródło
10

[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ć.

Uday Reddy
źródło
Przepraszamy za brak odpowiedzi na prośbę o czat. Jestem bardzo zajęty przez następne dwa tygodnie. Dziękuję za napisanie tego! To pierwsza techniczna odpowiedź na stronie, którą rozumiem.
Vijay D
Przy tej okazji mogę podłączyć wtyczkę do naszej Midlands Graduate School in Theoretical Computer Science, która ma na celu rozwiązanie wszystkich tego rodzaju problemów. Jest otwarty dla wszystkich doktorantów z dowolnego miejsca na świecie.
Uday Reddy,
9

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 ]

Uday Reddy
źródło