A Constructive Framework for Galois Connections

TL;DR

This paper introduces a new class of constructive Galois connections called partitioning GCs, enabling more flexible and mechanized static analysis through proof assistants, and establishes their theoretical equivalence to existing GCs.

Contribution

It proves the isomorphism between constructive Galois connections and partitioning GCs, and advocates for using partitioning GCs as a flexible, constructive framework for abstract interpretation.

Findings

Constructive Galois connections are isomorphic to partitioning GCs.

Partitioning GCs enable flexible set partition representations.

The approach facilitates mechanized, verified static analysis algorithms.

Abstract

Abstract interpretation-based static analyses rely on abstract domains of program properties, such as intervals or congruences for integer variables. Galois connections (GCs) between posets provide the most widespread and useful formal tool for mathematically specifying abstract domains. Recently, Darais and Van Horn [2016] put forward a notion of constructive Galois connection for unordered sets (rather than posets), which allows to define abstract domains in a so-called mechanized and calculational proof style and therefore enables the use of proof assistants like Coq and Agda for automatically extracting verified algorithms of static analysis. We show here that constructive GCs are isomorphic, in a precise and comprehensive meaning including sound abstract functions, to so-called partitioning GCs--an already known class of GCs which allows to cast standard set partitions as an abstract domain. Darais and Van Horn [2016] also provide a notion of constructive GC for posets, which we prove to be isomorphic to plain GCs and therefore lose their constructive attribute. Drawing on these findings, we put forward and advocate the use of purely partitioning GCs, a novel class of constructive abstract domains for a mechanized approach to abstract interpretation. We show that this class of abstract domains allows us to represent a set partition with more flexibility while retaining a constructive approach to Galois connections.

Equations

$$x\in \mu (y)\iff \eta (x)=y$$

$$x\in \mu (y)\iff \eta (x){\le }_{B}y$$

$$\begin{array}[]{rll}\text{powerset (or collecting) lifting:}&\quad f^{\diamond}:\wp(A)\rightarrow\wp(B)&f^{\diamond}(X)\triangleq\{f(x)~{}|~{}x\in X\}\\ \text{singleton powerset lifting:}&\quad f^{\scriptscriptstyle\rhd}:A\rightarrow\wp(B)&f^{\scriptscriptstyle\rhd}(a)\triangleq\{f(b)\}\\ \text{domain powerset lifting:}&\quad g^{*}:\wp(A)\rightarrow\wp(B)&g^{*}(X)\triangleq\cup_{x\in X}g(x)\\ \text{singleton lowering:}&\quad{h^{\scriptscriptstyle\{\!\cdot\!\}}}:A\rightarrow B&{h^{\scriptscriptstyle\{\!\cdot\!\}}}(a)\triangleq h(\{a\})\\ \text{lub domain powerset lifting:}&\quad k^{\vee}:\wp(A)\rightarrow C&k^{\vee}(X)\triangleq\vee_{a\in X}k(a)\end{array}$$

$$x\in \mu (y)\iff \eta (x)=y$$

$$x\in \mu (y)\iff \eta (x){\le }_{B}y$$

$$x\in \mu (y)\&y^{\prime }=\eta (f(x))\Rightarrow y^{\prime }=f_{♯}(y)$$

$$x\in \mu (y)\&x^{\prime }=f(x)\Rightarrow x^{\prime }\in \mu (f_{♯}(y))$$

$$y=\eta (f(x))\Rightarrow y=f_{♯}(\eta (x))$$

$$x^{\prime }=f(x)\Rightarrow x^{\prime }\in \mu (f_{♯}(\eta (x)))$$

$${\mathrm{sq}}_{\mathcal{S}}=\{\varnothing \mapsto \varnothing ,<0\mapsto >0,=0\mapsto =0,>0\mapsto >0,\le 0\mapsto \ge 0,\ne 0\mapsto >0,\ge 0\mapsto \ge 0,\mathbb{Z}\mapsto \ge 0\}.$$

$$x\in \mu (y)\&y^{\prime }=\eta (f(x))\iff y^{\prime }=f_{♯}(y)$$

$$x\in \mu (y)\&x^{\prime }=f(x)\iff x^{\prime }\in \mu (f_{♯}(y))$$

$$y=\eta (f(x))\iff y=f_{♯}(\eta (x))$$

$$x^{\prime }=f(x)\iff x^{\prime }\in \mu (f_{♯}(\eta (x)))$$

$$(1)$$

$$(2)$$

$$\eta (x)\triangleq \{\begin{array}{ll}(-\infty ,-10]& \text{if }x\in (-\infty ,-10]\\ [-9,-1]& \text{if }x\in [-9,-1]\\ [0,0]& \text{if }x=0\\ [1,9]& \text{if }x\in [1,9]\\ [10,+\infty )& \text{if }x\in [10,+\infty )\end{array}$$

$$f_{\mathcal{C}}(b)=\vee \{\eta (f(a))|a\in \mu (b)\}.$$

$$\eta (a)\le b\Rightarrow \eta (f(a))\le f_{♯}(b)$$

$$x:=2;y:=2;\text{while}x<9\text{do}x:=x\ast y;$$

$${\otimes }_{♯}(b_1,b_2)\triangleq {\eta }^{\vee }({\otimes }^{\diamond }(\mu (b_1),\mu (b_2))$$

$$\begin{gathered} {\vee }_B({\otimes }^{\diamond }(\{2,4\},\{-1,0\}))={\vee }_B\{0,-2,-4\}=\le 0= \\ {\otimes }_{♯}(>0,\le 0)={\otimes }_{♯}({\vee }_B\{2,4\},{\vee }_B\{-1,0\}). \end{gathered}$$

$${\gamma }^{\ast }(({\alpha }^{\{\cdot \}}{)}^{\diamond }(\wp (A)))$$

$$\displaystyle\gamma^{*}\Big{(}\big{\{}\{\alpha(\{a\})~{}|~{}a\in X\}~{}|~{}X\in\wp(A)\big{\}}\Big{)}$$

$$\{{\cup }_{a\in X}\gamma (\alpha (\{a\}))|X\in \wp (A)\}$$

$$\{\gamma (\alpha (X))|X\in \wp (A)\}$$

$$\gamma (\alpha (\wp (A)))$$

$$\displaystyle\big{\{}\gamma\big{(}(\lambda a.\alpha(\downarrow\!\!a))^{\vee}(Y)\big{)}~{}|~{}Y\in{\wp^{\downarrow}}(A)\big{\}}$$

$$\{\gamma ({\vee }_{y\in Y}\alpha (\downarrow y))|Y\in {\wp }^{\downarrow }(A)\}$$

$$\{\gamma (\alpha ({\cup }_{y\in Y}\downarrow y))|Y\in {\wp }^{\downarrow }(A)\}$$

$$\{\gamma (\alpha (Y))|Y\in {\wp }^{\downarrow }(A)\}$$

$$a\in \gamma ({\alpha }^{\{\cdot \}}(a^{\prime }))$$

$$a\in \gamma (\alpha (\{a^{\prime }\}))$$

$$\alpha (\{a\})\le \alpha (\{a^{\prime }\})$$

$$\gamma (\alpha (\{a\}))\subseteq \gamma (\alpha (\{a^{\prime }\}))$$

$$\gamma (\alpha (\{a\}))=\gamma (\alpha (\{a^{\prime }\}))$$

$$\alpha (\{a\})=\alpha (\{a^{\prime }\})$$

$${\alpha }^{\{\cdot \}}(a)={\alpha }^{\{\cdot \}}(a^{\prime })$$

$$\gamma (({\alpha }^{\{\cdot \}}{)}^{\vee }(\wp (A)))$$

$$\{\gamma (({\alpha }^{\{\cdot \}}{)}^{\vee }(X))|X\in \wp (A)\}$$

$$\{\gamma ({\vee }_{a\in X}{\alpha }^{\{\cdot \}}(a))|X\in \wp (A)\}$$

Full text

1 Introduction

Abstract interpretation [3, 4] is probably the most used and successful technique for defining approximations of program semantics (or, more in general, of computing systems) to be used for designing provably sound static program analyzers. Abstract domains play a crucial role in any abstract interpretation, since they encode, both logically for reasoning purposes and practically for implementations, which program properties are computed by a static analysis. Since its beginning [3], one major insight of abstract interpretation is given by the use of Galois connections (GCs) for defining abstract domains. A specification of an abstract domain $D$ through a Galois connection prescribes that: (1) both concrete and abstract domains, $C$ and $D$, are partially ordered, and typically they give rise to complete lattices; (2) definitions of abstraction $\alpha:C\rightarrow D$ and concretization $\gamma:D\rightarrow C$ maps to relate concrete and abstract values; (3) $\alpha$ and $\gamma$ give rise to an adjunction relation: $\alpha(c)\leq_{D}d\Leftrightarrow c\leq_{C}\gamma(d)$. GCs carry both advantages and drawbacks. One major benefit is the so-called calculational style for defining abstract operations [2, 14]: if $f:C\rightarrow C$ is any concrete operation involved by some semantic definition (e.g., integer addition or multiplication) then a corresponding correct approximation on $A$ is defined by $\alpha\circ f\circ\gamma:A\rightarrow A$, which turns out to be the best possible approximation of $f$ on the abstract domain $A$ and, as envisioned by Cousot [2], allows to systematically derive abstract operations in a correct-by-design manner. On the negative side, GCs have two main weaknesses. First, GCs formalize an ideal situation where each concrete property in $C$ has a unique best abstract approximation in $D$. Some very useful and largely used abstract domains cannot be defined by a GC, being convex polyhedra a prominent example of abstract domain where no abstraction map can be defined [7]. This problem motivated weaker abstract interpretation frameworks which only need concretization maps [5]. Secondly, it turns out that abstraction maps of GCs cannot be mechanized [15, 17], meaning that one cannot use automatic formal proof systems like Coq in order to extract certified algorithms of abstract interpretation, e.g., based on best correct approximations $\alpha\circ f\circ\gamma$. In other terms, the calculational approach of abstract interpretation cannot be automatized. Notably, Verasco [12, 13] (and its precursor described in [1]) is a static analyzer for C which has been formally designed and verified using the Coq proof assistant, and is based on abstract interpretation using only concretization maps. This latter motivation was one starting point of Darais and Van Horn [8] for investigating constructive versions Galois connections, together with the observation that many useful abstract domains, even if defined by an abstraction map, still would permit a mechanization of their soundness proofs. Also, Darais and Van Horn’s approach [8] generalizes ‘Galculator’ [20], which is a proof assistant based on a given small algebra of Galois connections.

Constructive Galois connections (CGCs) [8] stem from the observation that for many commonly used abstract domains: (1) the concrete domain is a powerset (or collecting) domain $\wp(A)$ of an unordered carrier domain $A$; (2) the abstraction map $\alpha:\wp(A)\rightarrow D$ is actually defined as collecting lifting of a basic abstraction function $\eta$ which is defined just on the carrier domain $A$ and takes values belonging to an unordered abstract domain $B$, that is, $\eta:A\rightarrow B$; (3) the concretization map $\mu:B\rightarrow\wp(A)$ provides meaning to basic abstract values ranging in $B$; (4) the $\alpha$/$\gamma$ adjunction relation can be equivalently reformulated in terms of the following correspondence between $\eta$ and $\mu$:

[TABLE]

Moreover, CGCs allow to give a soundness condition for pairs of concrete and abstract functions which are defined on carrier concrete and abstract domains $A$ and $B$. As a simple example taken from [8, Section 2], the standard toy parity abstraction for integer variables can be defined as a CGC as follows. The carrier concrete domain is $\mathbb{Z}$, the unordered parity domain is $\mathbb{P}=\{{\textit{even}},{\textit{odd}}\}$, abstraction $\operatorname{parity}:\mathbb{Z}\rightarrow\mathbb{P}$ and concretization $\mu:\mathbb{P}\rightarrow\wp(\mathbb{Z})$ mappings are straightforwardly defined and satisfy (CGC-Corr): $z\in\mu(a)\Leftrightarrow\operatorname{parity}(z)=a$. Also, a successor concrete operation $\operatorname{succ}:\mathbb{Z}\rightarrow\mathbb{Z}$ is approximated by a sound abstract successor $\operatorname{succ}_{\sharp}:\mathbb{P}\rightarrow\mathbb{P}$ such that $\operatorname{succ}_{\sharp}({\textit{even}})={\textit{odd}}$ and $\operatorname{succ}_{\sharp}({\textit{odd}})={\textit{even}}$.

Darais and Van Horn [8] also put forward a more general notion of constructive Galois connection for posets (CGP), where the carrier concrete domain $A$ and the abstract domain $B$ are posets (rather than unordered sets), and where the condition (CGC-Corr) is weakened to:

[TABLE]

This allows them to provide a constructive definition for ordered abstract domains like the sign abstraction of integer variables $\operatorname{Sign}=\{\varnothing,\><\!0,\>=\!0,\>>\!0,\>\leq\!0,\>\neq\!0,\>\geq\!0,\>\mathbb{Z}\}$ which encodes approximation relations between its abstract values, e.g., the abstract value $\geq\!0$ approximates $>\!0$.

Contributions. Our initial observation was that CGCs always encode a partition of the concrete carrier set $A$. As a simple example, for the above parity domain $\mathbb{P}$, the induced partition of $\mathbb{Z}$ obviously consists of two blocks: $\{z\in\mathbb{Z}~{}|~{}z~{}\text{even}\}$ and $\{z\in\mathbb{Z}~{}|~{}z~{}\text{odd}\}$. Furthermore, we also noticed that if an abstract domain $D$ of a collecting domain $\wp(A)$ does not induce an underlying partition of $A$ and $D$ is defined through a standard Galois connection $\mathcal{G}$ then $\mathcal{G}$ cannot be constructively and equivalently formulated by a CGC. Indeed, abstract domains which encode a partition of a given carrier set have been previously studied and formalized as so-called partitioning Galois connections (PGCs). Intuitively, a Galois connection defining a domain $D$ which abstracts a concrete collecting domain $\wp(A)$ is called partitioning [6, 18] when $D$ represents a partition $\mathcal{P}$ of the set $A$ together with all the possible unions of blocks in $\mathcal{P}$. Our first contribution shows that CGCs are isomorphic to PGCs. This isomorphism is constructive, meaning that we define two invertible transforms which map a CGC to an equivalent PGC and vice versa. Moreover, this isomorphism includes soundness of abstract operations, meaning that we also define invertible transforms of pairs of concrete/abstract operations which preserve their soundness. Secondly, we also investigated Darais and Van Horn’s CGPs, in order to characterize them as a suitable class of Galois connections. We show that CGPs actually amount to plain GCs of a powerdomain, and therefore CGPs are not able to isolate a specific class of GCs. This is a negative finding: the generalization from CGCs to CGPs loses the constructive attribute of CGCs. Drawing on these results, our third and most significant contribution is the definition of a novel class of constructive Galois connections, called purely constructive GCs (PCGCs), which is more flexible than CGCs while retaining a constructive approach to Galois connections. The basic idea underlying PCGCs is as follows. CGCs essentially represent a partition of the carrier concrete domain $A$ through an abstract domain $B$. We showed that this partition representation in $B$ implicitly brings all the possible unions of its blocks. We generalize this approach by allowing to select which unions of blocks to consider in the abstract domain $B$. Hence, $B$ may be defined as a partition $\mathcal{P}$ of $A$ together with an explicit choice of unions of blocks of $\mathcal{P}$, where this selection may range from none to all. As an example, a sign abstraction like $\operatorname{Sign}^{-}\triangleq\operatorname{Sign}\smallsetminus\{\neq\!0\}$ cannot be formalized as a CGC, although $\operatorname{Sign}^{-}$ still represents a partition of $\mathbb{Z}$ since $\operatorname{Sign}^{-}$ just lacks the union of blocks corresponding to the abstract value $\neq\!0$, that is, the union of $<\!0$ and $>\!0$. In our framework, $\operatorname{Sign}^{-}$ can be exactly defined as a PCGC. Moreover, PCGCs come together with a definition of sound abstract operations, which also accomodates the standard notions of completeness commonly used in abstract interpretation. This paper therefore advocates the use of PPGCs as a suitable class of constructive abstract domains for a mechanized approach to abstract interpretation.

2 Background

Notation.

Let $f:A\rightarrow B$, $g:A\rightarrow\wp(B)$ and $h:\wp(A)\rightarrow B$, $k:A\rightarrow C$, where $A$ and $B$ are sets and $C$ is a complete lattice with lub $\vee$. We then use the following definitions:

[TABLE]

Somewhere we use $f(X)$ as an alternative notation for $f^{\diamond}(X)$. If $A$ is a poset and $X\subseteq A$ then ${\downarrow\!X}\triangleq\{y\in A~{}|\exists x\in X.y\leq x\}$, and, in turn, ${\wp^{\downarrow}}(A)\triangleq\{X\subseteq A~{}|~{}X=\>\downarrow\!X\}$ denotes the downward powerdomain of $A$, which ordered by subset inclusion, is a complete lattice. We use $\downarrow\!a$ as a shorthand for $\downarrow\!\{a\}$. Recall that any set $A$ can be viewed as poset w.r.t. the so-called discrete partial order $\leq$: for all $x,y\in A$, $x\leq y$ iff $x=y$. Let us also recall that $\mathcal{P}\subseteq\wp(A)$ is a partition of $A$ when: $B\in\mathcal{P}\Rightarrow B\neq\varnothing$; if $B_{1},B_{2}\in\mathcal{P}$ and $B_{1}\neq B_{2}$ then $B_{1}\cap B_{2}=\varnothing$; $\cup_{B\in\mathcal{P}}B=A$.

Galois connections.

Recall that $\mathcal{G}=\langle\alpha,C,D,\gamma\rangle$ is a Galois connection (GC) when $C$ and $D$ are posets, $\alpha:C\rightarrow D$, $\gamma:D\rightarrow C$ and $\alpha(c)\leq_{D}d\>\Leftrightarrow c\leq_{C}\gamma(d)$. By following a standard terminology in abstract interpretation, $C$ and $D$ are called concrete and abstract domains, while $\alpha$ and $\gamma$ are called abstraction and concretization maps. $\mathcal{G}$ is a disjunctive GC when $\gamma$ is additive (intuitively meaning that it abstractly represents logical disjunctions with no loss of precision). $\mathcal{G}$ is a Galois insertion (GI) when $\alpha$ is surjective (or, equivalently, $\gamma$ is injective).

Let us recall some standard definitions and terminology of abstract interpretation [3, 4]. Let $f:C\rightarrow C$ and $f_{\sharp}:D\rightarrow D$ be, respectively, concrete and abstract functions. The pair $\langle f,f_{\sharp}\rangle_{\mathcal{G}}$ is sound (w.r.t. $\mathcal{G}$) when $\alpha\circ f\circ\gamma\sqsubseteq f_{\sharp}$, or, equivalently, $\alpha\circ f\sqsubseteq f_{\sharp}\circ\alpha$. Also, the pair $\langle f,f_{\sharp}\rangle_{\mathcal{G}}$ is optimal when $\alpha\circ f\circ\gamma=f_{\sharp}$, backward complete when $\alpha\circ f=f_{\sharp}\circ\alpha$, forward complete when $f\circ\gamma=\gamma\circ f_{\sharp}$, precise when $f=\gamma\circ f_{\sharp}\circ\alpha$. The abstract function $f_{\mathcal{G}}\triangleq\alpha\circ f\circ\gamma$ is called the best correct approximation (BCA) of $f$ induced by $\mathcal{G}$.

Let $\mathcal{G}_{1}=\langle\alpha_{1},C,D_{1},\gamma_{1}\rangle$ and $\mathcal{G}_{2}=\langle\alpha_{2},C,D_{2},\gamma_{2}\rangle$ be two GCs with a common concrete domain $C$. $\mathcal{G}_{1}$ is more precise than $\mathcal{G}_{2}$, denoted by $\mathcal{G}_{1}\sqsubseteq\mathcal{G}_{2}$, when $\gamma_{2}(\alpha_{2}(C))\subseteq\gamma_{1}(\alpha_{1}(C))$. In turn, $\mathcal{G}_{1}$ and $\mathcal{G}_{2}$ are isomorphic when $\mathcal{G}_{1}\sqsubseteq\mathcal{G}_{2}$ and $\mathcal{G}_{2}\sqsubseteq\mathcal{G}_{1}$, i.e., when $\gamma_{1}(\alpha_{1}(C))=\gamma_{2}(\alpha_{2}(C))$ holds. The intuition is that $\mathcal{G}_{1}$ and $\mathcal{G}_{2}$ abstractly encode the same properties of $C$ up to a renaming of the abstract values in $D_{i}$. If $f^{\sharp}_{1}:D_{1}\rightarrow D_{1}$ and $f^{\sharp}_{2}:D_{2}\rightarrow D_{2}$ are two abstract functions for $f:C\rightarrow C$ then $f^{\sharp}_{1}$ is called isomorphic to $f^{\sharp}_{2}$ when $\gamma_{1}\circ f_{1}^{\sharp}\circ\alpha_{1}=\gamma_{2}\circ f_{2}^{\sharp}\circ\alpha_{2}$.

3 Constructive Galois Connections

Constructive Galois connections (CGCs) have been defined by Darais and Van Horn [8, Section 3] to provide a Galois connection-like correspondence between sets rather than posets: $\langle\eta,A,B,\mu\rangle_{\text{CGC}}$ is a CGC when $A$ and $B$ are sets, and $\eta:A\rightarrow B$, $\mu:B\rightarrow\wp(A)$ satisfy the following equivalence

[TABLE]

The intuition is that $A$ is a carrier set of the concrete powerset domain, $B$ is an unordered abstract domain, $\eta$ is a representation function for concrete singletons $\{a\}$ while $\mu$ is a concretization function, which give rise to a sort of unordered adjunction relation. CGCs have the following properties.

Lemma 3.1** (CGC properties).**

Consider a CGC $\langle\eta,A,B,\mu\rangle$.

• (1)

$\eta(a_{1})=\eta(a_{2})\>\Leftrightarrow\>\mu(\eta(a_{1}))=\mu(\eta(a_{2}))\>\Leftrightarrow\>\mu(\eta(a_{1}))\cap\mu(\eta(a_{2}))\neq\varnothing$**

• (2)

$\mu(b)=\varnothing\>\Leftrightarrow\>b\not\in\eta(A)$**

As a consequence, we have that $\{\mu(\eta(a))\}_{a\in A}$ are the blocks of a partition of $A$, because $A=\cup_{a\in A}\mu(\eta(a))$ and if $\mu(\eta(a_{1}))\neq\mu(\eta(a_{2}))$ then $\mu(\eta(a_{1}))\cap\mu(\eta(a_{2}))=\varnothing$.

Darais and Van Horn [8, Section 3.1] also define constructive Galois connections for posets (CGPs) as follows. $\langle\eta,A,B,\mu\rangle$ is a CGP when $\langle A,\leq_{A}\rangle$ and $\langle B,\leq_{B}\rangle$ are posets (so that ${\wp^{\downarrow}}(A)_{\subseteq}$ is a complete lattice), $\eta:A\rightarrow B$ and $\mu:B\rightarrow{\wp^{\downarrow}}(A)$ are monotone and the following equivalence holds:

[TABLE]

Hence, in CGP-Corr $\leq_{B}$ replaces $=$ of CGC-Corr. We focus on the following properties of CGPs.

Lemma 3.2** (CGP properties).**

Consider a CGP $\langle\eta,A,B,\mu\rangle$.

• (1)

$\eta(a_{1})=\eta(a_{2})\>\Leftrightarrow\>\mu(\eta(a_{1}))=\mu(\eta(a_{2}))$**

• (2)

$\mu(b)=\varnothing\>\Leftrightarrow\>\downarrow\!\!b\cap\eta(A)=\varnothing$**

• (3)

If $B$ is a complete lattice then $\langle\eta^{\vee},{\wp^{\downarrow}}(A),B,\mu\rangle$ is a GC

• (4)

$\mu(B)=\mu({\eta^{\vee}}({\wp^{\downarrow}}(A)))$**

Example 3.3**.**

Consider $\mathbb{Z}$ with the discrete partial order, so that ${\wp^{\downarrow}}(\mathbb{Z})=\wp(\mathbb{Z})$, $B\triangleq\{+,\top\}$ with ordering $+\leq\top$, $\eta:\mathbb{Z}\rightarrow B$ be defined by $\eta(x)\triangleq\textbf{if}\>x>0\>\textbf{then}\,+\,\textbf{else}\,\top$ and $\mu:\mathbb{Z}\rightarrow\wp(\mathbb{Z})$ be defined by $\mu(+)=\mathbb{Z}_{>0}$ and $\mu(\top)=\mathbb{Z}$. It turns out that $\langle\eta,\mathbb{Z},B,\mu\rangle$ is not a CGC, because $1\in\mu(\top)$ while $+=\eta(1)\neq\top$. Instead, $+=\eta(1)\leq\top$ holds, and indeed this is a CGP. Notice that $\{\mu(\eta(z))~{}|~{}z\in\mathbb{Z}\}=\{\mathbb{Z}_{>0},\mathbb{Z}\}$ is not a partition of $\mathbb{Z}$. Besides, if $B^{\prime}=\{-,0,+,\bot\}$, $\beta:\mathbb{Z}\rightarrow B^{\prime}$ encodes the sign of an integer, and $\delta:B^{\prime}\rightarrow\wp(\mathbb{Z})$ is defined by: $\delta(-)=\mathbb{Z}_{<0}$, $\delta(0)=\{0\}$, $\delta(+)=\mathbb{Z}_{>0}$, $\delta(\bot)=\varnothing$, then $\langle\beta,\mathbb{Z},B^{\prime},\delta\rangle$ is clearly a CGC. ∎

In the following we will need to compare CGCs with a common concrete carrier set. Thus, consider two CGCs $\mathcal{C}_{1}=\langle\eta_{1},A,B_{1},\mu_{1}\rangle$ and $\mathcal{C}_{2}=\langle\eta_{2},A,B_{2},\mu_{2}\rangle$. Then, $\mathcal{C}_{1}$ is defined to be more precise than $\mathcal{C}_{2}$ (or, $\mathcal{C}_{2}$ is more abstract than $\mathcal{C}_{1}$) when $\mu_{2}(B_{2})\subseteq\mu_{1}(B_{1})$, and this is denoted by $\mathcal{C}_{1}\sqsubseteq\mathcal{C}_{2}$. Also, $\mathcal{C}_{1}$ and $\mathcal{C}_{2}$ are isomorphic when $\mathcal{C}_{1}\sqsubseteq\mathcal{C}_{2}$ and $\mathcal{C}_{2}\sqsubseteq\mathcal{C}_{1}$, i.e., when $\mu_{1}(B_{1})=\mu_{2}(B_{2})$, and this is denoted by $\mathcal{C}_{1}\cong\mathcal{C}_{2}$. The intuition is that two CGCs are isomorphic when they represent the same abstraction $\mu_{i}(B_{i})$ of $\wp(A)$ up to a renaming of the abstract values. This notion of isomorphism is justified by the following result, where $f_{1,2}$ and $f_{2,1}$ play the role of renaming functions for abstract values.

Lemma 3.4** (CGC Isomorphism).**

Consider $\mathcal{C}_{1}=\langle\eta_{1},A,B_{1},\mu_{1}\rangle$ and $\mathcal{C}_{2}=\langle\eta_{2},A,B_{2},\mu_{2}\rangle$ CGCs. Then, $\mathcal{C}_{1}\cong\mathcal{C}_{2}$ iff there exist $f_{1,2}:\eta_{1}(A)\rightarrow\eta_{2}(A)$ and $f_{2,1}:\eta_{2}(A)\rightarrow\eta_{1}(A)$ such that $f_{1,2}\circ f_{2,1}=\mathrm{id}=f_{2,1}\circ f_{1,2}$, $\mu_{1}\circ\eta_{1}=\mu_{2}\circ f_{1,2}\circ\eta_{1}$ and $\mu_{2}\circ\eta_{2}=\mu_{1}\circ f_{2,1}\circ\eta_{2}$.

We also define a notion of nonempty isomorphism $\cong_{\varnothing}$ which does not take into account possible empty sets in $\mu(B_{i})$: $\langle\eta_{1},A,B_{1},\mu_{1}\rangle\cong_{\varnothing}\langle\eta_{2},A,B_{2},\mu_{2}\rangle$ when $\mu_{1}(B_{1})\cup\{\varnothing\}=\mu_{2}(B_{2})\cup\{\varnothing\}$. This is justified by the observation that for any CGC $\langle\eta,A,B,\mu\rangle$, we have that $\langle\eta,A,B,\mu\rangle\cong_{\varnothing}\langle\eta,A,\eta(A),\mu\rangle$, because, by Lemma 3.2 (2), all the abstract values in $B\smallsetminus\eta(A)$ represent the empty set. These can therefore be viewed as “useless” abstract values and lead to a notion of constructive Galois insertion (CGI) which is the analogue of GI: $\langle\eta,A,B,\mu\rangle$ is a CGI when it is a CGC and $\eta$ is surjective.

4 Partitioning Galois Connections

Partitioning Galois connections/insertions (PGCs/PGIs) have been introduced in [6, Section 5]: given a partition $\mathcal{P}$ of a set $A$, any subset $X\in\wp(A)$ is over-approximated by the unique minimal cover of $X$ through blocks in $\mathcal{P}$. PGCs have been studied and used in [18, 19] for generalizing strong preservation of temporal logics in model checking. Let $\mathcal{G}=\langle\alpha,\wp(A)_{\subseteq},D_{\leq},\gamma\rangle$ be a Galois connection, where $A$ is any carrier set and $D$ is a poset, and let $\operatorname{prt}(\mathcal{G})\triangleq\{\gamma(\alpha(\{a\}))\}_{a\in A}$. $\mathcal{G}$ is called a partitioning Galois connection when: (1) $\operatorname{prt}(\mathcal{G})$ is a partition of $A$; (2) $\gamma$ is additive, i.e., $\gamma$ preserves arbitrary lub’s. The main feature of a PGC is that any abstract value $d$ represents a union of blocks of the partition $\operatorname{prt}(\mathcal{G})$, namely $\gamma(d)=\cup_{a\in\gamma(d)}\gamma(\alpha(\{a\}))$, and, vice versa, for any set of blocks $\{\gamma(\alpha(\{a\}))~{}|~{}a\in S\}$ of the partition $\operatorname{prt}(\mathcal{G})$, for some $S\in\wp(A)$, there exists $d\in A$ such that $\gamma(d)=\cup\{\gamma(\alpha(\{a\}))~{}|~{}a\in S\}$, where $d=\alpha(S)$. In other terms, the abstract domain $D$ is a representation of all the possible unions of blocks in $\operatorname{prt}(\mathcal{G})$. Although this is the standard definition of PGC, instead of representing all the possible unions of blocks of a partition, one could equivalently represent no union of blocks at all: this means that the condition (2) of PGCs of having an additive concretization map $\gamma$ could be replaced by $(2^{\prime})$: if $x,y\in D$ and $x,y$ are uncomparable then $\gamma(x\vee_{D}y)=A$. Hence, if $\alpha(\{a_{1}\})$ and $\alpha(\{a_{2}\})$ represent in $D$ two different blocks then their lub represent no information at all (i.e., $\gamma(\alpha(\{a_{1},a_{2}\}))=A$).

It turns out that the notion of CGC is completely equivalent to that of PGC, in the following precise meaning based on a pair of invertible transforms of CGCs and PGCs.

Theorem 4.1** (CGC-PGC Equivalence).**

• (1)

If $\mathcal{C}=\langle\eta,A,B,\mu\rangle$ is a CGC then $\mathbb{T}_{\text{PGC}}(\mathcal{C})$ $\triangleq\langle\eta^{\diamond},\wp(A)_{\subseteq},\wp(B)_{\subseteq},\mu^{*}\rangle$ is a PGC.

• (2)

If $\mathcal{G}=\langle\alpha,\wp(A)_{\subseteq},D_{\leq},\gamma\rangle$ is a PGC then $\mathbb{T}_{\text{CGC}}(\mathcal{G})$ $\triangleq\langle{\alpha^{\scriptscriptstyle\{\!\cdot\!\}}},A,\{\alpha(\{a\})~{}|~{}a\in A\},\gamma\rangle$ is a CGC.

• (3)

The transforms $\mathbb{T}_{\text{PGC}}$ and $\mathbb{T}_{\text{CGC}}$ are one the inverse of the other, up to nonempty isomorphism.

Example 4.2**.**

Consider the standard abstract domain for sign analysis as encoded by the GI $\mathcal{S}=\langle\alpha,\wp(\mathbb{Z}),\operatorname{Sign},\gamma\rangle$, where $\operatorname{Sign}$ is the following lattice:

\mathbb{Z}$$\geq 0$$\neq 0$$\leq 0$$>0$$<0$$=0$$\varnothing

while abstraction and concretization maps are defined as usual. Let us observe that $\mathcal{S}$ is indeed a PGC (more precisely, a PGI), where $\operatorname{prt}(\mathcal{S})=\{\mathbb{Z}_{<0},\mathbb{Z}_{=0},\mathbb{Z}_{>0}\}$. Then, $\mathbb{T}_{\text{CGC}}(\mathcal{S})$ provides a CGC which is nonempty isomorphic to the CGC $\mathcal{C}=\langle\beta,\mathbb{Z},B^{\prime},\delta\rangle$ of Example 3.3: these two CGCs only differ for the element $\bot\in B^{\prime}$ whose meaning is $\varnothing=\delta(\bot)$. Conversely, $\mathbb{T}_{\text{PGC}}(\mathcal{C})$ is a PGC which is isomorphic to the PGI $\mathcal{S}$: $\wp(B^{\prime})$ is the abstract domain of $\mathbb{T}_{\text{PGC}}(\mathcal{C})$, so that, since $B^{\prime}$ includes the “useless” value $\bot$, we obtain a PGC rather than a PGI, because its concretization map $\delta^{*}$ is not injective, e.g., $\delta^{*}(\{\bot,+\})=\delta^{*}(\{\bot\})$. ∎

Furthermore, it turns out that the CGC/PGC transforms of Theorem 4.1 preserve the relative precision relations as follows.

Corollary 4.3**.**

If $\mathcal{C}_{1}$ and $\mathcal{C}_{2}$ are CGCs then $\mathcal{C}_{1}\sqsubseteq\mathcal{C}_{2}$ iff $\mathbb{T}_{\text{PGC}}(\mathcal{C}_{1})$ $\sqsubseteq$ $\mathbb{T}_{\text{PGC}}(\mathcal{C}_{2})$.

As a consequence, one can define a lattice of CGCs, ordered w.r.t. their relative precision up to isomorphism, which is order-theoretically isomorphic to the so-called lattice of partitioning abstract domains [19, Theorem 3.2].

Let us also recall that [8] also put forward a definition of Kleisli Galois connection (KGC) between posets, which relies on a “monadic” notion of abstraction/concretization maps. Actually, this class of constructive abstractions is shown in [8, Section 6] to be equivalent to CGCs, where this isomorphism includes the notion of soundness (and optimality) for abstract functions. Hence, we do not need to replicate our isomorphism between KGCs and PGCs, which automatically follows.

CGCs as Least Disjunctive Bases.

Given a CGC $\mathcal{C}=\langle\eta,A,B,\mu\rangle$, Theorem 4.1 shows that $\mathbb{T}_{\text{PGC}}(\mathcal{C})=\langle\eta^{\diamond},\wp(A)_{\subseteq},\wp(B)_{\subseteq},\mu^{*}\rangle$ is a PGC. We observe that $\{\{x\}~{}|~{}x\in B\}$ is the set of join-irreducible elements of the complete lattice $\wp(B)_{\subseteq}$ — recall that an element $x$ of a complete lattice is join-irreducible when, for any $S$, $x=\vee S\Rightarrow x\in S$. In abstract interpretation terms [9], this observation means that $\{\{x\}~{}|~{}x\in B\}$ can be essentially viewed as the so-called least disjunctive basis of the partitioning abstract domain $\wp(B)_{\subseteq}$. Least disjunctive basis have been introduced in [9] as an inverse operation to the disjunctive completion of abstract domains, that is, the least disjunctive refinement of an abstract domain $D$. Given an abstract domain $D$, its least disjunctive basis is defined to be the most abstract domain having the same disjunctive completion as $D$. Hence, the least disjunctive basis of $D$ reveals and therefore removes all the disjunctive information inside $D$. A concrete domain which is a powerset (ordered by subset inclusion) satisfies the hypotheses of [9, Theorem 4.13], so that the least disjuctive basis of an abstract domain $D$ exists and is characterized as the closure under arbitrary meets of the join-irreducible elements of $D$. This result can be applied to the abstract domain $\wp(B)_{\subseteq}$ of the PGC $\mathbb{T}_{\text{PGC}}(\mathcal{C})$, whose least disjunctive basis is given by the meet-closure of $\{\{x\}~{}|~{}x\in B\}$, where this meet-closure simply adds $\varnothing$ and $B$. In this sense, this section systematically reconstructed the notion of CGC as least disjunctive basis of a partitioning abstract domain.

Constructive Closure Operators.

In abstract interpretation, abstract domains up to renaming of abstract values are encoded by closure operators, which are isomorphic to GCs [4]. Hence, the isomorphism between CGCs and PGCs in Theorem 4.1 leads to the following notion. Given any set $A$, a map $\varphi:A\rightarrow\wp(A)$ is a constructive closure operator (CCO) when the following condition holds: $x\in\varphi(y)\>\Leftrightarrow\>\varphi(x)=\varphi(y)$.

CCOs turn out to be the closure operator counterpart of CGCs, as shown by the following result.

Corollary 4.4** (CGC-CCO Equivalence).**

• (1)

If $\mathcal{C}=\langle\eta,A,B,\mu\rangle$ is a CGC then $\mathbb{T}_{\text{CCO}}$ $(\mathcal{C})\triangleq\mu\circ\eta:A\rightarrow\wp(A)$ is a CCO.

• (2)

If $\varphi:A\rightarrow\wp(A)$ is a CCO then $\mathbb{T}_{\text{CGC}}$ $(\varphi)\triangleq\langle\varphi,A,\{\varphi(a)~{}|~{}a\in A\},\mathrm{id}\rangle$ is a CGC.

• (3)

The transforms $\mathbb{T}_{\text{CCO}}$ and $\mathbb{T}_{\text{CGC}}$ are one the inverse of the other, up to nonempty isomorphism.

4.1 Characterization of CGPs

Let us now focus on CGPs. Can this class of constructive abstractions be characterized in terms of Galois connections? Let the carrier concrete set $A$ be a poset, the abstract domain $B$ be a complete lattice, $\eta:A\rightarrow B$ and $\mu:B\rightarrow{\wp^{\downarrow}}(A)$ be monotone. By relying on CGPs/GCs transforms, we show that the class of CGPs turns out to be isomorphic to the class of GCs of the concrete powerdomain ${\wp^{\downarrow}}(A)$.

Theorem 4.5** (CGP-GC Equivalence).**

• (1)

If $\mathcal{C}=\langle\eta,A,B,\mu\rangle$ is a CGP then $\mathbb{T}_{\text{GC}}(\mathcal{C})\triangleq\langle\eta^{\vee},{\wp^{\downarrow}}(A)_{\subseteq},B,\mu\rangle$ is a GC.

• (2)

If $\mathcal{G}=\langle\alpha,{\wp^{\downarrow}}(A)_{\subseteq},D_{\leq},\gamma\rangle$ is a GC then $\mathbb{T}_{\text{CGP}}(\mathcal{G})\triangleq\langle\lambda a.\alpha(\downarrow\!\!\{a\}),A,D,\gamma\rangle$ is a CGP.

• (3)

The transforms $\mathbb{T}_{\text{GC}}$ and $\mathbb{T}_{\text{CGP}}$ are one the inverse of the other, up to isomorphism between GCs.

Otherwise stated, this result shows that CGPs, specifically defined for adapting CGCs to carrier sets which are posets, indeed boil down to plain GCs of the powerdomain ${\wp^{\downarrow}}(A)$, and therefore lose their constructive attribute.

Example 4.6**.**

Consider the following lattice $D$ of integer intervals ordered by subset inclusion:

\mathbb{Z}$$[-9,+\infty)$$[-7,7]$$[1,5]$$[-5,-1]$$\varnothing

By considering $\mathbb{Z}$ as discretely ordered, this lattice $D$ gives rise to a GI $\mathcal{G}=\langle\alpha,\wp(\mathbb{Z}),D,\gamma\rangle$ where $\gamma$ is the identity and, for example, we have that $\alpha(\{2\})=[1,5]$, $\alpha(\{0\})=\alpha(\{6\})=[-7,7]$, $\alpha(\{10\})=[-9,+\infty)$, $\alpha(\{-10\})=\mathbb{Z}$. Then, by Theorem 4.5 (2), $\mathbb{T}_{\text{CGP}}(\mathcal{G})=\langle\lambda z.\alpha(\{z\}),\mathbb{Z},D,\gamma\rangle$ is a CGP. Ler us remark that the GI $\mathcal{G}$ is neither partitioning nor disjunctive, so that the intuition is that the CGP $\mathbb{T}_{\text{CGP}}(\mathcal{G})$ should not be considered as being “constructive”. As a limit infinite example, consider the complete lattice $E\triangleq\{[0,n]~{}|~{}n\in\mathbb{N}\}\cup\{\mathbb{N}\}$, ordered by subset inclusion, which is an infinite increasing chain of intervals of natural numbers. This complete lattice gives rise to a GI $\mathcal{E}=\langle\alpha,\wp(\mathbb{N}),E,\gamma\rangle$ where $\mathbb{N}$ is discretely ordered and $\gamma$ is the identity. Here, Theorem 4.5 (2) yields a legal CGP $\mathbb{T}_{\text{CGP}}(\mathcal{E})=\langle\eta,\mathbb{N},E,\mathrm{id}\rangle$ where $\eta(n)=[0,n]$ and whose constructive trait can hardly be identifiable. ∎

5 Soundness of Abstract Operations

Our next objective is to transform a sound pair of functions from CGCs to PGCs and vice versa, in order to show that the equivalence between CGCs and PGCs also include soudness (and further optimality conditions) of abstract functions. For notational simplicity, we consider unary functions, but the whole approach can be straighforwardly generalized to generic $n$-ary functions (that we will use in some examples).

Let $\mathcal{C}=\langle\eta,A,B,\mu\rangle$ be a CGC, $f:A\rightarrow A$ be a concrete function and $f_{\sharp}:B\rightarrow B$ be a corresponding abstract function. Let us recall that Darais and Van Horn [8] provide four equivalent soudness conditions for $\langle f,f_{\sharp}\rangle$ to be sound w.r.t. $\mathcal{C}$:

[TABLE]

On the one hand, on the transformed PGC $\mathbb{T}_{\text{PGC}}(\mathcal{C})=\langle\eta^{\diamond},\wp(A)_{\subseteq},\wp(B)_{\subseteq},\mu^{*}\rangle$, we simply the powerset lifting of concrete and abstract functions, namely, we define $\mathbb{T}_{\text{PGC}}(\langle f,f_{\sharp}\rangle)\triangleq\langle f^{\diamond},f_{\sharp}^{\diamond}\rangle$, where $f^{\diamond}:\wp(A)\rightarrow\wp(A)$ and $f_{\sharp}^{\diamond}:\wp(B)\rightarrow\wp(B)$.

On the other hand, let $\mathcal{G}=\langle\alpha,\wp(A)_{\subseteq},D_{\leq},\gamma\rangle$ be a PGC. On PGCs, we consider concrete functions on $\wp(A)$ which are defined as collecting version of a mapping $g:A\rightarrow A$ on the carrier set $A$, that is, $g^{\diamond}:\wp(A)\rightarrow\wp(A)$ will be our concrete function. A corresponding monotone abstract function $g_{\sharp}:D\rightarrow D$ is called block-preserving when $g_{\sharp}$ maps (abstract representations of) blocks to (abstract representations of) blocks, namely, when the following condition holds: $\forall a\in A.\exists a^{\prime}\in A.\>g_{\sharp}(\alpha(\{a\}))=\alpha(\{a^{\prime}\})$.

Lemma 5.1**.**

If $\mathcal{G}$ is a PGI, $\langle g^{\diamond},g_{\sharp}\rangle$ is sound and $g_{\sharp}$ is block-preserving then, for any $a\in A$, $g_{\sharp}(\alpha(\{a\}))=\alpha(\{g(a)\})$ and $g^{\diamond}(\gamma(\alpha(\{a\})))\subseteq\gamma(\alpha(\{g(a)\}))$.

Thus, given a sound pair $\langle g^{\diamond},g_{\sharp}\rangle$ w.r.t. $\mathcal{G}$ where $g_{\sharp}$ is block preserving, on the transformed CGC $\mathbb{T}_{\text{CGC}}(\mathcal{G})=\langle{\alpha^{\scriptscriptstyle\{\!\cdot\!\}}},A,\{\alpha(\{a\})~{}|~{}a\in A\},\gamma\rangle$ we consider the carrier concrete function $g:A\rightarrow A$ and the following restriction of the abstract function $g_{\sharp}$ to abstract representations of blocks: $g_{\sharp}^{r}:\{\alpha(\{a\})~{}|~{}a\in A\}\rightarrow\{\alpha(\{a\})~{}|~{}a\in A\}$ which, by Lemma 5.1, can be defined as $g_{\sharp}^{r}(\alpha(\{a\}))\triangleq\alpha(\{g(a)\})$. We denote this transform by $\mathbb{T}_{\text{CGC}}(\langle g^{\diamond},g_{\sharp}\rangle)\triangleq\langle g,g_{\sharp}^{r}\rangle$.

Given two CGCs $\mathcal{C}_{i}=\langle\eta_{i},A,B_{i},\mu_{i}\rangle$, $i=1,2$, a concrete function $f:A\rightarrow A$ and two corresponding abstract functions $f^{\sharp}_{i}:B_{i}\rightarrow B_{i}$, we use the notation $\langle f,f_{1}^{\sharp}\rangle\cong\langle f,f_{2}^{\sharp}\rangle$ to mean that $f_{i}$ is sound for $f$ w.r.t. $\mathcal{C}_{i}$ and $\mu_{1}\circ f_{1}^{\sharp}\circ\eta_{1}=\mu_{2}\circ f_{2}^{\sharp}\circ\eta_{2}$, that is, the concrete projections of $f_{1}^{\sharp}$ and $f_{2}^{\sharp}$ coincide so that these functions can be viewed as isomorphic. With this notion, our correspondance between CGCs and PGCs can be extended to include soundness as follows.

Theorem 5.2**.**

• (1)

Let $\mathcal{C}=\langle\eta,A,B,\mu\rangle$ be a CGC, $f:A\rightarrow A$ and $f_{\sharp}:B\rightarrow B$. Then, $\langle f,f_{\sharp}\rangle$ is sound iff $\mathbb{T}_{\text{PGC}}(\langle f,f_{\sharp}\rangle)$ is sound w.r.t. $\mathbb{T}_{\text{PGC}}(\mathcal{C})$.

• (2)

Let $\mathcal{G}=\langle\alpha,\wp(A)_{\subseteq},D_{\leq},\gamma\rangle$ be a PGC, $g^{\diamond}:\wp(A)\rightarrow\wp(A)$, for some $g:A\rightarrow A$, and $g_{\sharp}:D\rightarrow D$ be monotone and block-preserving. Then, $\langle g^{\diamond},g_{\sharp}\rangle$ is sound iff $\mathbb{T}_{\text{CGC}}(\langle g^{\diamond},g_{\sharp}\rangle)$ is sound w.r.t. $\mathbb{T}_{\text{CGC}}(\mathcal{G})$.

• (3)

If $\langle f,f_{\sharp}\rangle$ is sound then $\mathbb{T}_{\text{CGC}}(\mathbb{T}_{\text{PGC}}(\langle f,f_{\sharp}\rangle))$ $\cong\langle f,f_{\sharp}\rangle$. If $\langle g^{\diamond},g_{\sharp}\rangle$ is sound and $g_{\sharp}$ is block-preserving and additive then $\mathbb{T}_{\text{PGC}}(\mathbb{T}_{\text{CGC}}(\langle g^{\diamond},g_{\sharp}\rangle))$ $\cong\langle g^{\diamond},g_{\sharp}\rangle$.

Example 5.3**.**

Consider the PGI $\mathcal{S}=\langle\alpha,\wp(\mathbb{Z}),\operatorname{Sign},\gamma\rangle$ for the standard sign domain introduced in Example 4.2. Consider the square operation $\operatorname{sq}:\mathbb{Z}\rightarrow\mathbb{Z}$ such that $\operatorname{sq}(z)=z^{2}$ and its collecting lifting $\operatorname{sq}^{\diamond}:\wp(\mathbb{Z})\rightarrow\wp(\mathbb{Z})$. Correspondingly, consider $\operatorname{sq}_{\mathcal{S}}:\operatorname{Sign}\rightarrow\operatorname{Sign}$ defined as BCA of $\operatorname{sq}^{\diamond}$, namely:

[TABLE]

Then, let us observe that $\operatorname{sq}_{\mathcal{S}}$ is (monotone and) block-preserving: indeed, the set of (abstract) blocks is $B=\{<\!0,\,=\!0,\,>\!0\}$ and $\operatorname{sq}_{\mathcal{S}}$ maps blocks to blocks. Hence, here we have that $\mathbb{T}_{\text{CGC}}(\mathcal{S})=\langle\eta,\mathbb{Z},B,\mu\rangle$ and $\mathbb{T}_{\text{CGC}}(\langle\operatorname{sq}^{\diamond},\operatorname{sq}_{\mathcal{S}}\rangle)=\langle\operatorname{sq},\operatorname{sq}_{\mathcal{S}}^{r}\rangle$ where $\operatorname{sq}_{\mathcal{S}}^{r}:\mathbb{Z}\rightarrow\mathbb{Z}$ is such that $\operatorname{sq}_{\mathcal{S}}^{r}(\alpha(\{z\}))=\alpha(\{\operatorname{sq}(z)\})$. ∎

Completeness.

As observed in [8], the above four equivalent soundness conditions for CGCs lead to four non-equivalent conditions of completeness for abstract functions, where $\Leftrightarrow$ replaces $\Rightarrow$:

[TABLE]

It is worth remarking that these completeness conditions for a pair $\langle f,f_{\sharp}\rangle$ can be equivalently stated using well known optimality/completeness conditions for Galois connections for the transformed pair $\mathbb{T}_{\text{PGC}}(\langle f,f_{\sharp}\rangle)$.

Lemma 5.4**.**

• (1)

$\langle f,f_{\sharp}\rangle$* satisfies (CGC-Cmp/$\eta\mu$) iff $\mathbb{T}_{\text{PGC}}(\langle f,f_{\sharp}\rangle)$ is best correct approximation w.r.t. $\mathbb{T}_{\text{PGC}}(\mathcal{C})$.*

• (2)

$\langle f,f_{\sharp}\rangle$* satisfies (CGC-Cmp/$\mu\mu$) iff $\mathbb{T}_{\text{PGC}}(\langle f,f_{\sharp}\rangle)$ is forward complete w.r.t. $\mathbb{T}_{\text{PGC}}(\mathcal{C})$.*

• (3)

$\langle f,f_{\sharp}\rangle$* satisfies (CGC-Cmp/$\eta\eta$) iff $\mathbb{T}_{\text{PGC}}(\langle f,f_{\sharp}\rangle)$ is backward complete w.r.t. $\mathbb{T}_{\text{PGC}}(\mathcal{C})$.*

• (4)

$\langle f,f_{\sharp}\rangle$* satisfies (CGC-Cmp/$\mu\eta$) iff $\mathbb{T}_{\text{PGC}}(\langle f,f_{\sharp}\rangle)$ is precise w.r.t. $\mathbb{T}_{\text{PGC}}(\mathcal{C})$.*

6 Purely Partitioning Galois Connections

Drawing on the above results, we define a novel class of constructive abstract domains, which we call purely constructive Galois connections (PCGCs). The idea is that PCGCs generalize CGCs as follows. CGCs essentially represent a partition of the carrier concrete domain $A$ as an abstract domain $B$. We showed that this partition representation also brings all the possible unions of its blocks. The goal is to generalize this approach by allowing to decide which unions of blocks to consider in the abstract domain $B$. Hence, $B$ may be defined as a partition $P$ of $A$ together with an explicit selection of unions of blocks of $P$, where this selection may range from none to all.

A purely constructive Galois connection (PCGC) $\langle\eta,A,B,\mu\rangle_{\text{PCGC}}$ consists of an unordered concrete carrier set $A$ and of an ordered abstract domain which is required to be a poset $\langle B,\leq\rangle$, together with the mappings $\eta:A\rightarrow B$ and $\mu:B\rightarrow\wp(A)$ which satify the following two conditions:

[TABLE]

Thus, condition (2) coincides with (CGP-Corr), while condition (1) amounts to (CGC-Corr) restricted to abstract values ranging in $\eta(A)$. PCGCs have the following properties.

Lemma 6.1** (PCGC properties).**

Consider a PCGC $\langle\eta,A,B_{\leq},\mu\rangle$.

• (1)

$\eta(a_{1})=\eta(a_{2})\>\Leftrightarrow\>\mu(\eta(a_{1}))=\mu(\eta(a_{2}))\>\Leftrightarrow\>\mu(\eta(a_{1}))\cap\mu(\eta(a_{2}))\neq\varnothing$**

• (2)

$\mu(b)=\varnothing\>\Rightarrow\>b\not\in\eta(A)$, while the viceversa does not hold

• (3)

If $B$ is a complete lattice then $\langle\eta^{\vee},\wp(A)_{\subseteq},B_{\leq},\mu\rangle$ is a GC

In particular, let us remark that: by Lemma 6.1 (1), $\{\mu(\eta(a))\}_{a\in A}$ still is a partition of $A$; by Lemma 6.1 (2), differently from CGCs, if $b\not\in\eta(A)$ it may happen that $\mu(b)\neq\varnothing$; by Lemma 6.1 (3), analogously to CGPs, $\eta^{\vee}$ and $\mu$ give rise to a GC.

Example 6.2**.**

Consider the following finite lattice $B$ of integer intervals ordered by subset inclusion:

\mathbb{Z}$$[-9,+\infty)$$(-\infty,9]$$[-9,9]$$[10,+\infty)$$[1,9]$$[0,0]$$[-9,-1]$$(-\infty,-10]$$\varnothing

Let $\eta:\mathbb{Z}\rightarrow B$ be defined as follows:

[TABLE]

while $\mu:B\rightarrow\wp(\mathbb{Z})$ is simply defined as the identity map. Then, it is simple to check that $\mathcal{P}=\langle\eta,\mathbb{Z},B,\mu\rangle$ is a PCGC. However, it turns out that $\mathcal{P}$ is not a CGC: in fact, $0\in\mu([-9,9])$ while $\eta(0)=[0,0]\neq[-9,9]$. Also, if $\mathbb{Z}$ is considered as a poset w.r.t. the discrete order then ${\wp^{\downarrow}}(\mathbb{Z})=\wp(\mathbb{Z})$ and $\eta$ and $\mu$ are monotone, so that, by PCGC (2), $\mathcal{P}$ is a CGP. Consider now $B^{\prime}\triangleq(B\smallsetminus\{[-9,9],(-\infty,9],[-9,+\infty)\})\cup\{[-10,10]\}$, which still is a finite lattice where $[-10,10]$ is the lub in $B^{\prime}$ of $\{[-9,-1],[0,0],[1,9]\}$, although $[-10,10]$ is not the union of these blocks. In this case, $\langle\eta,\mathbb{Z},B^{\prime},\mu\rangle$ is not a PCGC, because $10\in\mu([-10,10])$ but $\eta(10)=[10,+\infty)\not\subseteq[-10,10]$, so that PCGC (2) does not hold. Finally, consider the CGC $\mathcal{C}=\langle\eta,\mathbb{Z},B,\mu\rangle$ defined in Example 3.3. Then, $\mathcal{C}$ is not a PCGC because $1\in\mu(\eta(0))=\mathbb{Z}$ but $+=\eta(1)\neq\eta(0)=\top$. ∎

Similarly to Theorems 4.1 and 4.5, let us now characteriza PCGCs as a class of Galois connections. Recall that a GC $\mathcal{G}=\langle\alpha,\wp(A)_{\subseteq},D_{\leq},\gamma\rangle$ is a PGC when $\operatorname{prt}(\mathcal{G})$ is a partition of $A$ and $\gamma$ is additive. By dropping this latter requirement of additivity for $\gamma$, we define $\mathcal{G}$ to be a purely partitioning Galois connection (PPGC) just when $\operatorname{prt}(\mathcal{G})$ is a partition of $A$. The terminology “purely partitioning” hints at the property (which is not hard to check) that the disjunctive completion of $D$ indeed yields a partitioning Galois connection. It turns out that this class of GCs characterize PCGCs as follows.

Theorem 6.3** (PCGC-PPGC Equivalence).**

• (1)

If $B_{\leq}$ is a complete lattice and $\mathcal{C}=\langle\eta,A,B_{\leq},\mu\rangle$ is a PCGC then $\mathbb{T}_{\text{PPGC}}(\mathcal{C})$ $\triangleq\langle\eta^{\vee},\wp(A)_{\subseteq},B_{\leq},\mu\rangle$ is a PPGC.

• (2)

If $\mathcal{G}=\langle\alpha,\wp(A)_{\subseteq},D_{\leq},\gamma\rangle$ is a PPGC then $\mathbb{T}_{\text{PCGC}}(\mathcal{G})$ $\triangleq\langle{\alpha^{\scriptscriptstyle\{\!\cdot\!\}}},A,D_{\leq},\gamma\rangle$ is a PCGC.

• (3)

The transforms $\mathbb{T}_{\text{PPGC}}$ and $\mathbb{T}_{\text{PCGC}}$ are one the inverse of the other, up to isomorphism.

Example 6.4**.**

Consider the PCGC $\mathcal{P}$ defined in Example 6.2, so that $\mathbb{T}_{\text{PPGC}}(\mathcal{P})=\langle\eta^{\vee},\wp(\mathbb{Z})_{\subseteq},B_{\leq},\mathrm{id}\rangle$ is a PPGC where the corresponding partition of $\mathbb{Z}$ is $P=\{(-\infty,10],[-9,-1],$ $[0,0],[1,9],[10,+\infty)\}$ and the abstraction map $\eta^{\vee}$ approximates a set of integers $X\in\wp(\mathbb{Z})$ by the least union of blocks of $P$ which belongs to $B$: for example, $\eta^{\vee}(\{1,10\})=[-9,+\infty)$ and $\eta^{\vee}(\{0,1\})=[-9,9]$. ∎

CGCs as PCGCs as CGPs.

It turns out that any CGC is indeed a PCGC, which, in turn, is a CGP. Let $\langle\eta,A,B,\mu\rangle$ be a CGC. Firstly, it is enough to consider $B$ as a poset for the discrete partial order $\leq$, since this makes $\langle\eta,A,B_{\leq},\mu\rangle$ a PCGC. In fact: (1) $a\in\mu(\eta(a^{\prime}))$ iff, by (CGC-Corr), $\eta(a)=\eta(a^{\prime})$; (2) if $b\in\eta(A)$ then $b=\eta(a^{\prime})$, for some $a^{\prime}$, so that, by (CGC-Corr), $a\in\mu(b)\Leftrightarrow\eta(a)=b$, while if $b\not\in\eta(A)$, then, by Lemma 3.1 (2), $\mu(b)=\varnothing$. Furthermore, any PCGC $\langle\eta,A,B_{\leq},\mu\rangle$ can be viewed as a CGP simply by making the concrete carrier set $A$ a poset for the discrete order, so that ${\wp^{\downarrow}}(A)=\wp(A)$, and $\eta$ becomes trivially monotone as well as $\mu:B\rightarrow\wp(A)$: in fact, if $b_{1}\leq b_{2}$ and $a\in\mu(b_{1})$ then $\eta(a)\leq b_{1}\leq b_{2}$, so that $a\in\mu(b_{2})$.

6.1 Soundness of Abstract Operations

Let $\mathcal{C}=\langle\eta,A,B_{\leq},\mu\rangle$ be a PCGC and $f:A\rightarrow A$ be a concrete function. By relying on Theorem 6.3 (1), we are able to define the BCA of the lifted function $f^{\diamond}:\wp(A)\rightarrow\wp(A)$ w.r.t. the PPGC $\langle\eta^{\vee},\wp(A)_{\subseteq},B_{\leq},\mu\rangle=\mathbb{T}_{\text{PPGC}}(\mathcal{C})$. This is denoted by $f_{\mathcal{C}}:B\rightarrow B$ and is therefore defined by $f_{\mathcal{C}}\triangleq\eta^{\vee}\circ f^{\diamond}\circ\mu$, so that:

[TABLE]

Hence, given an abstract function $f_{\sharp}:B\rightarrow B$, this BCA leads us to define $\langle f,f^{\sharp}\rangle$ to be sound for $\mathcal{C}$ when $f_{\sharp}$ is less precise than the BCA, that is, when for any $b\in B$, $f_{\mathcal{C}}(b)\leq f_{\sharp}(b)$. This turns out to be equivalent to the following condition: $\langle f,f^{\sharp}\rangle$ is sound w.r.t. $\mathcal{C}$ iff

[TABLE]

It is then easy to transform a sound pair of concrete/abstract functions $\langle f,f_{\sharp}\rangle$ for a PCGC $\mathcal{C}$ into the pair $\mathbb{T}_{\text{PPGC}}(\langle f,f_{\sharp}\rangle)\triangleq\langle f^{\diamond},f_{\sharp}\rangle$ for the corresponding PPGC $\mathbb{T}_{\text{PPGC}}(\mathcal{C})=\langle\eta^{\vee},\wp(A)_{\subseteq},B_{\leq},\mu\rangle$. Conversely, if $\mathcal{D}=\langle\alpha,\wp(A)_{\subseteq},D_{\leq},\gamma\rangle$ is a PPGC and $\langle g^{\diamond},g_{\sharp}\rangle$ is a sound pair for $\mathcal{D}$, where $g^{\diamond}:\wp(A)\rightarrow\wp(A)$ for some $g:A\rightarrow A$, then $\langle g^{\diamond},g_{\sharp}\rangle$ is transformed into $\mathbb{T}_{\text{PCGC}}(\langle g^{\diamond},g_{\sharp}\rangle)\triangleq\langle g,g_{\sharp}\rangle$ relatively to the PCGC $\mathbb{T}_{\text{PCGC}}(\mathcal{D})$. A result analogous to Theorem 5.2 can then be proved.

Theorem 6.5**.**

• (1)

Let $\mathcal{C}=\langle\eta,A,B_{\leq},\mu\rangle$ be a PCGC, with $B$ complete lattice, $f:A\rightarrow A$ and $f_{\sharp}:B\rightarrow B$. Then, $\langle f,f_{\sharp}\rangle$ is sound iff $\mathbb{T}_{\text{PPGC}}(\langle f,f_{\sharp}\rangle)$ is sound w.r.t.  $\mathbb{T}_{\text{PPGC}}(\mathcal{C})$.

• (2)

Let $\mathcal{D}=\langle\alpha,\wp(A)_{\subseteq},D_{\leq},\gamma\rangle$ be a PPGC, $g^{\diamond}:\wp(A)\rightarrow\wp(A)$, for some $g:A\rightarrow A$, and $g_{\sharp}:D\rightarrow D$. Then, $\langle g^{\diamond},g_{\sharp}\rangle$ is sound iff $\mathbb{T}_{\text{PCGC}}(\langle g^{\diamond},g_{\sharp}\rangle)$ is sound w.r.t. $\mathbb{T}_{\text{PCGC}}(\mathcal{D})$.

• (3)

The transforms $\mathbb{T}_{\text{PPGC}}$ and $\mathbb{T}_{\text{PCGC}}$ are one the inverse of the other.

Since $f_{\sharp}$ is defined to be sound when $\eta^{\vee}\circ f^{\diamond}\circ\mu\leq f_{\sharp}$, it is then natural to define $f_{\sharp}$ optimal when $\eta^{\vee}\circ f^{\diamond}\circ\mu=f_{\sharp}$, backward complete when $\eta^{\vee}\circ f^{\diamond}=f_{\sharp}\circ\eta^{\vee}$ and forward complete when $f^{\diamond}\circ\mu=\mu\circ f_{\sharp}$. In particular, these definitions allow us to apply the abstraction refinement operators introduced in [11] for minimally refining the abstract domain $B$ in order to obtain a backward/forward complete abstract function and the technique introduced in [10] for simplifying abstract domains while retaining the optimality of abstract operations.

6.2 An Example of PCGC

Consider the following infinite complete lattice $B_{\leq}$.

\mathbb{Z}$$\geq 0$$\neq 0$$\leq 0$$>0$$<0$$2$$1[math]-1$$-2$$\cdots$$\cdots$$\cdots$$\cdots$$\cdots$$\cdots$$\varnothing

$B$ is intended to be an abstract domain which includes both constant and sign information of an integer variable. Indeed $B$ can be defined as reduced product of the standard constant propagation domain [16] and of the sign abstraction in Example 4.2. For example, for a while program such as:

[TABLE]

a standard analysis with this abstract domain $B$ allows us to derive the loop invariant $\{x>0,\>y=2\}$.

It turns out that the abstraction $B$ can be constructively defined. This definition of $B$ relies on $\eta:\mathbb{Z}\rightarrow B$ and $\mu:B\rightarrow\wp(\mathbb{Z})$ which are essentially defined as identity functions. It should be clear that $B$ is a purely partitioning domain, while it is not a fully partitioning domain, and therefore $B$ cannot be equivalently defined within the constructive Galois connection approach. In fact, $\mathcal{C}=\langle\eta,\mathbb{Z},B,\mu\rangle$ is not a CGC, because $1\in\mu(>\!0)$ while $1=\eta(1)\neq\;>\!0$. Instead, $\mathcal{C}$ turns out to be a PCGC.

Next, consider the concrete binary integer multiplication $\otimes:\mathbb{Z}\times\mathbb{Z}\rightarrow\mathbb{Z}$. By following Theorem 6.5 (1), we define a corresponding abstract multiplication $\otimes_{\sharp}:B\times B\rightarrow B$ as follows:

[TABLE]

Namely, $\otimes_{\sharp}$ is the best correct approximation of the powerset lifting $\otimes^{\diamond}:\wp(\mathbb{Z})\times\wp(\mathbb{Z})\rightarrow\wp(\mathbb{Z})$ w.r.t. the PPGC $\langle\eta^{\vee},\wp(\mathbb{Z})_{\subseteq},B_{\leq},\mu\rangle=\mathbb{T}_{\text{PPGC}}(\mathcal{C})$. For instance, $\otimes_{\sharp}(2,<\!0)=\><\!0$ and $\otimes_{\sharp}(-2,\leq 0)=\>\geq 0$. Then, since $\langle\otimes^{\diamond},\otimes_{\sharp}\rangle$ is sound, by construction, for $\mathbb{T}_{\text{PPGC}}(\mathcal{C})$, we have that $\langle\otimes,\otimes_{\sharp}\rangle$ is sound for $\mathcal{C}$. Furthermore, as expected, it turns out that $\otimes_{\sharp}$ is backward complete for $\mathcal{C}$, meaning that for any $X,Y\in\wp(\mathbb{Z})$, $\vee_{B}\{x\otimes y~{}|~{}x\in X,y\in Y\}=\otimes_{\sharp}(\vee_{B}X,\vee_{B}Y)$. For instance, we have that:

[TABLE]

7 Conclusion

This paper showed that constructive Galois connections, proposed by Darais and Van Horn [8] as a way to define domains to be used in a mechanized and calculational style of abstract interpretation, are isomorphic to an already known class of Galois connections which formalize partitions of an unordered set as an abstract domain. Building on that, we defined a novel class of constructive abstract domains for a mechanized approach to abstract interpretation, called purely constructive Galois connections. We showed that this class of abstract domains permits to represent a set partition with more flexibility while preserving a constructive approach to Galois connections.

Appendix A Proofs

See 3.1

Proof.

Firstly, let us observe that for any $a\in A$, $a\in\mu(\eta(a))$.

(1) If $\mu(\eta(a_{1}))=\mu(\eta(a_{2}))$ then $a_{1}\in\mu(\eta(a_{1}))=\mu(\eta(a_{2}))$ so that, by (CGC-Corr), $\eta(a_{1})=\eta(a_{2})$. Next, we show that $\mu(\eta(a_{1}))=\mu(\eta(a_{2}))\>\Leftrightarrow\>\exists a\in A.a\in\mu(\eta(a_{1}))\cap\mu(\eta(a_{2}))$: on the one hand, since $a_{1}\in\mu(\eta(a_{1}))$ then $a_{1}\in\mu(\eta(a_{2}))$; on the other hand, if $a\in\mu(\eta(a_{1}))\cap\mu(\eta(a_{2}))$, then, by (CGC-Corr), $\eta(a_{1})=\eta(a)=\eta(a_{2})$, so that $\mu(\eta(a_{1}))=\mu(\eta(a_{2}))$.

(2) Let us check that $\mu(b)\neq\varnothing\>\Leftrightarrow\>b\in\eta(A)$: there exists $a\in\mu(b)$ iff, by (CGC-Corr), there exists $a\in A$ such that $\eta(a)=\eta(b)$ iff $b\in\eta(A)$. ∎

See 3.2

Proof.

(1) If $\mu(\eta(a_{1}))=\mu(\eta(a_{2}))$ then $a_{1}\in\mu(\eta(a_{2}))$ and $a_{2}\in\mu(\eta(a_{1}))$, so that, by (CGP-Corr), $\eta(a_{1})\leq_{B}\eta(a_{2})\leq\eta(a_{1})$.

(2) If $a\in\mu(b)$ then, by (CGP-Corr), $\eta(a)\leq_{B}b$, so that $\eta(a)\in\>\downarrow\!\!b\cap\eta(A)$. Conversely, if $b^{\prime}\in\>\downarrow\!\!b\cap\eta(A)$ then $b^{\prime}=\eta(a^{\prime})\leq_{B}b$, for some $a^{\prime}\in A$, so that, by (CGP-Corr), $a^{\prime}\in\mu(b)$.

(3) Let us check that for all $X\in{\wp^{\downarrow}}(A)$ and $b\in B$, $\eta^{\vee}(X)\leq_{B}b\Leftrightarrow X\subseteq\mu(b)$: $\eta^{\vee}(X)\leq_{B}b$ iff $\vee_{a\in X}\eta(a)\leq_{B}b$ iff $\forall a\in X.\>\eta(a)\leq_{B}b$ iff $\forall a\in X.\>a\in\mu(b)$ iff $X\subseteq\mu(b)$.

(4) Since, by (3), $\langle\eta^{\vee},{\wp^{\downarrow}}(A),B,\mu\rangle$ is a GC, we have that $\mu=\mu\circ\eta^{\vee}\circ\mu$, so that $\mu(B)=\mu({\eta^{\vee}}({\wp^{\downarrow}}(A)))$ follows. ∎

See 3.4

Proof.

$(\Rightarrow)$ For any $a\in A$, we have that $\mu_{1}(\eta_{1}(a))\in\mu_{2}(B_{2})$, so that $\mu_{1}(\eta_{1}(a))=\mu_{2}(b_{2})$ for some $b_{2}\in B_{2}$. Then, since $a\in\mu_{2}(b_{2})$, by Lemma 3.1 (2), $b_{2}\in\eta_{2}(A)$, so that there exists some $x^{2}_{a}\in A$ such that $b_{2}=\eta_{2}(x^{2}_{a})$ and, in turn, $\mu_{1}(\eta_{1}(a))=\mu_{2}(\eta_{2}(x^{2}_{a}))$. We define $f_{1,2}(\eta_{1}(a))\triangleq\eta_{2}(x^{2}_{a})$. Dually, for any $a\in A$ there exists $x^{1}_{a}\in A$ such that $\mu_{2}(\eta_{2}(a))=\mu_{1}(\eta_{1}(x^{1}_{a}))$, so that we define $f_{2,1}(\eta_{2}(a))\triangleq\eta_{1}(x^{1}_{a})$. Thus, we have that for any $a\in A$, $\mu_{1}(\eta_{1}(a))=\mu_{2}(\eta_{2}(x^{2}_{a}))=\mu_{1}(\eta_{1}(x^{1}_{x^{2}_{a}}))$, so that, by Lemma 3.1 (1), $\eta_{1}(a)=\eta_{1}(x^{1}_{x^{2}_{a}})$. Dually, $\eta_{2}(a)=\eta_{1}(x^{2}_{x^{1}_{a}})$. Hence, it turns out that $f_{1,2}(f_{2,1}(\eta_{2}(a)))=f_{1,2}(\eta_{1}(x^{1}_{a}))=\eta_{2}(x^{2}_{x^{1}_{a}})=\eta_{2}(a)$ and $f_{2,1}(f_{1,2}(\eta_{1}(a)))=f_{2,1}(\eta_{2}(x^{2}_{a}))=\eta_{1}(x^{1}_{x^{2}_{a}})=\eta_{1}(a)$. Moreover, $\mu_{1}(\eta_{1}(a))=\mu_{2}(\eta_{2}(x^{2}_{a}))=\mu_{2}(f_{1,2}(\eta_{1}(a)))$ and $\mu_{2}(\eta_{2}(a))=\mu_{1}(\eta_{1}(x^{2}_{a}))=\mu_{1}(f_{2,1}(\eta_{2}(a)))$.

$(\Leftarrow)$ If $x\in\mu_{1}(B_{1})$ then $x\in\mu_{1}(b_{1})$, for some $b_{1}\in B_{1}$, so that, by Lemma 3.1 (2), $b_{1}=\eta_{1}(a)$ and $x\in\mu_{1}(\eta_{1}(a))$ for some $a\in A$. Thus, $x\in\mu_{1}(\eta_{1}(a))=\mu_{2}(f_{1,2}(\eta_{1}(a)))$, namely, $x\in\mu_{2}(B_{2})$. Dually, $\mu_{2}(B_{2})\subseteq\mu_{1}(B_{1})$. ∎

See 4.1

Proof.

(1) In order to have a GC, it must be that for any $X\in\wp(A)$, $Y\in\wp(B)$, $\eta^{\diamond}(X)\subseteq Y\Leftrightarrow X\subseteq\mu^{*}(Y)$. From left to right: if $a\in X$ then $\eta(a)\in Y$, so that, since $a\in\mu(\eta(a))$, we have that $a\in\mu^{*}(Y)$. From right to left: if $b\in\eta^{\diamond}(X)$ then $b=\eta(a)$ for some $a\in X$, so that, since $a\in\mu^{*}(Y)$, we have that $a\in\mu(b^{\prime})$ for some $b^{\prime}\in Y$, therefore $b=\eta(a)=b^{\prime}$, so that $b\in Y$. Let us notice that $\mu^{*}$ is clearly disjunctive: $\mu^{*}(\cup_{i}Y_{i})=\cup_{i}\mu^{*}(Y_{i})$. Finally, $\{\mu^{*}(\eta^{\diamond}(\{a\}))~{}|~{}a\in A\}=\{\mu^{*}(\{\eta(a)\})~{}|~{}a\in A\}=\{\mu(\eta(a))~{}|~{}a\in A\}$, so that, by Lemma 3.1 (3-4), and since $\cup_{a\in A}\mu(\eta(a))=A$ it turns out that $\{\mu(\eta(a))~{}|~{}a\in A\}$ is a partition of $A$.

(2) First, notice that $a^{\prime}\in\gamma(\alpha(\varnothing))\Leftrightarrow\alpha(\{a^{\prime}\})=\alpha(\varnothing)$ holds. Then, it is enough to check that $a^{\prime}\in\gamma(\alpha(\{a\})\Leftrightarrow\alpha(\{a^{\prime}\})=\alpha(\{a\})$, for any $a,a^{\prime}\in A$. On the one hand, if $a^{\prime}\in\gamma(\alpha(\{a\}))$ then, by PCG, $\gamma(\alpha(\{a^{\prime}\}))=\gamma(\alpha(\{a\}))$, so that $\alpha(\{a^{\prime}\})=\alpha(\gamma(\alpha(\{a^{\prime}\})))=\alpha(\gamma(\alpha(\{a\})))=\alpha(\{a\})$. On the other hand, if $\alpha(\{a^{\prime}\})=\alpha(\{a\})$ then, by CG, $a^{\prime}\in\gamma(\alpha(\{a^{\prime}\}))=\gamma(\alpha(\{a\}))$.

(3) If $\mathcal{C}=\langle\eta,A,B,\mu\rangle$ is a CGC then we have that $\mathcal{C}\cong_{\varnothing}\mathbb{T}_{\text{CGC}}(\mathbb{T}_{\text{PGC}}(\mathcal{C}))$ because $\mu^{*}(\{\eta^{\diamond}(\{a\})~{}|~{}a\in A\})=\{\mu^{*}(\{\eta(a)\})~{}|~{}a\in A\}=\{\mu(\eta(a))~{}|~{}a\in A\}$, so that, by Lemma 3.1 (2), $\mu^{*}(\{\eta^{\diamond}(\{a\})~{}|~{}a\in A\})\cup\{\varnothing\}=\mu(B)\cup\{\varnothing\}$. On the other hand, if $\mathcal{C}=\langle\alpha,\wp(A)_{\subseteq},D_{\leq},\gamma\rangle$ is a PGC then $\mathcal{C}\cong\mathbb{T}_{\text{PGC}}(\mathbb{T}_{\text{CGC}}(\mathcal{C}))$ because

[TABLE]

∎

See 4.3

Proof.

By definition, we have that $\mathcal{C}_{1}\sqsubseteq\mathcal{C}_{2}$ iff $\mu_{2}(B_{2})\subseteq\mu_{1}(B_{1})$, while $\mathbb{T}_{\text{PGC}}(\mathcal{C}_{1})\sqsubseteq\mathbb{T}_{\text{PGC}}(\mathcal{C}_{2})$ iff $\mu_{2}^{*}(\eta_{2}^{\diamond}(\wp(A)))\subseteq\mu_{1}^{*}(\eta_{1}^{\diamond}(\wp(A)))$. As in the proof of Theorem 4.1 (3), we have that $\mu_{i}^{*}(\eta_{i}^{\diamond}(\wp(A)))=\mu_{i}(\eta_{i}(A))$. By Lemma 3.1 (2), we have that $\mu_{i}(B_{i})=\mu_{i}(\eta_{i}(A))\cup\{\varnothing\}$. Thus, $\mu_{2}(B_{2})\subseteq\mu_{1}(B_{1})$ iff $\mu_{2}(\eta_{2}(A))\cup\{\varnothing\}\subseteq\mu_{1}(\eta_{1}(A))\cup\{\varnothing\}$ iff $\mu_{2}(\eta_{2}(A))\subseteq\mu_{1}(\eta_{1}(A))$. ∎

See 4.5

Proof.

(1) This is Lemma 3.2 (3).

(2) It turns out that $\mathbb{T}_{\text{CGP}}(\mathcal{G})$ is a CGP: (a) $\lambda a.\alpha(\downarrow\!\!\{a\}):A\rightarrow D$ is monotone: clear, because $a\leq a^{\prime}$ implies $\downarrow\!\!\{a\}\subseteq\>\downarrow\!\!\{a^{\prime}\}$, so that, by monotonicity of $\alpha$, $\alpha(\downarrow\!\!\{a\})\leq_{D}\alpha(\downarrow\!\!\{a^{\prime}\})$; (b) $\gamma:D\rightarrow{\wp^{\downarrow}}(A)$ is monotone because $\mathcal{G}$ is a GC; (c) $a\in\gamma(d)\Leftrightarrow\alpha(\downarrow\!\!\{a\})\leq_{D}d$: in fact, $a\in\gamma(d)\Leftrightarrow\>\downarrow\!a\subseteq\gamma(d)\Leftrightarrow{\alpha(\downarrow\!\!\{a\})}\leq_{D}d$.

(3) On the one hand, if $\mathcal{C}=\langle\eta,A,B,\mu\rangle$ is a CGP then we have that $\mathcal{C}=\mathbb{T}_{\text{CGP}}(\mathbb{T}_{\text{GC}}(\mathcal{C}))$ because $\mathbb{T}_{\text{CGP}}(\mathbb{T}_{\text{GC}}(\mathcal{C}))=\langle\lambda a.\eta^{\vee}(\downarrow\!\!a),A,B,\mu\rangle$ and for any $a\in A$, $\eta^{\vee}(\downarrow\!\!a)=\vee_{x\leq a}\eta(x)=\eta(a)$, because $\eta$ is monotonic. On the other hand, if $\mathcal{G}=\langle\alpha,{\wp^{\downarrow}}(A)_{\subseteq},D_{\leq},\gamma\rangle$ is a GC then

[TABLE]

so that $\mathcal{G}\cong\mathbb{T}_{\text{GC}}(\mathbb{T}_{\text{CGP}}(\mathcal{G}))$ holds. ∎

See 4.4

Proof.

(1) By (CGC-Corr), $x\in\mu(\eta(y))$ iff $\eta(x)=\eta(y)$ iff, by Lemma 3.1 (1), $\mu(\eta(x))=\mu(\eta(y))$.

(2) By definition, $x\in\varphi(a)$ iff $\varphi(x)=\varphi(a)$, and this precisely means that $\mathbb{T}_{\text{CGC}}(\varphi)$ is a CGC.

(3) If $\varphi:A\rightarrow\wp(A)$ is a CCO then $\mathbb{T}_{\text{CCO}}(\mathbb{T}_{\text{CGC}}(\varphi))=\varphi$. If $\mathcal{C}=\langle\eta,A,B,\mu\rangle$ is a CGC then $\mathcal{C}\cong_{\varnothing}\langle\mu\circ\eta,A,\{\mu(\eta(a))~{}|~{}a\in A\},\mathrm{id}\rangle=\mathbb{T}_{\text{CGC}}(\mathbb{T}_{\text{CCO}}(\mathcal{C}))$ clearly holds, by Lemma 3.1 (2). ∎

See 5.1

Proof.

By soundness in GCs, $g^{\diamond}(\gamma(\alpha(\{a\})))\subseteq\gamma(g_{\sharp}(\alpha(\gamma(\alpha(\{a\})))))$ $=\gamma(g_{\sharp}(\alpha(\{a\})))$. Also, since $a\in\gamma(\alpha(\{a\}))$, we have that $g(a)\in g^{\diamond}(\gamma(\alpha(\{a\})))$. Since $g_{\sharp}$ is block preserving, $g(a)\in g^{\diamond}(\gamma(\alpha(\{a\})))\subseteq\gamma(g_{\sharp}(\alpha(\{a\})))=\gamma(\alpha(\{a^{\prime}\}))$, for some $a^{\prime}\in A$. Hence, since $g(a)\in\gamma(\alpha(\{a^{\prime}\}))$ and $\gamma(\alpha(\{a^{\prime}\}))$ is a block, we have that $\gamma(\alpha(\{g(a)\}))=\gamma(\alpha(\{a^{\prime}\}))$, and, in turn, $\gamma(\alpha(\{g(a)\}))=\gamma(g_{\sharp}(\alpha(\{a\})))$, so that $\alpha(\gamma(\alpha(\{g(a)\})))=\alpha(\gamma(g_{\sharp}(\alpha(\{a\}))))$. By GI, $\alpha\circ\gamma=\mathrm{id}$, consequently $g_{\sharp}(\alpha(\{a\}))=\alpha(\{g(a)\})$. Also, $g^{\diamond}(\gamma(\alpha(\{a\})))\subseteq\gamma(g_{\sharp}(\alpha(\{a\})))=\gamma(\alpha(\{g(a)\}))$. ∎

See 5.2

Proof.

(1) We have that $\langle f,f_{\sharp}\rangle$ is sound iff $\forall a\in A.\>f(a)\in\mu(f_{\sharp}(\eta(a)))$. Also, we have that $\mathbb{T}_{\text{PGC}}(\langle f,f_{\sharp}\rangle)$ is sound w.r.t. $\mathbb{T}_{\text{PGC}}(\mathcal{C})$ iff $\forall X\in\wp(A).\>f^{\diamond}(X)\subseteq\mu^{*}(f_{\sharp}^{\diamond}(\eta^{\diamond}(X)))$ iff $\{f(x)~{}|~{}x\in X\}\subseteq\cup_{y\in X}\mu(f_{\sharp}(\eta(y)))$ iff $\forall X\in\wp(A).\forall x\in X.\exists y\in X.f(x)\in\mu(f_{\sharp}(\eta(y)))$. Then, $\forall a\in A.\>f(a)\in\mu(f_{\sharp}(\eta(a)))$ iff $\forall X\in\wp(A).\forall x\in X.\exists y\in X.f(x)\in\mu(f_{\sharp}(\eta(y)))$ clearly holds.

(2) $\langle g^{\diamond},g_{\sharp}\rangle$ is sound iff $\forall X\in\wp(A).\>g^{\diamond}(X)\subseteq\gamma(g_{\sharp}(\alpha(X)))$ iff $\forall X\in\wp(A).\>\{g(x)~{}|~{}x\in X\}\subseteq\gamma(g_{\sharp}(\alpha(X)))$. Moreover, $\mathbb{T}_{\text{CGC}}(\langle g^{\diamond},g_{\sharp}\rangle)=\langle g,g_{\sharp}^{r}\rangle$ is sound for $\langle{\alpha^{\scriptscriptstyle\{\!\cdot\!\}}},A,\{\alpha(\{a\})~{}|~{}a\in A\},\gamma\rangle$ iff $\forall a\in A.\>g(a)\in\gamma(g_{\sharp}^{r}({\alpha^{\scriptscriptstyle\{\!\cdot\!\}}}(a)))=\gamma(g_{\sharp}^{r}(\alpha(\{a\})))=\gamma(g_{\sharp}(\alpha(\{a\})))$, where the latter equality follows by Lemma 5.1. Then, if $\langle g^{\diamond},g_{\sharp}\rangle_{\mathcal{D}}$ is sound then $\mathbb{T}_{\text{CGC}}(\langle g^{\diamond},g_{\sharp}\rangle)$ is clearly sound. On the other hand, if $\mathbb{T}_{\text{CGC}}(\langle g^{\diamond},g_{\sharp}\rangle)$ is sound and $X\in\wp(A)$ then $\{g(x)~{}|~{}x\in X\}\subseteq\cup_{x\in X}\gamma(g_{\sharp}(\alpha(\{x\})))\subseteq\gamma(g_{\sharp}(\alpha(X)))$, where the latter containment follows by monotonicity of $\gamma$, $g_{\sharp}$ and $\alpha$.

(3) Let $\langle f,f^{\sharp}\rangle$ be a sound pair for a CGC $\mathcal{C}=\langle\eta,A,B,\mu\rangle$. By (1) we know that $\langle f^{\diamond},f_{\sharp}^{\diamond}\rangle=\mathbb{T}_{\text{PGC}}(\langle f,f_{\sharp}\rangle)$ is sound for $\mathbb{T}_{\text{PGC}}(\mathcal{C})=\langle\eta^{\diamond},\wp(A)_{\subseteq},\wp(B)_{\subseteq},\mu^{*}\rangle$. Moreover, $f_{\sharp}^{\diamond}:\wp(B)\rightarrow\wp(B)$ is monotone and block-preserving, meaning that $f_{\sharp}^{\diamond}(\eta^{\diamond}(\{a\}))=\eta^{\diamond}(\{a^{\prime}\})$ for some $a^{\prime}\in A$, because, by soundness, $f(a)\in\mu(f_{\sharp}(\eta(a)))$, so that $\eta(f(a))=f_{\sharp}(\eta(a))$, thus implying that $f_{\sharp}^{\diamond}(\eta^{\diamond}(\{a\}))=\{f_{\sharp}(\eta(a))\}=\{\eta(f(a))\}=\eta^{\diamond}(\{f(a)\})$. Let us consider $\langle f,(f_{\sharp}^{\diamond})^{r}\rangle=\mathbb{T}_{\text{CGC}}(\mathbb{T}_{\text{PGC}}(\langle f,f_{\sharp}\rangle))$, where $\mathbb{T}_{\text{CGC}}(\mathbb{T}_{\text{PGC}}(\mathcal{C}))=\langle{(\eta^{\diamond})^{\scriptscriptstyle\{\!\cdot\!\}}},A,\{\eta^{\diamond}(\{a\})~{}|~{}a\in A\},\mu^{*}\rangle$. We have that $(f_{\sharp}^{\diamond})^{r}:\{\eta^{\diamond}(\{a\})~{}|~{}a\in A\}\rightarrow\{\eta^{\diamond}(\{a\})~{}|~{}a\in A\}$ is such that $(f_{\sharp}^{\diamond})^{r}(\eta^{\diamond}(\{a\}))=\eta^{\diamond}(f(a))=f_{\sharp}^{\diamond}(\eta^{\diamond}(\{a\}))$, so we have that $\mu^{*}((f_{\sharp}^{\diamond})^{r}({(\eta^{\diamond})^{\scriptscriptstyle\{\!\cdot\!\}}}(a)))=\mu^{*}((f_{\sharp}^{\diamond})^{r}(\eta^{\diamond}(\{a\})))=\mu^{*}(f_{\sharp}^{\diamond}(\eta^{\diamond}(\{a\})))=\mu(f_{\sharp}(\eta(a)))$. Hence, this shows that $\mathbb{T}_{\text{CGC}}(\mathbb{T}_{\text{PGC}}(\langle f,f_{\sharp}\rangle))\cong\langle f,f_{\sharp}\rangle$.

On the other hand, let $\langle g^{\diamond},g^{\sharp}\rangle$ be a sound pair for a PGC $\mathcal{D}=\langle\alpha,\wp(A)_{\subseteq},D_{\leq},\gamma\rangle$, where $g:A\rightarrow A$ and $g_{\sharp}$ is monotone and block-preserving. By (2), $\langle g,g_{\sharp}^{r}\rangle=\mathbb{T}_{\text{CGC}}(\langle g^{\diamond},g_{\sharp}\rangle)$ is sound for the CGC $\mathbb{T}_{\text{CGC}}(\mathcal{D})=\langle{\alpha^{\scriptscriptstyle\{\!\cdot\!\}}},A,\{\alpha(\{a\})~{}|~{}a\in A\},\gamma\rangle$. We therefore consider $\langle g^{\diamond},(g_{\sharp}^{r})^{\diamond}\rangle=\mathbb{T}_{\text{PGC}}(\mathbb{T}_{\text{CGC}}(\langle g,g_{\sharp}\rangle))$ which, by (1), is sound for $\mathbb{T}_{\text{PGC}}(\mathbb{T}_{\text{CGC}}(\mathcal{D}))=\langle({\alpha^{\scriptscriptstyle\{\!\cdot\!\}}})^{\diamond},\wp(A)_{\subseteq},\wp(\{\alpha(\{a\})~{}|~{}a\in A\}),\gamma^{*}\rangle$. We have to check that $\gamma\circ g_{\sharp}\circ\alpha=\gamma^{*}\circ(g_{\sharp}^{r})^{\diamond}\circ({\alpha^{\scriptscriptstyle\{\!\cdot\!\}}})^{\diamond}$. For any $X\in\wp(A)$, we have that $(g_{\sharp}^{r})^{\diamond}(({\alpha^{\scriptscriptstyle\{\!\cdot\!\}}})^{\diamond}(X))=(g_{\sharp}^{r})^{\diamond}(\{\alpha(\{a\})~{}|~{}a\in X\})=\{g_{\sharp}(\alpha(\{a\}))~{}|~{}a\in X\}$, so that $\gamma^{*}((g_{\sharp}^{r})^{\diamond}(({\alpha^{\scriptscriptstyle\{\!\cdot\!\}}})^{\diamond}(X)))=\cup_{a\in X}\gamma(g_{\sharp}(\alpha(\{a\})))$. Since $g_{\sharp}$ and $\gamma$ are additive, while $\alpha$ is always additive, we have that $\cup_{a\in X}\gamma(g_{\sharp}(\alpha(\{a\})))=\gamma(g_{\sharp}(\alpha(X)))$. ∎

See 5.4

Proof.

Let us furst recall that $\mathbb{T}_{\text{PGC}}(\mathcal{C})=\langle\eta^{\diamond},\wp(A)_{\subseteq},\wp(B)_{\subseteq},\mu^{*}\rangle$.

(1) $\langle f^{\diamond},f_{\sharp}^{\diamond}\rangle$ is BCA w.r.t.  $\mathbb{T}_{\text{PGC}}(\mathcal{C})$ iff $f_{\sharp}^{\diamond}=\eta^{\diamond}\circ f^{\diamond}\circ\mu^{*}$ iff $\forall Y\in\wp(B).\{f_{\sharp}(y)~{}|~{}y\in Y\}=\eta^{\diamond}(f^{\diamond}(\cup_{y\in Y}\mu(y)))=\{\eta(f(x))~{}|~{}x\in\mu(y),y\in Y\}$ iff $\langle f,f_{\sharp}\rangle$ satisfies (CGC-Cmp/$\eta\mu$).

(2) $\langle f^{\diamond},f_{\sharp}^{\diamond}\rangle$ is forward complete w.r.t.  $\mathbb{T}_{\text{PGC}}(\mathcal{C})$ iff $f^{\diamond}\circ\mu^{*}=\mu^{*}\circ f_{\sharp}^{\diamond}$ iff $\forall Y\in\wp(B).\{f(x)~{}|~{}x\in\mu(y),y\in Y\}=\cup\{\mu(f_{\sharp}(y))~{}|~{}y\in Y\}$ iff $\langle f,f_{\sharp}\rangle$ satisfies (CGC-Cmp/$\mu\mu$).

(3) $\langle f^{\diamond},f_{\sharp}^{\diamond}\rangle$ is backward complete w.r.t.  $\mathbb{T}_{\text{PGC}}(\mathcal{C})$ iff $\eta^{\diamond}\circ f^{\diamond}=f_{\sharp}^{\diamond}\circ\eta^{\diamond}$ iff $\forall X\in\wp(A).\{\eta(f(x))~{}|~{}x\in X\}=\{f_{\sharp}(\eta(x))~{}|~{}x\in X\}$ iff $\langle f,f_{\sharp}\rangle$ satisfies (CGC-Cmp/$\eta\eta$).

(4) $\langle f^{\diamond},f_{\sharp}^{\diamond}\rangle$ is precise w.r.t. $\mathbb{T}_{\text{PGC}}(\mathcal{C})$ iff $f^{\diamond}=\mu^{*}\circ f_{\sharp}^{\diamond}\circ\eta^{\diamond}$ iff $\forall X\in\wp(A).\{f(x)~{}|~{}x\in X\}=\cup\{\mu(f_{\sharp}(\eta(x)))~{}|~{}x\in X\}$ iff $\langle f,f_{\sharp}\rangle$ satisfies (CGC-Cmp/$\mu\eta$). ∎

See 6.1

Proof.

(1) $a\in\mu(\wedge_{i}b_{i})$ iff, by PCGC (2), $\eta(a)\leq\wedge_{i}b_{i}$ iff $\forall i.\,\eta(a)\leq b_{i}$ iff, by PCGC (2), $\forall i.\,a\in\mu(b_{i})$ iff $a\in\cap_{i}\mu(b_{i})$.

(2) The proof of $\eta(a_{1})=\eta(a_{2})\>\Leftrightarrow\>\mu(\eta(a_{1}))=\mu(\eta(a_{2}))$, by PCGC (1), is the same of Lemma 3.2 (1). Also, $\mu(\eta(a_{1}))=\mu(\eta(a_{2}))\>\Rightarrow\>a_{1},a_{2}\in\mu(\eta(a_{1}))\cap\mu(\eta(a_{2}))$. Conversely, if $a\in\mu(\eta(a_{1}))\cap\mu(\eta(a_{2}))$ then, by PCGC (1), $\eta(a_{1})=\eta(a)=\eta(a_{2})$.

(3) If $b\in\eta(A)$ then $b=\eta(a)$, for some $a$, so that $a\in\mu(\eta(a))$. A counterexample to the vice versa is in Example 6.2.

(4) $\vee_{a\in X}\eta(a)\leq b\>\Leftrightarrow\>\forall a\in X.\eta(a)\leq b\>\Leftrightarrow\>\forall a\in X.a\in\mu(b)\>\Leftrightarrow\>X\subseteq\mu(b)$. ∎

See 6.3

Proof.

(1) By Lemma 6.1 (3), $\mathbb{T}_{\text{PPGC}}(\mathcal{C})=\langle\eta^{\vee},\wp(A)_{\subseteq},B_{\leq},\mu\rangle$ is a GC. If $a\in\mu(\eta^{\vee}(\{a_{1}\})\cap\mu(\eta^{\vee}(\{a_{2}\}))$ then, by PCGC (1), $\eta(a_{1})=\eta(a)=\eta(a_{2})$, so that $\mu(\eta^{\vee}(\{a_{1}\}))=\mu(\eta^{\vee}(\{a_{2}\}))$, implying that $\mathbb{T}_{\text{PPGC}}(\mathcal{C})$ is indeed a PPGC.

(2) Let us show PCGC (1):

[TABLE]

On the other hand, ${\alpha^{\scriptscriptstyle\{\!\cdot\!\}}}(a)={\alpha^{\scriptscriptstyle\{\!\cdot\!\}}}(a^{\prime})$ means $\alpha(\{a\})=\alpha(\{a^{\prime}\})$, so that, by GC, $a\in\gamma(\alpha(\{a\}))=\gamma(\alpha(\{a^{\prime}\}))=\gamma({\alpha^{\scriptscriptstyle\{\!\cdot\!\}}}(a^{\prime}))$. PCGC (2) also follows because $a\in\gamma(d)$ iff $\{a\}\subseteq\gamma(d)$ iff, by GC, $\alpha(\{a\})\leq d$ iff ${\alpha^{\scriptscriptstyle\{\!\cdot\!\}}}(a)\leq d$.

(3) Let $\mathcal{C}=\langle\eta,A,B_{\leq},\mu\rangle$ be a PCGC. We have that $\mathbb{T}_{\text{PCGC}}(\mathbb{T}_{\text{PPGC}}(\mathcal{C}))=\langle{(\eta^{\vee})^{\scriptscriptstyle\{\!\cdot\!\}}},A,B_{\leq},\mu\rangle$, so that $\mathbb{T}_{\text{PCGC}}(\mathbb{T}_{\text{PPGC}}(\mathcal{C}))=\mathcal{C}$ holds because ${(\eta^{\vee})^{\scriptscriptstyle\{\!\cdot\!\}}}=\eta$. On the other hand, let $\mathcal{D}=\langle\alpha,\wp(A)_{\subseteq},D_{\leq},\gamma\rangle$ be a PPGC. Here, $\mathbb{T}_{\text{PPGC}}(\mathbb{T}_{\text{PCGC}}(\mathcal{D}))=\langle({\alpha^{\scriptscriptstyle\{\!\cdot\!\}}})^{\vee},\wp(A)_{\subseteq},D_{\leq},\gamma\rangle$. We have that

[TABLE]

so that $\mathbb{T}_{\text{PPGC}}(\mathbb{T}_{\text{PCGC}}(\mathcal{D}))\cong\mathcal{D}$. ∎

See 6.5

Proof.

(1) We have that $\langle f,f_{\sharp}\rangle$ is sound w.r.t. $\mathcal{C}$ iff $\eta^{\vee}\circ f^{\diamond}\circ\mu\sqsubseteq f_{\sharp}$ iff $\langle f^{\diamond},f_{\sharp}\rangle$ is sound w.r.t. $\mathbb{T}_{\text{PPGC}}(\mathcal{C})=\langle\eta^{\vee},\wp(A)_{\subseteq},B_{\leq},\mu\rangle$.

(2) $\langle g^{\diamond},g_{\sharp}\rangle$ is sound w.r.t. $\mathcal{D}$ iff $\alpha\circ g^{\diamond}\circ\gamma\sqsubseteq g_{\sharp}$, while $\langle g,g_{\sharp}\rangle=\mathbb{T}_{\text{PCGC}}(\langle g^{\diamond},g_{\sharp}\rangle)$ is sound w.r.t. $\mathbb{T}_{\text{PCGC}}(\mathcal{D})=\langle{\alpha^{\scriptscriptstyle\{\!\cdot\!\}}},A,D_{\leq},\gamma\rangle$ iff $g^{\diamond}_{\mathbb{T}_{\text{PCGC}}(\mathcal{D})}\sqsubseteq g_{\sharp}$ iff $({\alpha^{\scriptscriptstyle\{\!\cdot\!\}}})^{\vee}\circ g^{\diamond}\circ\gamma\sqsubseteq g_{\sharp}$. Then, it is enough to observe that $({\alpha^{\scriptscriptstyle\{\!\cdot\!\}}})^{\vee}=\alpha$: in fact, for any $X\in\wp(A)$, $({\alpha^{\scriptscriptstyle\{\!\cdot\!\}}})^{\vee}(X)=\vee_{x\in X}{\alpha^{\scriptscriptstyle\{\!\cdot\!\}}}(x)=\vee_{x\in X}\alpha(\{x\})=\alpha(\cup_{x\in X}\{x\})=\alpha(X)$.

(3) Clear. ∎