Jak leczy się skutki uboczne w semantyce?

W sekcji „Wprowadzenie do języków programowania” Anthony'ego Aaby'ego na temat semantyki dokonuje następujących obserwacji:

Znaczna część pracy w semantyce języków programowania jest motywowana problemami napotkanymi przy próbie konstruowania i zrozumienia programów imperatywnych - programów z poleceniami przypisania. Ponieważ polecenie przypisania ponownie przypisuje wartości do zmiennych, przypisanie może mieć nieoczekiwane skutki w odległych częściach programu.

Uderza mnie to jako niezwykłe przyznanie, że dopuszczenie efektów ubocznych zmotywowałoby większą część pracy w semantyce.

W jaki sposób występowanie efektów ubocznych w języku programowania wpływa na możliwość mapowania programu na model obliczeniowy? Czy istnieją podejścia do zarządzania stanem, które mogą poprawić ten proces, jednocześnie pozwalając na skutki uboczne?

Opierając się na odpowiedzi Charlesa, główną trudnością w teorii języków programowania jest to, że naturalnym pojęciem równoważności programów zazwyczaj nie jest ścisła równość ani w najprostszej semantyce matematycznej, jaką można podać, ani w leżącym u podstaw modelu maszyny. Rozważmy na przykład następujący fragment kodu podobnego do języka Java:

Object x = new Object();
Object y = new Object();
... some more code ...

Tak więc ten program tworzy obiekt i nazywa go x, a następnie tworzy drugi obiekt o nazwie y, a następnie kontynuuje wykonywanie dodatkowego kodu. Załóżmy teraz, że programista decyduje o zmianie kolejności przydziału tych dwóch obiektów:

Object y = new Object();
Object x = new Object();
... some more code ...

Teraz zadaj pytanie: czy to refaktoryzacja zmienia zachowanie programu? Z jednej strony, na bazowej maszynie, xiy zostaną przydzielone w różnych lokalizacjach w dwóch uruchomieniach programu. W tym sensie program zachowuje się inaczej.

Ale w języku podobnym do języka Java można testować odniesienia tylko pod kątem równości, a nie porządku, więc jest to różnica, której „więcej kodu” nie może zaobserwować . W rezultacie większość programistów spodziewa się, że odwrócenie kolejności nie będzie miało wpływu na ostateczną odpowiedź, a większość autorów kompilatorów spodziewa się, że będzie mogła na tej podstawie przeprowadzać zmiany kolejności i optymalizacje. (Z drugiej strony, w C-jak język, to można porównać wskaźniki dla zamawiającego, oddając je do liczb całkowitych pierwszy, a więc takim zamianom czy nie koniecznie zachować zaobserwowania zachowania).

Jednym z głównych pytań semantyki jest odpowiedź na pytanie, kiedy dwa programy są wyraźnie równoważne. Ponieważ nasze pojęcie obserwacji zależy od cech języka programowania, otrzymujemy definicję w rodzaju „dwa programy są równoważne, gdy żaden program kliencki nie jest w stanie obliczyć różnych odpowiedzi na podstawie otrzymania tych programów jako danych wejściowych”. Kwantyfikacja wszystkich programów klienckich sprawia, że ​​to pytanie jest trudne - wydaje się, że ostatecznie musisz powiedzieć coś o wszystkich możliwych programach klienckich, aby powiedzieć coś o dwóch konkretnych fragmentach kodu.

Sztuczka z semantyką denotacyjną polega na podaniu matematycznej interpretacji, która pozwala uniknąć tej uniwersalnej kwantyfikacji - mówisz, że znaczenie fragmentu kodu jest pewną wartością matematyczną, i porównujesz je, sprawdzając, czy są one matematycznie równe lub nie. Jest to lokalne (tj. Kompozycyjne) i nie obejmuje kwantyfikacji wszystkich możliwych klientów. (Musisz wykazać, że semantyka denotacyjna oznacza oczywiście równoważność kontekstową, aby mogła ona brzmieć. Gdy jest kompletna - gdy równość denotacyjna jest dokładnie taka sama jak równoważność kontekstowa, mówimy, że semantyka jest „w pełni abstrakcyjna”.)

Oznacza to jednak, że musisz upewnić się, że semantyka denotacyjna potwierdza te równoważności. W tym przykładzie, jeśli chcesz nadać denotacyjną semantykę dla tego języka podobnego do Javy, musisz upewnić się, że nie tylko wywołanie nowego zabiera stertę i zwraca nową stertę z nowo utworzonym obiektem, ale że znaczenie programu jest niezmienny tak samo we wszystkich permutacjach stosu wejściowego. Może to obejmować dość złożone struktury matematyczne (np. W tym przypadku praca w kategorii, która zapewnia, że ​​wszystko działa modulo w odpowiedniej grupie permutacyjnej).

Istnieją oczywiście sposoby radzenia sobie z efektami w (denotacyjnej) semantyce. Na przykład możemy użyć idei Eugenio Moggiego, że efektami obliczeniowymi są monady (ta idea została również wykorzystana w projekcie Haskell). Jednym z problemów jest to, że monady są trudne do połączenia. Gordon Plotkin i John Power zasugerowali udoskonalenie monad Moggiego do teorii Lawvere'a lub teorii algebraicznych, jak się je nazywa, co obejmuje efekty algebraiczne (najczęstsze efekty to algebraiczne, takie jak stan, operacje we / wy, niedeterminizm, ale kontynuacje są nie). Aby uzyskać kompleksowe leczenie, zobacz tezę Matiji Pretnar .

Powinienem też wspomnieć o możliwej semantyce światów dla stanu lokalnego, opracowanej przez Franka Olesa i Johna Reynoldsa (przepraszam, nie mogę znaleźć lepszego linku, te rzeczy pochodzą z 1982 roku), która poprzedza monady Moggi. Użyli kategorii preheaves, aby uzyskać semantykę języka przypominającego algol, który poprawnie modelował wiele aspektów stanu lokalnego (ale nie wszystkie z nich, myślę, że model pozwalał na snapback, ale może moja pamięć źle mi służy).

Matthias Felleisen przedstawił przekonujące rozwiązanie problemu skutków ubocznych w semantyce w swojej serii „Syntaktyczne teorie kontroli i stanu”.

Ta linia pracy zaowocowała maszyną CESK, prostą abstrakcyjną strukturą maszyny zdolną do zwięzłego modelowania funkcjonalnych, obiektowych, imperatywnych, a nawet logicznych języków. CESK obsługuje nie tylko skutki uboczne, ale także „złożone” konstrukcje kontrolne, takie jak wyjątki, kontynuacje, lenistwo, a nawet wątki.

Maszyna CESK, a szerzej - semantyka operacyjna w szerszym zakresie, są de facto standardem w teorii języków programowania przez około dwie dekady.

Krótko mówiąc, maszyna CESK jest maszyną małostopniową z czterema komponentami do opisania każdego stanu maszyny: ciąg sterujący (uogólnienie licznika programu), środowisko, magazyn (zwany także stertą) i bieżąca kontynuacja.

Środowisko mapuje zmienne na adresy; sklep mapuje adresy na wartości.

Ułatwia to modelowanie zmiennych zmiennych: wystarczy zmienić wartość pod jego adresem.

Ułatwia także modelowanie wskaźników i alokację dynamiczną: po prostu spraw, aby adresy sklepów były najwyższej jakości.

Podobnie kontynuacje pierwszej klasy wynikają z nadania im wartości adresowalnych.

W jaki sposób występowanie efektów ubocznych w języku programowania wpływa na zdolność mapowania programu do modelu obliczeniowego?

Nie musi to utrudniać, ale nakłada ograniczenia na sposób konstruowania semantyki większych wyrażeń z mniejszych. Może bardzo źle oddziaływać z niektórymi innymi konstrukcjami programistycznymi, na przykład, jeśli chce się nadać semantykę denotacyjną w stylu Scotta dla języka umożliwiającego przypisanie funkcji wyższego rzędu do globalnych odniesień.

Problemem są nie tylko skutki uboczne, takie jak stan. Proste języki rozkazujące, takie jak strzeżony język poleceń Dijkstry, mają tego rodzaju skutki uboczne i mają ładną semantykę. Pojawiają się problemy z rozszerzeniami rachunku lambda o rodzaj semantyki operacyjnej oczekiwanej od języków programowania, nawet przy braku efektów ubocznych: najwcześniej, PCF Plotkina, podano modele denotacyjne stosunkowo wcześnie, ale semantyka nie była w pełni abstrakcyjna, co oznacza, że semantyka denotacyjna była zbyt ogólna, nie do końca odpowiadająca semantyce operacyjnej. PCF w końcu uzyskał w pełni abstrakcyjną semantykę denotacyjną pod koniec lat osiemdziesiątych z semantyką gier, która wcale nie przypomina semantyki teoretycznej Scott. Współbieżność nadal nie otrzymała w pełni odpowiedniego traktowania denotacyjnego.

Wielu kwestionuje znaczenie tego rodzaju semantyki. Zawsze możemy zapewnić pewnego rodzaju semantykę operacyjną, nawet jeśli ta „semantyka” jest tylko źródłem programu i nazwami niektórych komputerów, które skompilowały i uruchomiły program: z tego powodu Strachey potępił semantykę operacyjną. Ale semantyka operacji strukturalnych Plotkina pokazała, jak semantykę operacyjną można oddzielić od modeli maszyn, a praca Pitta pokazała, w jaki sposób semantyka może wspierać podobne rozumowanie programów i języków programowania do semantyki denotacyjnej. Tak więc semantyka operacyjna jest realną alternatywą dla semantyki denotacyjnej i została z powodzeniem zastosowana w znacznej liczbie języków programowania, takich jak Standard ML.

Czy istnieją podejścia do zarządzania stanem, które mogą poprawić ten proces, jednocześnie pozwalając na skutki uboczne?

W pewnym stopniu trudności w zapewnieniu semantyki odpowiadają trudnościom w zapewnieniu potężnych języków programowania, które zachowują się tak, jak można by się spodziewać. Pragmatycznie umotywowane decyzje projektowe - takie jak unikanie użycia stanu globalnego razem z współbieżnością, zwykle poprzez współbieżność przekazywania wiadomości - ułatwiają zapewnienie semantyki.