Równoważność analizy przepływu danych, abstrakcyjna interpretacja i wnioskowanie o typie?

Odpowiedź Babou na ostatnie pytanie przypomina mi, że kiedyś myślę, że przeczytałem artykuł na temat równoważności (zarówno pod względem faktów, które można wywnioskować lub udowodnić, jak i złożoności czasowej działania algorytmu wnioskowania) analizy przepływu danych , abstrakcyjna interpretacja i wnioskowanie typu .

W niektórych pod-przypadkach (jak między kontekstową analizą przepływu danych międzyproceduralną a abstrakcyjną interpretacją) równoważność jest dla mnie stosunkowo oczywista, ale pytanie to wydaje się bardziej subtelne w przypadku innych porównań. Na przykład nie mogę zrozumieć, w jaki sposób można wnioskować o typie Hindleya-Milnera, aby udowodnić niektóre właściwości, które można udowodnić za pomocą analizy przepływu danych wrażliwej na przepływ.

Jakie są najważniejsze odniesienia omawiające równoważności (lub różnice) między analizą przepływu danych, abstrakcyjną interpretacją i wnioskowaniem typu?

Analiza przepływu danych i wnioskowanie o typach są szczególnymi przypadkami abstrakcyjnej interpretacji.

Analiza przepływu danych i interpretacja abstrakcyjna wyglądają podobnie, ponieważ oba dotyczą obliczenia punktu stałego. Analizy przepływu danych zwykle mają abstrakcyjne domeny o skończonej wysokości, co zapewnia zakończenie. Ogólnie abstrakcyjna interpretacja nie zakłada takich abstrakcyjnych domen; w radzeniu sobie z domenami o nieskończonej wysokości interpretacja abstrakcyjna wykorzystuje techniki poszerzania i zawężania.

Okazuje się, że wnioskowanie typu dotyczy także obliczania punktów stałych, chociaż nie jest to oczywiste, imo. Oto artykuł, który wyraźnie pokazuje, że typy są abstrakcyjnymi interpretacjami: papier . Zasadniczo typy są postrzegane jako abstrakcja konkretnej semantyki programu. Na przykład w systemie typów Hindleya-Milnera abstrakcyjna dziedzina typów ma nieskończoną wysokość, a obliczenie (najbardziej ogólnego) typu przy użyciu unifikacji zasadniczo wykonuje (bardzo nieprecyzyjną) operację poszerzenia.

Dobrym miejscem do zapoznania się z tymi trzema podejściami i ich relacją jest książka Zasady analizy programu autorstwa Nielsona, Nielsona i Hankina.

Nie uważam za słuszne stwierdzenie, że analiza przepływu danych, abstrakcyjna interpretacja i wnioskowanie typu są tym samym. Chociaż istnieje wiele podobieństw, a może nawet więcej, niż można by się spodziewać, biorąc pod uwagę, że te trzy wywodzą się z różnych społeczności, istnieje również wiele różnic.

Uważam je za zasadniczo takie same. Mieli początkowo różne cele i zostali wymyśleni przez różne frakcje informatyczne.

Analiza przepływu danych pochodzi od frakcji inżynierów kompilatorów, próbujących mówić o ich algorytmach optymalizacyjnych i sprawdzających górne granice ich złożoności itp.

Interpretacja abstrakcyjna pochodzi z formalnej, matematycznej dziedziny informatyki. Jest to jeszcze bardziej formalna wersja z większym zainteresowaniem poprawnością i mniejszym budowaniem prawdziwych kompilatorów.

Wnioskowanie typu pochodzi z akademickiego obszaru programowania funkcjonalnego, gdzie początkowo było narzędziem do robienia fajnych rzeczy za pomocą kompilatorów. Potem pojawił się pomysł, że typ może być czymś więcej niż tylko „int” lub „float”, ale także innymi rzeczami, jak w klasycznej analizie przepływu danych.