Équivalence de l'analyse du flux de données, de l'interprétation abstraite et de l'inférence de type?

@ La réponse de Babou à une question récente me rappelle qu'à un moment donné, je pense avoir lu un article sur l'équivalence (en termes à la fois des faits qui peuvent être inférés ou prouvés et de la complexité temporelle de l'exécution de l'algorithme d'inférence) de l'analyse du flux de données , interprétation abstraite et inférence de type .

Dans certains sous-cas (comme entre l'analyse de flux de données interprocédurales contextuelle et l'interprétation abstraite), l'équivalence est relativement évidente pour moi, mais la question semble plus subtile pour d'autres comparaisons. Par exemple, je ne peux pas comprendre comment l'inférence de type Hindley-Milner pourrait être utilisée pour prouver certaines des propriétés qui peuvent être prouvées avec une analyse de flux de données sensible au flux.

Quelles sont les références séminales discutant les équivalences (ou différences) entre l'analyse de flux de données, l'interprétation abstraite et l'inférence de type?

L'analyse du flux de données et l'inférence de type sont des exemples spécifiques d'interprétation abstraite.

L'analyse du flux de données et l'interprétation abstraite se ressemblent car elles concernent toutes deux le calcul d'un point fixe. Les analyses de flux de données ont généralement des domaines abstraits de hauteur finie qui garantissent la terminaison. En général, l'interprétation abstraite ne suppose pas de tels domaines abstraits; pour traiter des domaines de hauteur infinie, l'interprétation abstraite utilise des techniques d'élargissement et de rétrécissement.

Il s'avère que l'inférence de type concerne également le calcul de points fixes, bien que cela soit loin d'être évident, imo. Voici un article qui montre explicitement que les types sont des interprétations abstraites: papier . Fondamentalement, les types sont considérés comme une abstraction de la sémantique concrète du programme. Dans le système de type Hindley-Milner, par exemple, le domaine abstrait des types est de hauteur infinie et le calcul d'un type (le plus général) en utilisant l'unification effectue essentiellement une opération d'élargissement (très imprécise).

Un bon endroit pour en savoir plus sur ces trois approches et comment les relier est le livre Principles of Program Analysis de Nielson, Nielson et Hankin.

Je ne pense pas qu'il soit correct de dire que l'analyse du flux de données, l'interprétation abstraite et l'inférence de type sont la même chose. Bien qu'il existe de nombreuses similitudes, et peut-être plus que ce à quoi on pourrait s'attendre, étant donné que les trois sont originaires de communautés différentes, il existe également de nombreuses différences.

Je les considère comme fondamentalement les mêmes. Ils avaient juste initialement des objectifs différents et ont été inventés par différentes factions informatiques.

L'analyse du flux de données provient de la faction d'ingénierie du compilateur, essayant de parler de leurs algorithmes d'optimisation et de vérifier les limites supérieures de leur complexité, etc.

L'interprétation abstraite provient du domaine mathématique formel de l'informatique. Il s'agit d'une version encore plus formelle avec plus d'intérêt pour la correction et moins pour la construction de vrais compilateurs.

L'inférence de type vient du domaine académique de la programmation fonctionnelle où c'était initialement un outil pour faire des trucs sympas avec des compilateurs. Puis l'idée est venue, qu'un type peut être beaucoup plus que simplement "int" ou "float" mais aussi d'autres choses comme dans l'analyse de flux de données classique.