Äquivalenz von Datenflussanalyse, abstrakter Interpretation und Typinferenz?

Die Antwort von @ Babou auf eine kürzlich gestellte Frage erinnert mich daran, dass ich einmal einen Artikel über die Äquivalenz (sowohl hinsichtlich der Fakten, die abgeleitet oder bewiesen werden können, als auch hinsichtlich der zeitlichen Komplexität der Ausführung des Inferenzalgorithmus) der Datenflussanalyse gelesen habe , abstrakte Interpretation und Typinferenz .

In einigen Teilfällen (z. B. zwischen vorwärtskontextsensitiver interprozeduraler Datenflussanalyse und abstrakter Interpretation) ist die Äquivalenz für mich relativ offensichtlich, aber die Frage scheint für andere Vergleiche subtiler zu sein. Zum Beispiel kann ich nicht herausfinden, wie die Inferenz vom Hindley-Milner-Typ verwendet werden kann, um einige der Eigenschaften zu beweisen, die mit einer flusssensitiven Datenflussanalyse bewiesen werden können.

Was sind die wegweisenden Referenzen, die die Äquivalenzen (oder Unterschiede) zwischen Datenflussanalyse, abstrakter Interpretation und Typinferenz diskutieren?

Datenflussanalyse und Typinferenz sind spezifische Beispiele für abstrakte Interpretation.

Datenflussanalyse und abstrakte Interpretation sehen ähnlich aus, da es bei beiden um die Berechnung eines Fixpunkts geht. Datenflussanalysen haben normalerweise abstrakte Domänen mit endlicher Höhe, die die Beendigung sicherstellen. Im Allgemeinen nimmt die abstrakte Interpretation solche abstrakten Bereiche nicht an; Um mit unendlichen Höhenbereichen umzugehen, werden bei der abstrakten Interpretation Techniken zum Erweitern und Verengen verwendet.

Es stellt sich heraus, dass es bei der Typinferenz auch um die Fixpunktberechnung geht, obwohl dies imo alles andere als offensichtlich ist. Hier ist ein Papier, das explizit zeigt, dass Typen abstrakte Interpretationen sind: Papier . Grundsätzlich werden Typen als Abstraktion der programmkonkreten Semantik angesehen. Im Hindley-Milner-Typsystem ist beispielsweise die abstrakte Domäne von Typen von unendlicher Höhe, und die Berechnung eines (allgemeinsten) Typs unter Verwendung der Vereinheitlichung führt im Wesentlichen eine (sehr ungenaue) Erweiterungsoperation durch.

Ein guter Ort, um mehr über diese drei Ansätze und deren Beziehung zu erfahren, ist das Buch Principles of Program Analysis von Nielson, Nielson und Hankin.

Ich denke nicht, dass es richtig ist zu sagen, dass Datenflussanalyse, abstrakte Interpretation und Typinferenz dasselbe sind. Obwohl es viele Ähnlichkeiten gibt und vielleicht mehr als erwartet, da die drei aus verschiedenen Gemeinschaften stammen, gibt es auch viele Unterschiede.

Ich betrachte sie als grundsätzlich gleich. Sie hatten anfangs nur unterschiedliche Ziele und wurden von verschiedenen Informatikfraktionen geprägt.

Die Datenflussanalyse stammt von der Compiler-Engineering-Fraktion, die versucht, über ihre Optimierungsalgorithmen zu sprechen und Obergrenzen für ihre Komplexität usw. zu prüfen.

Die abstrakte Interpretation stammt aus dem formalen, mathematischen Bereich der Informatik. Dies ist eine noch formellere Version mit mehr Interesse an Korrektheit und weniger an der Erstellung realer Compiler.

Typinferenz kommt aus dem akademischen Bereich der funktionalen Programmierung, wo es ursprünglich ein Werkzeug war, um coole Sachen mit Compilern zu machen. Dann kam die Idee auf, dass ein Typ viel mehr als nur "int" oder "float" sein kann, sondern auch andere Dinge wie in der klassischen Datenflussanalyse.