Jaka jest różnica między znaczeniem a denotacją?

W semantyce języka programowania często słyszy się, że ludzie mówią o znaczeniu i denotacji . Nie wydają się być tacy sami. Jaka jest różnica? Czy ta pierwsza jest związana z semantyką operacyjną, a druga z semantyką denotacyjną? Dzięki.

„Znaczenie” jest używane w szerszym znaczeniu niż w denotacji.

Oryginalna dychotomia, odziedziczona z logiki i filozofii, znajduje się między „sensem” a „denotacją” (które filozofowie nazywają „odniesieniem”).

To rozróżnienie można zilustrować oryginalnym przykładem Frege'a. Zauważył, że zwroty „gwiazda poranna” i „gwiazda wieczorna” odnoszą się do tego samego obiektu --- planety Wenus --- ale zdanie „gwiazda poranna i gwiazda wieczorna to ta sama planeta” faktycznie przekazuje pewne informacje do czytelnika. Zasugerował, że znaczenie wyrażenia rzeczownikowego może wykraczać poza rzeczywisty przedmiot, który oznacza, w tym coś o tym, jak przedstawia przedmiot, który oznacza.

Podobnie w języku programowania wyrażenie nie jest tym samym, co wyrażenie 56 , chociaż mogą być (powinny być!) Całkowicie nie do odróżnienia przez żaden program kliencki. Ale mimo że są nierozróżnialne , to nie są takie same - podczas oceny dwóch programów, w pierwszym przypadku twoja maszyna się zwielokrotnia, a nie w drugim.$8 \times 7$$56$

Budując semantykę denotacyjną, staramy się zbudować model języka, w którym programy nierozróżnialne oznaczają --- odnoszą się do --- tego samego obiektu matematycznego. Celem jest uproszczenie rozumowania na temat zachowania programów, ponieważ możemy rozumować o oznaczeniach, obiektach matematycznych, bez konieczności martwienia się o szczegóły prezentacji programu. Pozwala nam to uniknąć konieczności zajmowania się aspektami znaczenia programów, które nas nie interesują.

Sposób, w jaki sens i denotacja odnoszą się do semantyki operacyjnej, jest bardziej skomplikowany i inny. Mogę rozszerzyć swoją odpowiedź później, aby to opisać, ale muszę teraz pobiec. :)

EDYCJA: OK, teraz rozszerzam tę odpowiedź.

Związek między „denotacją” a „referencją” jest dość dokładny i jest dokładny, ponieważ ludzie, którzy wymyślili semantykę denotacyjną (np. Scott i Strachey) dość świadomie przyswajali idee z logiki filozoficznej w ramach swojego projektu.

Aby zrozumieć związek między znaczeniem i semantyką operacyjną, warto przypomnieć pojęcie filozofii Michaela Dummetta o „teorii znaczenia” i tym, jak różni się ona od „teorii semantycznej”.

W terminologii Dummetta teoria semantyczna jest kompozycyjnym sposobem powiązania zdań z wyznaczonymi obiektami matematycznymi. Logicznie sens zdania jest jego wartością prawdy i jest określany na podstawie wartości prawdy jego składników. Denotacyjna semantyka języków programowania wykorzystuje znacznie szerszą różnorodność obiektów matematycznych, ale działa w ten sam sposób - podajemy znaczenie terminu programowego w znaczeniu jego podtermów. Tak więc w terminologii Dummetta semantyka denotacyjna oferuje semantyczne teorie języków programowania.

Sens-teoria jest też kompozycyjny sposób odnoszenia się do obiektów matematycznych zdań, ale dodatkowo zawiera relację z tego, co uzasadnia związek między zdaniu i obiektu matematycznego. Rozwinął tę ideę, aby zrozumieć, jak intuicyjni matematycy rozumieli pojęcie prawdy. W szczególności mieli oni kompozycyjny opis znaczenia logicznych łączników, ale nie nadali im wartości semantycznych w taki sam sposób, jak robią to logicy klasyczni. Na przykład w rachunku intuicyjnej logiki Brouwera-Heytinga-Kołmogorowa prawdę definiuje się w następujący sposób:

• Kanoniczne dowód jest para ( P 1 , P 2 ) , w którym P 1 jest kanoniczna dowód A i P 2 jest kanoniczna dowód B .$A \land B$$(p_1, p_2)$$p_1$$A$$p_2$$B$
• Dowód kanoniczny jest parą ( i , p ) , gdzie i wynosi 0 lub 1 , a jeśli i wynosi 0 , to p jest kanonicznym dowodem A , a jeśli i wynosi 1 , to p jest kanoniczny dowód B .$A \vee B$$(i, p)$$i$$0$$1$$i$$0$$p$$A$$i$$1$$p$$B$
• Kanoniczne dowodem jest skuteczna procedura, która zajmuje żadnego kanonicznego dowód A i oblicza kanoniczną dowód B .$A \to B$$A$$B$
• Kanoniczny dowód $\forall x.\;A(x)$$n$$A(n)$
• $\exists x.\;A(x)$$(n, p)$$n$$p$$A(n)$

$A$$A$

Zauważmy, że ta definicja łączy zdania i wartości prawdy, ale połączenie musi być uzasadnione możliwością podania kanonicznych dowodów.

Semantyka operacyjna wchodzi w obraz dzięki temu pojęciu uzasadnienia. Semantyka operacyjna to tylko opis działania abstrakcyjnej maszyny. Po podaniu semantyki denotacyjnej ogólnie chcemy pokazać, że semantyka denotacyjna jest wierna semantyce operacyjnej. Właściwość ta nazywa się adekwatnością (wraz z pełną abstrakcją starszego brata ) i dokładnie sprowadza się do podania teorii znaczeń, która łączy abstrakcyjne stany maszyny z obiektami denotacyjnymi, która jest zamknięta pod redukcją maszyny abstrakcyjnej.

To właściwie nie jest cała historia, ponieważ przedstawiłem tutaj, jak połączyć podejścia operacyjne i denotacyjne za pomocą modelu wykonalności. Teorie typów mogą mieć również semantykę teoretyczną (faktycznie ta perspektywa najbardziej interesowała Dummetta), ale nie wyjaśniłem tego związku w tym poście.