@Babou's answer to a recent question reminds me that at one time I think I read a paper about the equivalence (in terms both of the facts that can be inferred or proved and the time complexity of running the inference algorithm) of data-flow analysis, abstract interpretation, and type inference.
In some sub-cases (like between forward context-sensitive interprocedural data-flow analysis and abstract interpretation) the equivalence is relatively obvious to me, but the question seems more subtle for other comparisons. For example, I can't figure out how Hindley-Milner type inference could be used to prove some of the properties that can be proved with flow-sensitive data-flow analysis.
What are the seminal references discussing the equivalences (or differences) between data-flow analysis, abstract interpretation and type inference?
Asked By : Wandering Logic
Answered By : bellpeace
Data flow analysis and type inference are specific instances of abstract interpretation.
Data flow analysis and abstract interpretation look similar since they are both about computing a fix point. Data flow analyses typically have finite-height abstract domains which ensures termination. In general, abstract interpretation does not assume such abstract domains; to deal with infinite height domains abstract interpretation uses techniques of widening and narrowing.
It turns out that type inference is also about fix-point computation, although that is far from obvious, imo. Here is a paper that explicitly shows that types are abstract interpretations: paper. Basically, types are seen as an abstraction of program concrete semantics. In Hindley-Milner type system, for instance, abstract domain of types is of infinite height and computing a (most general) type using unification is essentially performing a (very imprecise) widening operation.
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/30746
0 comments:
Post a Comment
Let us know your responses and feedback