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

29

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?

Hongjin Liang
źródło
1
Możesz podać linki do tych artykułów, które przeczytałeś. Ułatwiłoby to wyjaśnienie, które konkretne przykłady wprowadzają Cię w błąd.
Marc Hamann,
1
Dla relacji logicznych przeczytałem ostatni artykuł Hura i Dreyera „Logiczna relacja Kripkego między ML a montażem” (POPL'11). Przeczytałem również klasyczne rozdziały książki Pierce'a „Zaawansowane tematy w typach i językach programowania”. Uważam, że logiczne relacje są definiowane indukcyjnie na strukturze typu języka, ale co, jeśli język nie ma struktury typu (np. C)? (Wydaje się, że to kolejne pytanie).
Hongjin Liang,
1
Do symulacji przeczytałem oryginalny artykuł „Algebraiczne prawa dla niedeterminizmu i współbieżności” Hennessy i Milnera. „Małe bisimulacje Koutavasa i Wanda do rozumowania programów imperatywnych wyższego rzędu” (POPL'06) są dla mnie niezrozumiałe i nie jestem pewien, dlaczego nazwali swoją metodę „bisimulacją”.
Hongjin Liang,
3
byłoby lepiej, gdybyś zamieścił informacje, które podałeś w komentarzach w poście. Możesz edytować swoje pytanie, klikając link edytuj pod pytaniem.
Kaveh
1
@HongjinLiang: Jeśli nie masz struktury typów (lub jeśli masz typy rekurencyjne), możesz użyć relacji logicznych indeksowanych krokowo - w relacjach logicznych używasz indukcji na typach, a indeksowanie krokowe wywołuje indukcję w krokach obserwacji. Wskaźniki znajdują się w oświadczeniu badawczym Amala Ahmeda: ccs.neu.edu/home/amal/ahmed-research.pdf . (Kolejny przegląd badań nad relacjami logicznymi to przemówienie Dereka Dreyera i jego oświadczenie badawcze: mpi-sws.org/~dreyer/research.pdf ).
Blaisorblade

Odpowiedzi:

20

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.

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

Uday Reddy
źródło
Zastanawiałem się, czy prawdą byłoby powiedzenie, że wspomniana wyżej relacja jest tak zwanym podnoszeniem relacji danym opisującym maszynę. R FF(R)Rfunctor F
Dave Clarke
@DaveClarke Tak, to ten sam pomysł. W stylu definicji Reynoldsa każdy konstruktor typu jest wyposażony w akcję relacyjną, która wiąże, z każdą relacją , odpowiednią relację spełnianie niektórych aksjomatów. W niektórych innych społecznościach chcieliby czerpać z innych zasad, skąd nazywają je podnoszeniem relacji . wytwarzają w procesie będzie działanie związek w sensie Reynoldsa. R : X X F ( R ) : F ( X ) F ( X ) F ( R ) F ( R )FR:XXF(R):F(X)F(X)F(R)F(R)
Uday Reddy
14

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.

Dave Clarke
źródło
Bardzo dziękuję za szczegółowe wyjaśnienie! Przeczytam twoje referencje i spróbuję znaleźć głębokie powiązania / różnice między nimi.
Hongjin Liang
czy jesteś pewien zdania „Pokazujesz, że program P i symulujesz program Q, a ten program Q może symulować program P i masz bisimulację.”? Niech A = (a. (B + c)) + (a.b + ac) i B = a.b + ac, o ile mogę stwierdzić, że A jest podobne do B, B jest podobne do A, ale A i B nie są bisimilar.
András Salamon
@ András: Masz rację. Moje oświadczenie nie jest wystarczająco precyzyjne. Różnicę tę uwydatnia zwrot „Mogą występować pewne dodatkowe warunki”.
Dave Clarke
Hennessy i Milner zdefiniowali trzy rodzaje relacji równoważności w swoim oryginalnym artykule do bisimulacji i podali kilka przykładów ilustrujących ich różnice. Twoje oryginalne stwierdzenie jest w rzeczywistości średnie w ich pracy, które jest słabsze niż bisimulacja i silniejsze niż równoważność śladowa. Nie jestem pewien, która równoważność jest lepsza. Może zależy to od praktycznego zastosowania.
Hongjin Liang
Symulacja jest również stosowana jako technika sprawdzająca w celu ustalenia uściślenia danych między dwoma typami danych. Każdy z tych dowodów symulacji dotyczy całych klas programów. Szczegóły patrz np. [1]. Sugeruje to, że rozróżnienie między tymi dwoma koncepcjami jest jeszcze bardziej rozmyte. [1]: CAR Hoare, He J i JW Sanders. Wcześniejsze zawężenie danych. Information Processing Letters , 25: 71-76, 1987.
Kai
8

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

Vijay D.
źródło
Twoja odpowiedź jest bardzo pomocna w łączeniu pojęć z abstrakcyjną interpretacją. Dziękuję Ci!
Hongjin Liang,
Szczere pytanie: nie jestem ekspertem, ale czy Reynolds (1983, „Typy, abstrakcja i polimorfizm parametryczny”) już nie definiuje relacji logicznych, które są powiązaniami Galois (Sec. 6)? Jedyne różnice, jakie zauważam: nie mówi on terminu „połączenie Galois”, a jedynie równoważne „funktony łączące między rzędami częściowymi uważanymi za kategorie”, a ogranicza się do domen. OTOH, Backhouse i Backhouse cytują Reynoldsa, ale nie omawiają tego twierdzenia, w ten czy inny sposób.
Blaisorblade,
6

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.

π

Martin Berger
źródło
Twoje referencje są naprawdę miłe! Nie słyszałem wcześniej o logicznych relacjach dla współbieżnych programów. Dziękuję Ci! Wydaje mi się, że trudność w zdefiniowaniu relacji logicznej polega na znalezieniu struktury typu. Przy tej samej strukturze typu można zdefiniować relację logiczną między różnymi językami programowania. Z drugiej strony symulacja wymaga programów do modelowania przez system zmiany stanu, co może być trudne, jeśli programy są napisane dla różnych modeli stanów.
Hongjin Liang
Dzień dobry! Tak, znalezienie odpowiedniej struktury typu może nie zawsze być łatwe. Możesz zdefiniować symulacje za pomocą różnych układów przejściowych dla dwóch rachunków, które chcesz porównać. Można argumentować, że definicja słabej symulacji właśnie to robi. Wszystko, czego naprawdę potrzebujesz, aby zdefiniować symulacje, to relacja do porównywania etykiet przejścia.
Martin Berger