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