¿Equivalencia de análisis de flujo de datos, interpretación abstracta e inferencia de tipos?

La respuesta de @ Babou a una pregunta reciente me recuerda que en un momento creo que leí un artículo sobre la equivalencia (en términos de los hechos que se pueden inferir o probar y la complejidad del tiempo de ejecutar el algoritmo de inferencia) del análisis de flujo de datos , interpretación abstracta e inferencia de tipos .

En algunos casos secundarios (como entre el análisis de flujo de datos interprocedural sensible al contexto directo y la interpretación abstracta), la equivalencia es relativamente obvia para mí, pero la pregunta parece más sutil para otras comparaciones. Por ejemplo, no puedo entender cómo se podría usar la inferencia de tipo Hindley-Milner para probar algunas de las propiedades que se pueden probar con el análisis de flujo de datos sensible al flujo.

¿Cuáles son las referencias fundamentales que discuten las equivalencias (o diferencias) entre el análisis del flujo de datos, la interpretación abstracta y la inferencia de tipos?

El análisis del flujo de datos y la inferencia de tipos son instancias específicas de interpretación abstracta.

El análisis del flujo de datos y la interpretación abstracta parecen similares, ya que ambos tratan de calcular un punto fijo. Los análisis de flujo de datos suelen tener dominios abstractos de altura finita que garantizan la terminación. En general, la interpretación abstracta no asume tales dominios abstractos; Para tratar dominios de altura infinita, la interpretación abstracta utiliza técnicas de ensanchamiento y estrechamiento.

Resulta que la inferencia de tipos también se trata del cálculo de punto fijo, aunque eso está lejos de ser obvio, en mi opinión. Aquí hay un documento que muestra explícitamente que los tipos son interpretaciones abstractas: papel . Básicamente, los tipos se ven como una abstracción de la semántica concreta del programa. En el sistema de tipos Hindley-Milner, por ejemplo, el dominio abstracto de los tipos es de altura infinita y el cálculo de un tipo (más general) que utiliza la unificación está realizando esencialmente una operación de ampliación (muy imprecisa).

Un buen lugar para aprender sobre estos tres enfoques y cómo se relacionan es el libro Principios del análisis de programas de Nielson, Nielson y Hankin.

No creo que sea correcto decir que el análisis del flujo de datos, la interpretación abstracta y la inferencia de tipos son lo mismo. Si bien hay muchas similitudes, y tal vez más de lo que cabría esperar, dado que las tres se originaron en diferentes comunidades, también hay muchas diferencias.

Los considero básicamente lo mismo. Inicialmente tenían objetivos diferentes y fueron acuñados por diferentes facciones informáticas.

El análisis del flujo de datos proviene de la facción de ingeniería del compilador, tratando de hablar sobre sus algoritmos de optimización y probando los límites superiores de su complejidad, etc.

La interpretación abstracta proviene del campo formal y matemático de la informática. Esta es una versión aún más formal con más interés en la corrección y menos en la construcción de compiladores reales.

La inferencia de tipos proviene del campo académico de la programación funcional, donde inicialmente era una herramienta para hacer cosas geniales con los compiladores. Entonces surgió la idea de que un tipo puede ser mucho más que simplemente "int" o "flotante", sino también otras cosas como en el análisis de flujo de datos clásico.