Na jakie pytania semantyka denotacyjna może odpowiedzieć, na co semantyka operacyjna nie może?

Znam semantykę operacyjną (zarówno małą, jak i dużą) do definiowania języków programowania. Interesuje mnie również nauka semantyki denotacyjnej, ale nie jestem pewien, czy będzie to warte wysiłku. Czy po prostu będę uczyć się tego samego materiału z innego punktu widzenia, czy też są spostrzeżenia, które mogę uzyskać tylko dzięki zrozumieniu semantyki denotacyjnej?

Nie ma prawdziwej zgodności, która charakteryzuje semantykę denotacyjną (patrz także ten artykuł), z tym wyjątkiem, że musi być kompozycyjna . Oznacza to, że jeśli jest funkcją semantyczną, odwzorowującą programy na ich znaczenie, coś takiego jak poniżej musi tak być w przypadku wszystkich konstruktorów -arnych programów i wszystkich programów , ..., (domyślnie zakładając typowanie):$\newcommand{\SEMB}[1]{\lbrack\!\lbrack #1 \rbrack\!\rbrack} \SEMB{\cdot}$$n$$f$$M_1$$M_n$

$$\SEMB{f(M_1, ..., M_n)} = trans(f) (\SEMB{M_1}, ..., \SEMB{M_n})$$

Tutaj jest konstruktorem odpowiadającym domenie semantycznej. Kompozycyjność jest podobna do pojęcia homomorfizmu w algebrze.$trans(f)$$f$

Semantyka operacyjna nie jest w tym sensie kompozycyjna. Historycznie semantyka denotacyjna została opracowana częściowo dlatego, że semantyka operacyjna nie była kompozycyjna. Zgodnie z przełomową teoretyczną semantyką denotacyjną porządku D. -calculus D. Scotta , większość semantyki denotacyjnej była teoretyką porządku. Wyobrażam sobie, że - poza czystym interesem intelektualnym - semantyka denotacyjna została w większości wymyślona, ​​ponieważ wówczas (1960):$\lambda$

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

Problem polegał na tym, że pojęcie równości programów nie było tak dobrze rozumiane, jak jest teraz. Argumentowałbym, że oba problemy zostały znacznie złagodzone (1), na przykład poprzez techniki oparte na bisimilacji pochodzące z teorii procesów (które można postrzegać jako specyficzną formę semantyki operacyjnej) lub np. Pitts pracuje nad semantyką operacyjną i programem równoważność, oraz (2) przez rozwój np. logiki separacji lub logiki Hoare'a uzyskanych jako typowane wersje logiki Hennessy-Milnera poprzez osadzenie języka programowania w typach π-rachunku. Zauważ, że logika programu (= semantyka aksjomatyczna) również jest złożona.

Innym sposobem patrzenia na semantykę denotacyjną jest to, że istnieje wiele języków programowania i wszystkie wyglądają trochę podobnie, więc może uda nam się znaleźć prosty, ale uniwersalny metajęzyk i odwzorować wszystkie języki programowania w sposób kompozycyjny na te meta język. W latach 60. XX wieku uważano, że niektóre pisane -calculus są tym meta-językiem. Zdjęcie może zawierać więcej niż 1000 słów:$\lambda$

Jaka jest zaleta tego podejścia? Może warto spojrzeć na to z ekonomicznego POV. Jeśli chcemy udowodnić coś interesującego w klasie programu obiektowego, mamy dwie opcje.

• Udowodnij to bezpośrednio na poziomie obiektu.

• Udowodnij, że tłumaczenie na meta-poziom (iz powrotem) „zachowuje” właściwość, a następnie udowodnij to dla meta-poziomu, a następnie przesuń wynik z powrotem na poziom obiektu.

Łączny koszt tego drugiego jest prawdopodobnie wyższy niż koszt pierwszego, ale koszt udowodnienia tłumaczenia może być amortyzowany dla wszystkich przyszłych zastosowań, podczas gdy koszt udowodnienia właściwości meta-poziomu jest znacznie mniejszy niż koszt dowodu na poziomie obiektu.

Oryginalne podejście teoretyczne do semantyki denotacyjnej do tej pory nie spełniło tej obietnicy, ponieważ skomplikowanym funkcjom językowym, takim jak orientacja obiektowa, współbieżność i obliczenia rozproszone, nie podano jeszcze dokładnej semantyki teoretycznej. Przez „precyzyjny” rozumiem semantykę, która pasuje do naturalnej semantyki operacyjnej takich języków.

---

Czy warto uczyć się semantyki denotacyjnej? Jeśli masz na myśli teoretyczne podejście do semantyki denotacyjnej, prawdopodobnie nie, chyba że chcesz pracować w teorii języków programowania i rozumieć starsze prace. Innym powodem uczenia się teoretycznych podejść do semantyki denotacyjnej jest piękno tego podejścia.

Napiszę za jedyne Ď " tak, że ⟨ p , Ď ⟩ → $O(p,\sigma)$$\sigma'$$\langle p, \sigma \rangle \to \sigma'$$\bot$$D(p)$$p$$O(p,\sigma)=D(p)(\sigma)$$S(p)$$\sigma\mapsto O(p,\sigma)$$D(p)$

Teraz weź kompilator . Powiedzenie, że jest to kompilator oznacza, że ​​zachowuje semantykę, tj. S ( $C:X \to X'$$S(C(p))=S'(p)$$p$$\sigma$$O(C(p),\sigma)=O'(p,\sigma)$$p$$D(C(p))=D'(p)$$\sigma$

Głupi przykład:

$C(p)=$$(q;q')$$(skip;q;skip;q';skip)$

$p$$C$