Jakie są różnice między relacjami logicznymi a symulacjami?

Jestem początkującym pracującym nad metodami potwierdzającymi równoważność programu. Przeczytałem kilka artykułów na temat definiowania relacji logicznych lub symulacji, aby udowodnić, że dwa programy są równoważne. Ale jestem dość zdezorientowany co do tych dwóch technik.

Wiem tylko, że relacje logiczne są definiowane indukcyjnie, podczas gdy symulacje oparte są na koindukcji. Dlaczego są zdefiniowane w taki sposób? Jakie są ich zalety i wady? Który powinienem wybrać w różnych sytuacjach?

Mam odpowiedź na to pytanie, które może być nowe. W rzeczywistości zastanawiam się nad tym przez ostatnie 6 miesięcy i nie zostało to jeszcze opisane w gazetach.

Ogólna teza jest taka, że ​​zasady rozumowania relacyjnego, takie jak „relacje logiczne”, „symulacje”, a nawet „niezmienniki”, są przejawami abstrakcji danych lub ukrywania informacji. Wszędzie tam, gdzie kryje się informacja, zasady te pojawiają się.

Pierwszymi ludźmi, którzy to odkryli, byli teoretycy automatów. Automaty mają stan ukryty. Potrzebujesz więc uzasadnienia relacyjnego, aby mówić o ich równoważności. Teoretycy automatów zmagali się z homomorfizmami przez jakiś czas, poddali się i wymyślili pojęcie zwane „relacyjnym pokryciem”, które jest formą relacji symulacyjnych.

Milner podjął ten pomysł w mało znanym, ale bardzo fundamentalnym artykule zatytułowanym „ Algebraiczne pojęcie symulacji między programami ” w 1971 r. Hoare znał go i wykorzystał przy tworzeniu „ Dowodu poprawności reprezentacji danych ” w 1972 r. (Ale wykorzystał abstrakcja funkcjonuje zamiast relacji, ponieważ uważał je za „prostsze”). Później wycofał roszczenie dotyczące prostoty i wrócił do używania relacji w „ Udoskonaleniu udoskonalania danych ”. Reynolds zastosował rozumowanie relacyjne w „ Craft of Programming", Rozdział 5 (1981). Myślał, że relacje są bardziej naturalne i ogólne niż funkcje abstrakcyjne. Jeśli wrócisz i przeczytasz ten rozdział, znajdziesz pomysły relacyjnej parametryczności czające się, czekające na odkrycie. Pewnie, dwa lata później, Reynolds opublikował „Typy, abstrakcja i polimorfizm parametryczny” (1983).

Wygląda na to, że wszystkie te pomysły nie mają nic wspólnego z typami, ale tak naprawdę mają. Stanowe języki i modele mają wbudowaną abstrakcję danych. Nie trzeba definiować „abstrakcyjnego typu danych”, aby ukryć informacje. Po prostu zadeklarujesz zmienną lokalną i ukryjesz ją. Możemy uczyć go studentów pierwszego roku na zajęciach z języka Java w ciągu pierwszych kilku tygodni. Bez potu

Z drugiej strony języki i modele funkcjonalne muszą ukrywać informacje za pomocą typów . Modele funkcjonalne nie mają wbudowanej abstrakcji danych. Musimy dodać to jawnie, używając lub . Jeśli więc przetłumaczysz język stanowy na język funkcjonalny, zauważysz, że cały stan lokalny jest tłumaczony na zmienne typu. Dokładny opis tego, jak to działa, znajduje się w moim artykule „ Obiekty i klasy w językach podobnych do Algolu ”, ale pomysły naprawdę pochodzą z Reynoldsa 1981 („Esencja Algolu”). Właśnie teraz lepiej rozumiemy te klasyczne pomysły.$\forall$$\exists$

Weź dwie maszyny i , które mają być równoważne. Milner 1971 mówi: zdefiniuj relację między stanami i i pokaż, że dwie maszyny zachowują relację. Parametryczność Reynoldsa mówi, pomyśl o stanach maszyn jako należących do typów i . Zdefiniuj relację między nimi. Jeśli maszyny są typu i , sparametryzowane według typów ich stanów, sprawdź, czy te dwie maszyny są powiązane relacją . M ′ M M ′ X X ′ R F ( X ) F ( X ′ ) F ( R $M$$M'$$M$$M'$$X$$X'$$R$$F(X)$$F(X')$$F(R)$

Zatem symulacje i parametryczna relacja to w zasadzie ten sam pomysł . To nie jest tylko powierzchowne podobieństwo. Pierwszy z nich jest przeznaczony dla języków stanowych, w których wbudowana jest abstrakcja danych. Ten drugi jest przeznaczony dla języków bezstanowych, w których pozyskiwanie danych odbywa się za pomocą zmiennych typu.

A co z relacjami logicznymi? Z pozoru logiczne relacje wydają się być bardziej ogólnym pomysłem. Podczas gdy parametryczność mówi o tym, jak powiązać zmienne typu w tym samym modelu, relacje logiczne wydają się odnosić typy w różnych modelach. (Dave Clarke napisał to znakomicie wcześniej). Mam jednak wrażenie (i nadal trzeba to wykazać), że jest to przypadek jakiejś formy parametryczności wyższego typu, która nie została jeszcze sformułowana. Bądź na bieżąco, aby uzyskać więcej postępów na tym froncie.

[Uwaga dodana] Związek między relacjami logicznymi a symulacjami omówiono w naszym najnowszym artykule Relacje logiczne i parametryczność: Program Reynoldsa dla teorii kategorii i języków programowania .

Jedną z kluczowych różnic jest to, że relacje logiczne są stosowane jako technika pokazująca, że ​​klasa programów (np. Dane wejściowe do kompilatora) odpowiada innej klasie programów (np. Dane wyjściowe kompilatora), podczas gdy stosowane są relacje symulacji aby pokazać zgodność między dwoma programami.

Podobieństwo między tymi dwoma pojęciami polega na tym, że oba definiują relację służącą do wykazania zgodności między dwoma różnymi podmiotami. W pewnym sensie relację logiczną można traktować jako relację symulacji zdefiniowaną indukcyjnie na podstawie składni typów. Istnieją jednak różne rodzaje relacji symulacyjnych.

Relacje logiczne mogą być wykorzystane do pokazania zgodności między językiem takim jak ML a jego tłumaczeniem na język asemblerowy, tak jak w czytanym dokumencie. Relacja logiczna jest definiowana indukcyjnie na strukturze typu. Relacja logiczna zapewnia środki kompozycyjne do pokazania, na przykład, że tłumaczenie jest poprawne, poprzez pokazanie, że tłumaczenie jest poprawne dla każdego konstruktora typu. Przy typach funkcji warunek warunku poprawności powiedziałby coś takiego: tłumaczenie tej funkcji przyjmuje dobrze przetłumaczone dane wejściowe na dobrze przetłumaczone dane wyjściowe.

Relacje logiczne są uniwersalną techniką dla języków opartą na rachunku lambda. Inne zastosowania relacji logicznych obejmują ( stąd ): charakteryzowanie definiowalności lambda, powiązanie denotacyjnych definicji semantycznych, charakteryzowanie parametrycznego polimorfizmu, modelowanie abstrakcyjnej interpretacji, weryfikowanie reprezentacji danych, definiowanie w pełni abstrakcyjnej semantyki i modelowanie stanu lokalnego w językach wyższego rzędu.

Relacje symulacyjne są zwykle używane do wykazania równoważności dwóch programów. Zazwyczaj takie programy generują pewien rodzaj obserwacji, na przykład wysyłanie wiadomości w kanałach. Jeden program P symuluje inne Q, jeśli P może zrobić wszystko, co Q może zrobić, chociaż być może więcej.

Z grubsza bisimulacja to dwie relacje symulacji razem. Pokazujesz, że program P i symulacja programu Q oraz że program Q może symulować program P i masz bisimulację, chociaż generalnie występują dodatkowe warunki. Wpis Wikipedii dotyczący bisimulacji jest dobrym (bardziej precyzyjnym) punktem wyjścia. Istnieją tysiące wariantów tego pomysłu, ale jest to fundamentalny pomysł, który został opracowany na nowo w mniej więcej takiej samej formie, jak informatyka, logika modalna i teoria modeli. Artykuł Sangiorgi zawiera wspaniałą historię tego pomysłu.

Jedna praca ustanawiająca związek między tymi dwoma pojęciami to Nota o logicznych relacjach między semantyką i składnią autorstwa Andy'ego Pittsa, która wykorzystuje relacje logiczne, ostatecznie pojęcie semantyczne zdefiniowane syntaktycznie, aby udowodnić pewną właściwość bisimulacji aplikacyjnej , która jest pojęciem czysto syntaktycznym.

Te dwa typy relacji wydają się być stosowane w różnych kontekstach. Symulacje logiczne dla języków pisanych i relacji symulacji w przypadku obliczeń procesowych lub logiki modalnej interpretowanej w systemach przejściowych. Dave Clarke przedstawił wiele intuicyjnych wyjaśnień, więc dodam tylko kilka wskazówek, które mogą pomóc.

Pracowano nad scharakteryzowaniem obu pojęć przy użyciu interpretacji abstrakcyjnej. Może nie być to, czego chcesz, ale przynajmniej oba pojęcia są traktowane w tej samej strukturze matematycznej.

Samson Abramsky wykorzystał relacje logiczne, aby udowodnić prawidłowość i zakończenie analizy ścisłości leniwego rachunku Lambda ( interpretacja abstrakcyjna, relacje logiczne i rozszerzenia Kan ). Pokazał także, że relacje logiczne definiują funkcje abstrakcji w sensie połączenia Galois interpretacji abstrakcyjnej. Niedawno Backhouse i Backhouse pokazali, jak konstruować połączenia Galois dla typów wyższego rzędu z połączeń Galois dla typów bazowych oraz że konstrukcje te można równo opisać za pomocą relacji logicznych ( Relacje logiczne i Połączenia Galois ). Zatem w specyficznym kontekście typowanych języków funkcjonalnych oba pojęcia są równoważne.

Relacje symulacyjne charakteryzują zachowanie własności między strukturami Kripke dla różnych logik modalnych i czasowych. Zamiast typów mamy modalności w logice. Relacje symulacyjne definiują również powiązania Galois, a tym samym abstrakcje. Można zapytać, czy te abstrakcje mają specjalne właściwości. Odpowiedź jest taka, że ​​standardowe abstrakcje są dźwiękowe, a abstrakcje oparte na relacjach symulacji są kompletne. Pojęcie kompletności dotyczy powiązań Galois, które mogą nie być zgodne z interpretacją intuicyjną. Ta linia pracy została opracowana przez Davida Schmidta ( Relacje binarne zachowujące strukturę dla abstrakcji programu ) oraz Francesco Ranzato i Francesco Tapparo ( Uogólnione silne zachowanie przez abstrakcyjną interpretację ).

Powiedziałbym, że te dwa pojęcia są nieco niejasne. Oba dotyczą binarnych relacji mechanizmów obliczeniowych, które w jakiś sposób ucieleśniają pojęcie równości. Relacje logiczne są definiowane przez indukcję struktury typu, podczas gdy symulacje można definiować w dowolny sposób, ale termin ten odnosi się do koindukcji.

$\pi$