Jaki jest cel abstrakcyjnej interpretacji w językach programowania?

Próbuję teraz lepiej zrozumieć, czym jest „abstrakcyjna interpretacja” w językach programowania. Znalazłem dobry rozdział w książce, który wyjaśnia pomysł rozszerzenia dziedziny o najmniej ustalony element, cztery aksjomaty, które dają stały punkt dla funkcji ciągłej i tak dalej. Rozumiem te szczegóły techniczne (choć nie jestem całkiem pewien, do czego dokładnie odnosi się „interpretacja abstrakcyjna” w całym tym schemacie).

Nie jestem pewien, co motywuje stosowanie interpretacji abstrakcyjnej? Czy to tylko identyfikacja stałych punktów dla funkcji obliczalnych? Czy główną motywacją jest rekursja w większości języków programowania?

Byłbym również szczęśliwy, gdyby uzyskać ogólny przegląd, który jest wystarczająco głęboki technicznie dla kogoś, kto ma wykształcenie informatyczne. Uważam, że strona Wikipedii jest raczej niepokojąca.

Interpretacja abstrakcyjna jest bardzo ogólną koncepcją i w zależności od tego, kogo zapytasz, otrzymasz różne wyjaśnienia, ponieważ wszechstronne koncepcje dopuszczają wiele perspektyw. Widok w tej odpowiedzi jest mój i nie zakładam, że jest ogólny.

Twardość obliczeniowa jako motywacja

Zacznijmy od problemów decyzyjnych, których rozwiązania mają następującą strukturę:

Procedura ma często dolną granicę twardości NP. Sprawdzanie właściwości semantycznych programów jest nawet nierozstrzygalne. Co możemy zrobić?

Zróbmy dwie obserwacje. Po pierwsze, czasami możemy rozwiązać określone przypadki problemów, nawet jeśli nie jesteśmy w stanie rozwiązać ogólnego problemu. Po drugie, aplikacje takie jak optymalizacja kompilatora tolerują aproksymację, ponieważ kompilator, który eliminuje niektóre, ale nie wszystkie źródła nieefektywności, jest użyteczny. Aby sprecyzować tę intuicję, musimy odpowiedzieć:

1. Co to znaczy formalnie rozwiązać niektóre, ale nie wszystkie przypadki problemów?
2. Jakie jest przybliżone rozwiązanie problemu decyzyjnego?

Streszczenie interpretacji Pomysł 1: Zmień opis problemu

Dla mnie głównym wglądem w abstrakcyjną interpretację jest zmiana sformułowania problemu, aby zamiast pytać o odpowiedź Tak / Nie , prosimy o odpowiedź Tak / Nie / Może .

W rezultacie każdy problem ma trywialne, stałe rozwiązanie czasowe ( być może wyjście ). Możemy teraz skupić się na opracowaniu procedury, która nie zawsze daje Może . Aby powrócić do powyższych pytań, rozwiązanie, które działa w przypadku niektórych problemów, to takie, które powraca Może w przypadku problemów, których nie może rozwiązać. Co więcej, być może jest to przybliżenie odpowiedzi Tak i Nie, ponieważ nie jesteśmy pewni, jaka jest odpowiedź.

Ten pomysł nie ogranicza się do problemów decyzyjnych. Rozważ te problemy dotyczące programów.

1. Które wiersze kodu w programie są martwe (nigdy nie zostaną wykonane)?
2. Które zmienne w programie mają stałe wartości?
3. Które twierdzenia w programie są naruszane?

We wszystkich tych sytuacjach możemy przejść od rozwiązania dokładnego do przybliżonego, rozważając rozwiązania, które mają pewną niepewność.

1. Co to jest zestaw wierszy kodu, który jest martwy?
2. Co to jest zestaw zmiennych w programie, które mają stałe wartości?
3. Jaki zestaw twierdzeń w programie nie jest naruszony?

Wyprodukowane zestawy nie muszą być największe. Ten pomysł jest bardzo ogólny i dotyczy problemów, które mają niewiele wspólnego z analizą programu.

1. Zamiast dodawać $m$ i $n$, możemy poprosić o zasięg $[a,b]$ w której leży suma.
2. Zamiast mnożenia $m$ przez $n$ możemy poprosić $k$ bity wyniku (konkretne, typowe przykłady to znak lub bit parzystości).
3. Zamiast pytać o satysfakcjonujące przypisania do formuły, możemy poprosić o zestaw zawierający satysfakcjonujące przypisania.

Zauważ, że nie tylko zmieniliśmy problem, ale także ściśle go uogólniliśmy, ponieważ rozwiązanie pierwotnego problemu jest nadal rozwiązaniem zmodyfikowanego problemu. Najważniejsze pytanie, na które obecnie nie ma odpowiedzi, brzmi: jak znaleźć przybliżone rozwiązanie?

Streszczenie Interpretacja Pomysł 2: Charakterystyka stałoprzecinkowa oryginalnych rozwiązań

Drugim wielkim pomysłem jest zaobserwowanie, że zestaw rozwiązań wielu problemów charakteryzuje się jako stały punkt w sieci rozwiązań kandydujących. Na przykład załóżmy, że masz wykres i chcesz wiedzieć, czy wierzchołek$t$ jest osiągalny z wierzchołka $s$. Możemy to rozbić na znalezienie zestawu$\mathit{Reach}(s)$ wszystkich wierzchołków osiągalnych z $s$ a następnie sprawdzanie, czy $t$jest w tym zestawie. Możemy dalej to zaobserwować$\mathit{Reach}(s)$ jest najmniejszym rozwiązaniem równania:

$X = \{s\} \cup \{ w ~|~ v \text{ is in } X \text{ and } (v,w) \text{ is an edge}\}$

Wartość charakterystyki punktu stałego polega na tym, że dokładne rozwiązanie można postrzegać jako granicę szeregu przybliżeń. W tym przykładzie$n$-tym elementem serii jest zbiór wierzchołków wykresu osiągalny w $n$ kroki od $s$ a aproksymacja jest podzbiorem tych wierzchołków.

Charakterystyka punktu stałego jest decyzją projektową. Istnieje wiele różnych charakterystyk zestawu rozwiązań. Każdy z nich może mieć inne zalety. W przypadku języków programowania mamy więcej struktury niż tylko posługiwanie się wykresem. Równania punktów stałych, na których nam zależy, można zdefiniować przez indukcję struktury programu wejściowego. Ten pomysł nie jest specyficzny dla programów. Stosując abstrakcyjną interpretację do elementów języka strukturalnego, takich jak gramatyka, formuła logiczna, program, wyrażenie arytmetyczne itp., Możemy zdefiniować punkty stałe poprzez indukcję struktury jakiegoś obiektu syntaktycznego.

Podając tę ​​charakterystykę punktu stałego, zobowiązujemy się do określonego sposobu obliczania rozwiązań. W rzeczywistości nie obliczymy tego stałego punktu, ponieważ jest on co najmniej tak trudny jak rozwiązanie pierwotnego problemu, co prowadzi nas do następnego kroku.

Streszczenie interpretacji Pomysł 3: Przybliżenie punktu stałego

Zamiast obliczać stały punkt funkcji $F$ w kratkę $L$, możemy obliczyć stały punkt innej funkcji $G$ w kratkę $M$. Pod warunkiem spełnienia określonych warunków dotyczących$M$ do $L$, rozwiązanie obliczone w $M$ gwarantuje się, że jest przybliżeniem rozwiązania w $L$. Jest to jeden z podstawowych wyników abstrakcyjnej interpretacji, zwany zwykle twierdzeniem o przeniesieniu punktu stałego . Warunek solidności wynika albo z połączeń Galois, albo ze słabszych ustawień obejmujących funkcje abstrakcji lub konkretyzacji, lub relacji poprawności.

Twierdzenie o przeniesieniu punktu stałego gwarantuje, że nie musisz udowadniać, że obliczasz przybliżenie dźwięku przy każdym projektowaniu analizy przybliżonej. Musisz tylko udowodnić, że kraty$L$ (zawierający oryginalne rozwiązania) i $M$ (zawierające przybliżenia) i funkcje $F$ i $G$spełniają pewne ograniczenia. To wielka wygrana, jeśli jesteś projektantem analizy i zależy ci na solidności.

Intuicja stojąca za przeniesieniem punktu stałego może być wnikliwa. Możemy uznać punkt stały za granicę (ewentualnie transfinitowego) łańcucha elementów. Obliczanie przybliżonych rozwiązań sprowadza się do przybliżenia tego limitu, co możemy zrobić, przybliżając elementy łańcucha.

Pojęcie przybliżenia zależy od zastosowania. Jeśli używasz zasięgu wykresu do planowania podróży, możesz zaakceptować przybliżenie, które mówi, że nie ma drogi między nimi$s$ i $t$ nawet jeśli istnieje ścieżka, ale nie będziesz szczęśliwy, jeśli algorytm mówi, że istnieje ścieżka $s$ do $t$ gdzie nie ma ścieżki.

Streszczenie Interpretacja Idea 4: Algorytmy aproksymacji stałoprzecinkowej

Wszystko, co widzieliśmy do tej pory, było matematycznym wynikiem istnienia. Ostatnim krokiem jest obliczenie przybliżenia. Kiedy sieć aproksymacji jest skończona (lub jeśli warunek łańcucha rosnącego / malejącego) jest spełniony, możemy zastosować prostą procedurę iteracyjną. Jeśli sieć jest nieskończona, procedura iteracyjna może nie wystarczyć, choć obliczenie stałego punktu może być nadal rozstrzygalne. W tej sytuacji stosuje się wiele technik w celu dalszego przybliżenia rozwiązania lub przeskoczenia do konkretnego rozwiązania szybciej niż naiwny algorytm iteracji. W kontekście obliczania rozwiązania słyszysz takie terminy, jak poszerzenie , zawężenie , iteracja strategii , przyspieszenie itp.

Podsumowanie

Moim zdaniem abstrakcyjna interpretacja stanowi matematyczną podstawę pojęcia abstrakcji w taki sam sposób, jak logika matematyczna stanowi matematyczną podstawę rozumowania. Rozwiązania wielu problemów, na których nam zależy, mają charakterystykę jako punkty stałe. Ta obserwacja nie ogranicza się do problemów z językiem programowania, a nawet do informatyki. Przybliżone rozwiązania można scharakteryzować jako przybliżenia punktów stałych i są one obliczane za pomocą specjalistycznych algorytmów. Te charakterystyki i algorytmy wykorzystają strukturę wystąpienia problemu. W przypadku programów struktura ta wynika ze składni języka.

Obliczanie przybliżeń problemów, które nie mają naturalnych wskaźników, jest sztuką stale rozwijaną i udoskonalaną przez praktyków. Interpretacja abstrakcyjna jest jedną z teorii matematycznych dla nauki stojącej za tą sztuką.

Odniesienia Istnieje kilka dobrych samouczków na temat interpretacji abstrakcyjnej, które można przeczytać.

1. Przypadkowe wprowadzenie do abstrakcyjnej interpretacji , Patrick Cousot (Wspólna praca z Radhią Cousot), Warsztaty nt. Biologii systemowej i metod formalnych (SBFM'12)
2. Delikatne wprowadzenie do formalnej weryfikacji systemów komputerowych poprzez abstrakcyjną interpretację , Patrick i Radhia Cousot, Marktoberdorf Summer School 2010.
3. Wykład 13: Abstrakcja Część I , Patrick Cousot, Abstrakcyjna interpretacja, Kurs MIT.
4. Wstęp do interpretacji abstrakcyjnej , Samson Abramsky i Chris Hankin, Abstract Interpretation of Declarative Languages, 1987.
5. Abstrakcyjna interpretacja i zastosowanie do programów logicznych , Patrick i Radhia Cousot, 1992. Dwie pierwsze sekcje zawierają ogólny przegląd wysokiego poziomu z kilkoma przykładami.

Zgadzam się, że często trudno jest wydobyć główny punkt ze wszystkich tych szczegółów. (W rzeczywistości moim wielkim problemem przy każdym traktowaniu abstrakcyjnej interpretacji, jaką widziałem, jest to, że prezentują tyle maszyn bez motywowania.)

Oto jak o tym myślę:

Interpretacja abstrakcyjna uruchamia programy w przybliżeniu na dużych zestawach danych naraz.

Nie obejmuje to wszystkiego, ale ogólnie dobrze się trzyma.

Przykładem kanonicznym jest ocena wyrażeń arytmetycznych w celu ustalenia znaku wyniku. Możesz sobie wyobrazić hipotetyczną, nieskończenie szybką maszynę, która potrafi ocenić wyrażenie na każdym pozytywnym wejściu i zwrócić zestaw wyników. Jeśli miałeś jedną z nich, możesz w zasadzie określić rzeczy takie jak „ten program zwraca liczby dodatnie, gdy podane są liczby dodatnie”.

Ale oczywiście nie masz tej maszyny. Utkniesz w prawdziwym życiu, więc musisz albo zrobić to samo symbolicznie , co może czasem dać dokładne odpowiedzi, ale często nie, lub w przybliżeniu w sposób, który zawsze zwraca odpowiedzi, ale mogą nie być dokładne. To drugie robi abstrakcyjna interpretacja.

Nie możesz nawet reprezentować zestawu wszystkich liczb dodatnich bezpośrednio. Zamiast tego potrzebujesz abstrakcji tego zestawu. Musisz także wyodrębnić liczby ujemne i zero. W efekcie powstaje rodzina skończonych zestawów abstrakcyjnych$\{neg,zero,pos\}$, które reprezentują konkretne zestawy$\{\{...,-2,-1\},\{0\},\{1,2,...\}\}$.

Teraz możesz wymyślić reguły, takie jak „dodanie dwóch liczb dodatnich daje liczbę dodatnią” lub $add : pos \times pos \to pos$. Wymyśl reguły dla każdego z prymitywów języka i możesz udawać, że oceniasz wyrażenia arytmetyczne na dużych zestawach danych wejściowych jednocześnie.

Oczywiście reguła „dodawanie liczby dodatniej i ujemnej” sprawi ci kłopotu, ponieważ takie uzupełnienia mogą zwrócić wszystko. Abstrakcyjna struktura interpretacji pomaga tutaj: mówi, że powinieneś zwrócić możliwie jak najściślejsze przybliżenie dźwięku . Jeśli twoje reguły są prawidłowe i mówią, że dodanie zwraca coś w zbiorze abstrakcyjnym, każda konkretna ocena powinna zwrócić liczbę w odpowiednim konkretnym zbiorze. Na przykład$add : pos \times pos \to pos$ zasada jest zdrowa, jeśli $add(a,b)$ jest pozytywny dla każdego pozytywnego $a$ i $b$. Również,$pos \times neg \to (pos \sqcup zero \sqcup neg)$ jest dźwiękiem, gdzie „$\sqcup$„to operacja unii zbiorów abstrakcyjnych.

Wierzę, że nawet najmłodszy badacz PL mógłby po południu zakodować taką abstrakcyjną interpretację. W rzeczywistości nie jest to takie trudne i powinieneś spróbować, zanim przeczytasz więcej, aby poznać podstawy. Gdy to zrobisz, odkryjesz, że twoje abstrakcyjne zestawy wymagają pewnego pojęcia przecięcia (oznaczonego jako „$\sqcap$„) i podzbiór (oznaczony jako„$\sqsubseteq$„). Powinny one odpowiadać konkretnemu przecięciu i podzbiorowi.

Jeśli chcesz udowodnić, że twoja abstrakcyjna interpretacja jest tak ścisła, jak to możliwe, będziesz chciał, aby związek Galois sformalizował tę korespondencję. Samo posiadanie zapewnia, że ​​dla każdego konkretnego zestawu istnieje ścisły zestaw abstrakcyjny.

Jeśli chcesz pracować z językiem z pętlami lub rekurencją, twoje programy mogą się nie kończyć, więc będziesz potrzebować $\bot$wartość reprezentująca nieterminację. Musisz „obliczyć” (w sensie matematycznym) konkretne funkcje jako punkty stałe i podobnie obliczyć funkcje abstrakcyjne. Jeśli masz funkcje wyższego rzędu, przekonasz się, że typowa maszyneria topologiczna w ogóle ich nie obsługuje (aplikacja wyższego rzędu zasadniczo nie jest ciągła) i potrzebujesz domen Scott.

IOW, to, co zidentyfikowaliście jako motywację do interpretacji abstrakcyjnej, to tak naprawdę motywacja do maszyny wymaganej do wykonania abstrakcyjnej interpretacji w językach równoważnych Turingowi. Rzeczywistą motywacją jest użyteczne podsumowanie zachowania programów, uruchamiając je na wielu wejściach jednocześnie.