Galois Connections for Recursive Types

Abstract

Building a static analyser for a real language involves modeling of large domains capturing the many available data types. To scale domain design and support efficient development of project-specific analyzers, it is desirable to be able to build, extend, and change abstractions in a systematic and modular fashion. We present a framework for modular design of abstract domains for recursive types and higher-order functions, based on the theory of solving recursive domain equations. We show how to relate computable abstract domains to our framework, and illustrate the potential of the construction by modularizing a monolithic domain for regular tree grammars. A prototype implementation in the dependently typed functional language Agda shows how the theoretical solution can be used in practice to construct static analysers.

Authors ordered alphabetically.

A Proofs

Theorem 1

If $\rho _1 \subseteq \rho _2$ then $[\![e ]\!]\rho _1 \subseteq [\![e ]\!]\rho _2$

Proof

Most cases follow straightforwardly by induction over the syntax of terms e and functoriality of the powerset lifting $\mathscr {P}$. We will consider the interesting cases below:

• Case $e = x$: follows by monotonicity of premise.

• Case : follows by monotonicity of extension and induction hypothesis.

• Case : follows by monotonicity of extension and induction hypothesis.

• Case $e = \textsf {fix } \; x. e_0$: follows by monotonicity of extension, induction hypothesis and the fact that the intersection of a set of monotone functions is itself a set of monotone functions.

Proposition 1

Let E be a set and ${E^{\sharp }}$ a complete lattice. There is a bijective correspondence between maps and Galois connections . The correspondence maps a Galois connection to $\upalpha ^{{1}{}}_{}$ defined as $\upalpha ^{{1}{}}_{} (x) = \upalpha _{}(\{x\})$ and a map $\upalpha ^{{1}{}}_{}$ to the Galois connection:

The correspondence can be summarized in the following diagram.

Proof

$$\begin{aligned} \upalpha (X) \sqsubseteq e^{\sharp }&\iff \left( \bigsqcup _{x \in X} \upalpha ^{{1}{}}_{}(x) \right) \sqsubseteq e^{\sharp } \\&\iff \forall x \in X. \upalpha ^{{1}{}}_{}(x) \sqsubseteq e^{\sharp } \\&\iff X \subseteq \upgamma (e^{\sharp }) \end{aligned}$$

Theorem 3

Suppose the abstract interpretation of recursive types

satisfies the equations

$$\begin{aligned} \textsf {fold }^{\sharp }\circ \textsf {unfold }^{\sharp }= \textsf {id }\qquad \textsf {unfold }^{\sharp }\circ \textsf {fold }^{\sharp }\sqsupseteq \textsf {id }\end{aligned}$$

If then $[\![t ]\!] \subseteq \upgamma ([\![t ]\!]^{\sharp })$, or equivalently $\upalpha ([\![t ]\!]) \sqsubseteq [\![t ]\!]^{\sharp }$

Theorem 3 is proved by induction on typing judgements, and must therefore be extended to open terms. This is done in the following lemma, which uses an extension of the maps $\upgamma$ and $\upalpha$ to contexts defined in the obvious (pointwise) way.

Lemma 1

Suppose , and that $\rho \in [\![\varGamma ]\!]$ and $\rho ^{\sharp } \in [\![\varGamma ]\!]^{\sharp }$, are such that $\rho \subseteq \upgamma (\rho ^{\sharp })$. If the conditions on the abstract interpretation of recursive types of Theorem 3 are satisfied, then $[\![t ]\!]\rho \subseteq \upgamma ([\![t ]\!]^{\sharp }\rho ^{\sharp })$ or, equivalently, $\upalpha ([\![t ]\!]\rho ) \subseteq [\![t ]\!]^{\sharp }\rho ^{\sharp }$

Theorem 3 obviously follows from this as a special case. Before proving Lemma 1 we need a few lemmas.

Lemma 2

If B is an open type and A a closed one, then and

Proof

Easy induction on B, which we omit.

Lemma 3

For any open type B and closed type A the following equality holds

In diagram style, this is

Proof

Induction on B. The cases of integers and unit type are trivial. In the case of a type variable X, we get

In the case of a product type we get

using the induction hypothesis in the third equality. The case for sum types is somewhat similar, except here we must branch over the input being an injection on the left or right. In the first case we get

again using the induction hypothesis in the third equality. The case of the input being an injection on the right is similar.

The final case is that of functions: . If $f : {[\![A_1 ]\!] \rightarrow [\![B_1 ]\!]([\![A ]\!]^\sharp )}$ then

By the induction hypothesis

which implies

since either side of this equation is the unique extension of the corresponding sides of the equation above to continuous maps. Thus, we get

proving the case and concluding the proof.

Lemma 4

If B is an open type, then the following diagram commutes

Proof

It suffices to show that since the two compositions in the diagram are the unique extensions of the two sides of this equation to continuous maps. By definition of $\upalpha ^{{1}{}}_{\mu X.B}$ we get

$$\begin{aligned} \upalpha ^{{1}{}}_{\mu X.B} \circ \textsf {fold }&= \textsf {fold }^{\sharp }\circ \upalpha ^{{1}{}}_{B}([\![\mu X.B ]\!]^\sharp ) \circ [\![B ]\!](\upalpha ^{{1}{}}_{\mu X.B}) \end{aligned}$$

By Lemma 3 the right hand side of this is equal to which concludes the proof.

We can now prove Lemma 1.

Proof (Lemma 1). By induction on typing derivation:

• Case $t = x$ trivial

• Case $t = \textsf {fix } \; \lambda x. s.$: By IH we get:

  $$\begin{aligned}{}[\![s ]\!]\rho [x \mapsto \upgamma ([\![t ]\!]^{\sharp }\rho ^{\sharp })]&\subseteq \upgamma ([\![s ]\!]^{\sharp }\rho ^{\sharp }[x \mapsto [\![t ]\!]^{\sharp }\rho ^{\sharp }]) \\&= \upgamma ([\![t ]\!]^{\sharp }\rho ^{\sharp }) \end{aligned}$$

  So $\upgamma ([\![t ]\!]^{\sharp }\rho ^{\sharp })$ is a post-fixpoint of $\lambda a. [\![s ]\!]\rho [x \mapsto a]$ and so greater than the greatest lower bound of these ($[\![t ]\!]\rho = \bigcap \{ a \mid [\![s ]\!]\rho [x \mapsto a] \subseteq a \}$).

• Case $t = s \; u$: Recall that is defined as:

  $$ \upalpha (F) = \bigsqcup _{f \in F} \upalpha _{B} \circ \mathscr {P}(f) \circ \upgamma _{A} $$

  Then

  

• Case We must show that for all $f \in [\![\lambda x. u ]\!]\rho$ it holds that

  $$\upalpha \circ \mathscr {P}(f) \circ \upgamma \sqsubseteq [\![\lambda x. u ]\!]^{\sharp }\rho ^{\sharp }$$

  or equivalently

  $$\begin{aligned} \mathscr {P}(f) \circ \upgamma \sqsubseteq \upgamma \circ [\![\lambda x. u ]\!]^{\sharp }\rho ^{\sharp } \end{aligned}$$

  (1)

  We know by IH that for all $a^{\sharp }$ it holds

  $$\begin{aligned}{}[\![u ]\!]\rho [x \mapsto \upgamma (a^{\sharp })]&\subseteq \upgamma ([\![u ]\!]^{\sharp }\rho ^{\sharp }[x \mapsto \upalpha (\upgamma (a^{\sharp }))]) \end{aligned}$$

  (2)
  $$\begin{aligned}&\subseteq \upgamma ([\![u ]\!]^{\sharp }\rho ^{\sharp }[x \mapsto a^{\sharp }]) \end{aligned}$$

  (3)

  To show Eq. (1) we must show that for all $a \in \upgamma (a^{\sharp })$ it holds:

  $$\begin{aligned} f(a)&\in \upgamma (([\![\lambda x. u ]\!]^{\sharp }\rho ^{\sharp })a^{\sharp }) \\&= \upgamma ([\![u ]\!]^{\sharp }\rho ^{\sharp }[x \mapsto a^{\sharp }]) \end{aligned}$$

  The assumption $f \in [\![\lambda x. u ]\!]\rho$ means precisely that $f(a) \in [\![u ]\!]\rho [x \mapsto \{a\}] \subseteq [\![u ]\!]\rho [x \mapsto \upgamma (a^{\sharp })]$ (by monotonicity), so by Eq. (3) we conclude.

• Case $t = \textsf {fold } \; u : \mu X. A$, The case is proved as follows

  $$\begin{aligned} \upalpha ([\![\textsf {fold } \; u ]\!]\rho )&= \upalpha (\mathscr {P}(\textsf {fold })([\![u ]\!]\rho )) \\&= \textsf {fold }^{\sharp }(\upalpha ([\![u ]\!]\rho )) \\&\sqsubseteq \textsf {fold }^{\sharp }([\![u ]\!]^{\sharp }\rho ^{\sharp }) \\&= [\![\textsf {fold } \; u ]\!]^{\sharp }\rho ^{\sharp } \end{aligned}$$

  using Lemma 4 for the second equality.

• Case First note that

  $$ \upalpha \circ \mathscr {P}(\textsf {unfold }) \sqsubseteq \textsf {unfold }^{\sharp } \circ \upalpha $$

  since

  $$\begin{aligned} \upalpha \circ \mathscr {P}(\textsf {unfold })&\sqsubseteq \textsf {unfold }^{\sharp }\circ \textsf {fold }^{\sharp }\circ \upalpha \circ \mathscr {P}(\textsf {unfold }) \\&= \textsf {unfold }^{\sharp }\circ \upalpha \circ \mathscr {P}(\textsf {fold }\circ \textsf {unfold }) \\&= \textsf {unfold }^{\sharp }\circ \upalpha \end{aligned}$$

  and so

  $$\begin{aligned} \upalpha ([\![\textsf {unfold } \; u ]\!]\rho )&= \upalpha (\mathscr {P}(\textsf {unfold })([\![u ]\!]\rho )) \\&\sqsubseteq \textsf {unfold }^{\sharp }(\upalpha ([\![u ]\!]\rho )) \\&\sqsubseteq \textsf {unfold }^{\sharp }([\![u ]\!]^{\sharp }\rho ^{\sharp }) \text { by IH} \\&= [\![\textsf {unfold } \; u ]\!]^{\sharp }\rho ^{\sharp } \end{aligned}$$