Kodowanie semantyczne

Kodowanie semantyczne to tłumaczenie między językami formalnymi . Dla programistów najbardziej znaną formą kodowania jest kompilacja języka programowania do kodu maszynowego lub kodu bajtowego. Konwersja między formatami dokumentów to także formy kodowania. Kompilacja TeX lub LaTeX do PostScript to również powszechnie spotykane procesy kodowania. Niektóre preprocesory wysokiego poziomu, takie jak Camlp4 firmy OCaml , obejmują również kodowanie jednego języka programowania w innym.

Formalnie zakodowanie języka A w język B jest odwzorowaniem wszystkich terminów A w B. Jeśli istnieje zadowalające zakodowanie A w B, B jest uważane za co najmniej tak potężne (lub przynajmniej tak wyraziste ) jak A.

Nieruchomości

Nieformalne pojęcie tłumaczenia nie jest wystarczające, aby pomóc określić ekspresyjność języków, ponieważ pozwala na trywialne kodowanie, takie jak mapowanie wszystkich elementów A na ten sam element B. Dlatego konieczne jest określenie definicji „wystarczająco dobrego” kodowania . To pojęcie różni się w zależności od zastosowania.

Zwykle oczekuje się, że kodowanie ${\ Displaystyle [\ cdot]: A \ longrightarrow B}$ zachowa szereg właściwości.

Konserwacja kompozycji

solidność: $Dla$ każdego n-arnego operatora $,$ -arnego że; ${\ Displaystyle \ forall T_ {A} ^ {1}, T_ {A} ^ {2} ,\kropki ,T_{A}^{n},[op_{A}(T_{A}^{1},T_{A}^{2},\cdots ,T_{A}^{n})] =op_{B}([T_{A}^{1}],[T_{A}^{2}],\cdots ,[T_{A}^{n}])} kompletność Dla każdego n-$
argumentowego: operatora ${\ displaystyle op_ {A}}$ z A istnieje operator n-ary $z$ ,; ${\ Displaystyle \ forall T_ {B} ^ {1}, T_ {B} ^ {2}, \ kropki, T_ {B} ^ {n},\istnieje T_{A}^{1},\kropki,T_{A}^{n},op_{B}(T_{B}^{1},\cdots,T_{B}^{ N})=[op_{A}(T_{A}^{1},T_{A}^{2},\cdots,T_{A}^{n})]}$

(Uwaga: o ile autor jest świadomy, to kryterium kompletności nigdy nie jest stosowane.)

Zachowanie kompozycji jest przydatne, o ile gwarantuje, że komponenty można badać osobno lub razem bez „zrywania” jakiejkolwiek interesującej właściwości. W szczególności w przypadku kompilacji solidność ta gwarantuje możliwość przeprowadzenia oddzielnej kompilacji komponentów, natomiast kompletność gwarantuje możliwość dekompilacji.

Zachowanie redukcji

Zakłada to istnienie pojęcia redukcji zarówno w języku A, jak iw języku B. Zazwyczaj w przypadku języka programowania redukcja jest relacją, która modeluje wykonanie programu.

Piszemy $kroku$ redukcji i $.$ dowolnej liczby kroków

solidność: Dla każdego terminu języka A, jeśli $Displaystyle T_ {\ Displaystyle T_ {1}, T_$ $} A} ^ {1} \ longrightarrow ^ {*} T_ {A} ^ {2}}$ następnie ${\ Displaystyle [T_ {A} ^ {1}] \ longrightarrow ^ {*}[T_{A}^{2}]}$ .
kompletność: Dla każdego terminu ${\ Displaystyle T_ {A} ^ {1}}$ języka A i wszystkich terminów ${\ Displaystyle T_ {B} ^ {2}}$ języka B, jeśli ${\ Displaystyle [T_ {A} ^ {1}] \ longrightarrow ^ {*} T_ {B} ^ {2}}$ to istnieje takie, że ${\ Displaystyle T_ {A} ^ {2}}$ ${\ Displaystyle T_ {B} ^ {2} = [T_ {A} ^ {2}]}$ .

To zachowanie gwarantuje, że oba języki zachowują się w ten sam sposób. Poprawność gwarantuje zachowanie wszystkich możliwych zachowań, podczas gdy kompletność gwarantuje, że żadne zachowanie nie zostanie dodane przez kodowanie. W szczególności w przypadku kompilacji języka programowania solidność i kompletność łącznie oznaczają, że skompilowany program zachowuje się zgodnie z semantyką wysokiego poziomu języka programowania.

Zachowanie wypowiedzenia

Zakłada to również istnienie pojęcia redukcji zarówno w języku A, jak i języku B.

solidność: $}}$ dowolnego terminu $się$ zbiegają , to wszystkie redukcje zbiegają się $A$ .
kompletność: dla dowolnego terminu , jeśli wszystkie redukcje z $\ Displaystyle$ $[T_ {A}]} są$ wszystkie redukcje ${\ displaystyle T_ {A}}$ zbiegają się.

W przypadku kompilacji języka programowania solidność gwarantuje, że kompilacja nie wprowadza niezakończeń, takich jak nieskończone pętle lub nieskończone rekurencje. Właściwość kompletności jest przydatna, gdy język B jest używany do badania lub testowania programu napisanego w języku A, prawdopodobnie poprzez wyodrębnienie kluczowych części kodu: jeśli to badanie lub test dowodzi, że program kończy się w B, to kończy się również w A.

Przechowywanie obserwacji

Zakłada to istnienie pojęcia obserwacji zarówno w języku A, jak iw języku B. W językach programowania typowymi obserwablami są wyniki wejść i wyjść, w przeciwieństwie do czystych obliczeń. W języku opisu, takim jak HTML , typowa obserwacja jest wynikiem renderowania strony.

solidność: dla każdego obserwowalnego $warunków$ istnieje obserwowalny ${\ displaystyle obs_ {B}}$ takich, że dla dowolnego terminu ${\ displaystyle T_ {A}}$ z obserwowalnym ${\ Displaystyle obs_ {A}}$ , ${\ Displaystyle [T_ {A}]}$ ma obserwowalny ${\ displaystyle obs_ {B}}$ .
kompletność: dla każdego obserwowalnego ${\ Displaystyle [T_ {A}]}$ $b$ obserwowalny B taki, że dla dowolnego terminu $}}$ z obserwowalnym ${\ Displaystyle obs_ {B}}$ , ${\ Displaystyle T_ {A}}$ ma obserwowalny ${\ displaystyle obs_ {A}}$ .

Zachowanie symulacji

Zakłada to istnienie pojęcia symulacji zarówno w języku A, jak iw języku B. W jednym języku programowania program symuluje inny, jeśli może wykonać wszystkie te same (obserwowalne) zadania i ewentualnie kilka innych. Symulacje są zwykle używane do opisywania optymalizacji czasu kompilacji.

$, T_ {A} ^ {2}}$ ZA ${A} ^ {2}}$ , jeśli symuluje ${\ Displaystyle T_ {A} ^ {1}}$ następnie ${\ Displaystyle [T_ {A} ^ {2}]}$ symuluje ${\ Displaystyle [T_ {A} ^ {1}]}$ .
T
kompletność: dla każdego warunku ${\ Displaystyle T_ {A} ^ {1}, T_ {A} ^ {2}}$ , jeśli symuluje ${\ Displaystyle [T_ {A} ^ {2}]}$ ${\ Displaystyle [T_ {A} ^ {1}]}$ następnie ${\ Displaystyle T_ {A} ^ {2}}$ symuluje ${\ Displaystyle T_ {A} ^ {1} }$ .

Zachowanie symulacji jest znacznie silniejszą właściwością niż zachowanie obserwacji, z którym się wiąże. Z kolei jest słabsza niż właściwość zachowania bisymulacji . Podobnie jak w poprzednich przypadkach, solidność jest ważna dla kompilacji, podczas gdy kompletność jest przydatna do testowania lub udowadniania właściwości.

Zachowanie równoważności

Zakłada to istnienie pojęcia równoważności zarówno w języku A, jak i języku B. Zazwyczaj może to być pojęcie równości ustrukturyzowanych danych lub pojęcie składniowo różnych, ale semantycznie identycznych programów, takich jak kongruencja strukturalna lub równoważność strukturalna.

solidność: $[ T_ {A} ^ {1}]}$ jeśli dwa terminy $1$ równoważne $A$ to i ${\ Displaystyle [T_ {A} ^ {2}]}$ są równoważne w B.
kompletności: , jeśli dwa terminy ${\ Displaystyle [T_ { A}^{1}]}$ i ${\ Displaystyle [T_ {A} ^ {2}]}$ są równoważne w B, a następnie ${\ Displaystyle T_ {A} ^ {1}}$ i ${\ Displaystyle T_ {A} ^{2}}$ są równoważne w A.

Zachowanie dystrybucji

Zakłada to istnienie pojęcia dystrybucji zarówno w języku A, jak iw języku B. Zazwyczaj w przypadku kompilacji programów rozproszonych napisanych w Acute, JoCaml lub E oznacza to dystrybucję procesów i danych między kilka komputerów lub procesorów.

solidność: $,$ termin jest złożeniem dwóch ${\ Displaystyle T_ {A} ^ {1} ~ | ~ T_ {A} ^ {2}}$ wtedy ${\ Displaystyle [T_ {A}]}$ musi być kompozycją dwóch agentów ${\ Displaystyle [T_ {A} ^ {1}] ~ | ~ [T_ {A} ^ {2}]}$ .
kompletność: , jeśli termin ${\ Displaystyle [T_ {A}]}$ to kompozycja dwóch agentów ${B} ^ {2}}$ $to$ musi być kompozycja dwóch agentów ${\ Displaystyle T_ {A} ^ {1} ~ | ~ T_ {A} ^ {2}}$ takie, że ${\ Displaystyle [T_ {A} ^ {1}] = T_ {B} ^ {1}}$ i ${\ Displaystyle [T_ {A} ^ {2}] = T_ {B }^{2}}$ .

Zobacz też

Linki zewnętrzne

Wiki o transformacji programu