<figure><img src="image_1.png" /></figure>

HAL
open science

# Relating Distances and Abstractions: An Abstract Interpretation Perspective

Marco Campion, Isabella Mastroeni, Caterina Urban

► To cite this version:

Marco Campion, Isabella Mastroeni, Caterina Urban. Relating Distances and Abstractions: An Abstract Interpretation Perspective. SAS 2025 - 32nd Static Analysis Symposium, Oct 2025, Singapore, Singapore. hal-05207631

HAL Id: hal-05207631

https://inria.hal.science/hal-05207631v1

Submitted on 12 Aug 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Relating Distances and Abstractions
## An Abstract Interpretation Perspective

Marco Campion¹[0000-0002-1099-3494], Isabella Mastroeni²[0000-0003-1213-536X], and Caterina Urban¹[0000-0002-8127-9642]

¹ Inria & ENS | PSL, Paris, France
{marco.campion,caterina.urban}@inria.fr

² University of Verona, Department of Computer Science, Verona, Italy
isabella.mastroeni@univr.it

**Abstract.** We establish a formal relation between quantitative and semantic approximations—formalized by pre-metrics and upper closure operators (ucos), respectively—by means of Galois connections. This connection reveals that it is far from trivial for a pre-metric to uniquely identify a uco, highlighting the structural constraints and, more generally, the distinct identity inherent to semantic approximations. Building on this foundation, we introduce a general composition of semantic and quantitative approximations. This allows us to define a new confidentiality property, called Partial Abstract Non-Interference, that measures bounded variations in program behavior over abstract properties of data. We then relate this property to Partial Completeness in abstract interpretation, revealing a deeper connection between static analysis precision and security guarantees.

**Keywords:** Distances · Abstractions · Abstract Interpretation · Partial Abstract Non-Interference · Partial Completeness

# 1 Introduction

Understanding the behavior of programs is a fundamental challenge in computer science. Due to inherent undecidability, some degree of approximation is unavoidable, both in how we observe program behavior and in how we formalize the properties we aim to analyze. Broadly speaking, we can distinguish between two main paradigms of approximation: semantic and quantitative. *Semantic approximations* capture qualitative properties of data and computations, often abstracting over irrelevant details to retain logical or behavioral correctness. *Quantitative approximations*, on the other hand, measure similarity or closeness between elements using metrics or more relaxed forms of distances.

These two perspectives can be pursued *independently*, or *combined* for a unified approach to approximation. Semantic approximations are at the heart of abstract interpretation [14,16], a foundational framework for soundly approximating program behavior through *abstractions*. They are also intrinsic to properties such as Abstract Non-Interference [24], a relaxation of classic Non-Interference [27] that captures variations in the semantic properties that may
influence program computations. In contrast, quantitative approximations underpin distance-based properties, useful when reasoning about approximations in a meaningful distance space. Notable examples include Approximate Non-Interference [18], which permits some exactly quantified leakage of information, as well as Program Continuity and Robustness [9,11,10], which ensure that arbitrarily small changes to inputs only cause arbitrarily small changes to program outputs, and Differential Privacy [20], which formalizes privacy loss as a bounded statistical difference in output distributions. In some cases, semantic and quantitative perspectives are combined to define a more general approximation approach. For instance, Partial Completeness in abstract interpretation [5] leverages pre-metrics compatible with the underlying domain structure to quantify precision loss in program analysis [8]. Similarly, Abstract Robustness [25], characterizes the robustness of deep neural networks against adversarial attacks by combining a distance over inputs with an abstraction of the outputs.

In general, semantic and quantitative approaches offer distinct perspectives on the problem of approximation, each relying on different formal frameworks to capture its nuances. In this work, we aim to explore whether and how these two methodologies relate:

*Are they fundamentally distinct tools for approximations, or can one be systematically derived from the other?*

*Can we formalize a way to combine their respective advantages into a unifying approximation framework?*

**Our Contribution.** We explore a formal correspondence between semantic approximations, modeled here as *upper closure operators* (ucos), and quantitative approximations, modeled here as *pre-metrics*. We show how semantic approximations can be derived from distance functions (and vice versa), through a process of abstractions using Galois connections. On the one hand, this connection confirms that ucos can be viewed as particular instances of pre-metrics—specifically, those that assign a distance of zero to elements sharing the same abstraction. On the other hand, however, it is far from trivial for a pre-metric to uniquely identify a uco, highlighting the structural constraints and, more generally, the distinct identity inherent to semantic approximations.

Building on this foundation, we formalize a *composition* operator of pre-metrics that first selects the domain of comparison and then measures distances within this selected domain, thereby enabling a form of layered abstraction. Such a composition, when involving a distance characterizing a semantic abstraction and a distance characterizing a quantitative abstraction, defines a new form of approximation, called *general approximation*, combining semantic and quantitative approaches while keeping the two types of approximations distinct.

This approach allows us to define a new confidentiality property, called *Partial Abstract Non-Interference*, that generalizes both Abstract Non-Interference and Approximate Non-Interference in a unifying view by combining both semantic and quantitative approximations. Partial Abstract Non-Interference allows bounded variations in the abstract program behavior over inputs sharing
a similar abstract property. We then relate this property to Partial Completeness in abstract interpretation, revealing a deeper connection between bounded (im)precision in abstract interpretation and security guarantees.

**Structure of the paper.** In Sec. 2 we formalize semantic approximations via upper closure operators, and quantitative approximations by pre-metrics, recalling their respective definitions from the literature. Sec. 3 establishes a formal relation between the two forms of approximations. This consists in an abstraction process—formalized by a series of Galois connections—from the domain of pre-metrics to the domain of ucos by passing through equivalence relations. Sec. 4 formally defines a possible way to combine pre-metrics, characterizing quantitative approximations, with distances characterizing semantic abstractions. This will form a general approximation framework which will be used in Sec. 6 to define a new confidentiality property based on the notion of Abstract Non-Interference, called Partial Abstract Non-Interference that quantifies semantic variations in the output domain. This newly defined property is then compared with the Partial Completeness property to establish a relation between them. A background on the Partial Completeness notion in abstract interpretation, and the Abstract Non-Interference property, is provided in Sec. 5.

# 2 Abstractions and Distances

In many domains, approximations are a fundamental tool for simplifying reasoning while retaining essential properties. Broadly speaking, we can distinguish between semantic (or qualitative) approximations, and quantitative approximations. Here we formalize semantic approximations via upper closure operators and quantitative approximations by means of pre-metrics.

## 2.1 Semantic Approximations via Upper Closure Operators

Qualitative or semantic approximations preserve certain semantic properties of the approximated data. Semantic approximations are at the heart of abstract interpretation [14,16], which offers a general methodology for approximating computations by evaluating functions (e.g., program semantics) over an abstract domain A instead of the concrete domain C. This approach is especially valuable when exact analysis is computationally infeasible or undecidable, trading precision for decidability. In this setting, A is referred to as an abstraction of C whenever there is a Galois Connection (GC), or a Galois Insertion (GI), between the two domains. More formally, given a partially ordered set (poset, for short) $\langle C, \le_C \rangle$, called the concrete domain, and a poset $\langle A, \le_A \rangle$, called the abstract domain, a GC is denoted by $\langle C, \le_C \rangle \overset{\gamma}{\underset{\alpha}{\rightleftarrows}} \langle A, \le_A \rangle$ where $\alpha: C \to A$ is the (monotone) abstraction function, sometimes referred to as the lower adjoint, and $\gamma: A \to C$ is the (monotone) concretization function, also referred to as the upper adjoint, both satisfying the following condition $\forall a \in A \text{ and } \forall c \in C$:

$$ \alpha(c) \le_A a \Leftrightarrow c \le_C \gamma(a) $$
A GC is a GI, denoted by $\langle C, \le_c \rangle \stackrel{\gamma}{\underset{\alpha}{\rightleftarrows}} \langle A, \le_\lambda \rangle$, when $\alpha \circ \gamma = \iota$, namely when their composition is the identity function ($\iota \stackrel{\text{def}}{=} \lambda x. x$). An essential property of a GC is that an upper/lower adjoint of a GC uniquely determines the other: $\alpha(c)$ is the least element $a$ with $c \le_c \gamma(a)$, and $\gamma(a)$ is the largest element $c$ with $\alpha(c) \le_\lambda a$. In particular, when both $\langle C, \le_c \rangle$ and $\langle A, \le_\lambda \rangle$ are complete lattices, respectively $\langle C, \le_c, \vee_c, \wedge_c, \top_c, \bot_c \rangle$ and $\langle A, \le_\lambda, \vee_\lambda, \wedge_\lambda, \top_\lambda, \bot_\lambda \rangle$, then $\alpha(c) = \wedge_\lambda \{a \in A \mid c \le_c \gamma(a)\}$ and $\gamma(a) = \vee_c \{c \in C \mid \alpha(c) \le_\lambda a\}$. It turns out that $\alpha$ is a complete join-morphism (sometimes also referred to as an additive function), namely for all $S \subseteq C: \alpha(\vee_c S) = \vee_\lambda \{\alpha(c) \mid c \in S\}$, dually $\gamma$ is a complete meet-morphism (co-additive function), namely for all $S \in A: \gamma(\wedge_\lambda S) = \wedge_\lambda \{\gamma(a) \mid a \in S\}$.

Galois connections/insertions can be equivalently formulated in terms of upper closure operators [16] (ucos or closures, for short).

**Definition 1 (Upper Closure Operator).** An upper closure operator on a poset $\langle C, \le_c \rangle$ is a function $\rho: C \to C$ with the following properties $\forall c, c' \in C$:

$$ (i) \quad c \le_c c' \Rightarrow \rho(c) \le_c \rho(c'); \qquad (\text{monotonicity}) $$

$$ (ii) \quad c \le_c \rho(c); \qquad (\text{extensivity}) $$

$$ (iii) \quad \rho(\rho(c)) = \rho(c). \qquad (\text{idempotence}) $$

Ucos are uniquely determined by the set of their fixpoints: $\rho(C) = \{c \in C \mid \rho(c) = c\}$. For instance, the composition $\gamma \circ \alpha$ is a uco of $C$. In the following, the set of all upper closure operators on a poset $C$ is denoted by $\text{Uco}(C)$.

**Example 1 (Sign and Parity Abstractions).** The closure $\text{Sign} \in \text{Uco}(\wp(\mathbb{Z}))$ abstracts a set of integers by discarding all information except the sign of its values. It corresponds to the identity function when applied to the empty set or in case the set contains the value zero only. The closure is defined by the set of fixpoints:

$$ \text{Sign}(\wp(\mathbb{Z})) \stackrel{\text{def}}{=} \{\emptyset, \{0\}, \{z \in \mathbb{Z} \mid z \le 0\}, \{z \in \mathbb{Z} \mid z \ge 0\}, \mathbb{Z}\} $$

Similarly, we can define the parity abstraction closure $\text{Par} \in \text{Uco}(\wp(\mathbb{Z}))$ as:

$$ \text{Par} \stackrel{\text{def}}{=} \{\emptyset, \text{Even} \stackrel{\text{def}}{=} \{n \in \mathbb{Z} \mid n \bmod 2 = 0\}, \text{Odd} \stackrel{\text{def}}{=} \{n \in \mathbb{Z} \mid n \bmod 2 = 1\}, \mathbb{Z}\} \triangleleft $$

Whenever $C$ is a complete lattice, then also $\text{Uco}(C)$, ordered point-wise, is a complete lattice denoted by $\langle \text{Uco}(C), \sqsubseteq, \sqcup, \sqcap, \lambda x. x, \lambda x. \top \rangle$. Here, for every $\rho, \eta \in \text{Uco}(C)$, $\{\rho_i\}_{i \in I} \subseteq \text{Uco}(C)$ where $I$ is an index set of ucos, and $x \in C: \rho \sqsubseteq \eta$ iff $\forall c \in C. \rho(c) \le_c \eta(c)$ iff $\eta(C) \subseteq \rho(C)$; $(\sqcap_{i \in I} \rho_i)(c) = \wedge_{i \in I} \rho_i(c)$; and $(\sqcup_{i \in I} \rho_i)(c) = c \Leftrightarrow \forall i \in I. \rho_i(c) = c$. Then, $\text{Uco}(C)$ is the so-called lattice of abstractions of $C$ [16], i.e., the complete lattice of all possible abstractions (up to isomorphic representation of their objects) of the concrete domain $C$.

Henceforth, we formally model semantic approximation through ucos:

**Definition 2 (Semantic Approximation).** Given a poset $\langle C, \le_c \rangle$ and the abstraction $\rho \in \text{Uco}(C)$, an element $x \in C$ is semantically approximated by $\rho(x)$, and the set $\{y \in C \mid \rho(y) = \rho(x)\}$ represents all elements in $C$ sharing the same semantic approximation as $x$.
<figure><img src="image_3.png" /><figcaption>Fig. 1: Metrics and their relaxed forms.</figcaption></figure>

**Example 2.** Let $\text{Int}: \wp(\mathbb{Z}) \to \wp(\mathbb{Z})$ map a set of integers $S \in \wp(\mathbb{Z})$ to the smallest interval $[l, u] \stackrel{\text{def}}{=} \{i \in \mathbb{Z} \mid l \le i \le u\}$ that contains it, namely such that $S \subseteq [l, u]$, where $l \in \mathbb{Z} \cup \{-\infty\}$, $u \in \mathbb{Z} \cup \{+\infty\}$ and $l \le u$. This is the well known interval abstraction $\text{Int} \in \text{Uco}(\wp(\mathbb{Z}))$ [13]. So, for instance, the set of integers $\{0, 1, 4\}$ can be semantically approximated by the interval $[0, 4]$ through $\text{Int}$. Moreover, the set $\{{\color{red}0}, 4\}, \{0, 1, 4\}, \{0, 2, 4\}, \{0, 3, 4\}, \{0, 1, 2, 4\}, \{0, 1, 3, 4\}, \{0, 1, 2, 3, 4\}}$ contains all sets of integers $S$ such that $\text{Int}(S) = [0, 4]$. $\triangleleft$

## 2.2 Quantitative Approximations via Pre-Metrics

Quantitative approximations preserve *closeness* of the approximated data, typically measured through a distance function in a suitable topological space. Here, we model distance functions using (pre-)metrics.

Let $\mathbb{R}^{\infty}$ be the set of real numbers extended with the infinite symbol $\infty$, such that for all $r \in \mathbb{R}$, $r < \infty$. Let $\mathbb{R}_{\ge n}$ be the restriction of $\mathbb{R}$ to values greater or equal than $n \in \mathbb{N}$. For instance, $\mathbb{R}_{\ge 0}^{\text{def}} = \{r \in \mathbb{R} \mid r \ge 0\} \cup \{\infty\}$.

**Definition 3 (Metric).** Given a non-empty set $L$, a metric is a binary function $\delta: L \times L \to \mathbb{R}^{\infty}$ with the following properties $\forall x, y, z \in L$:

(1) $\delta(x, y) \ge 0$; \qquad (non-negativity)

(2) $x = y \Leftrightarrow \delta(x, y) = 0$; \qquad (iff-identity)

(3) $\delta(x, y) = \delta(y, x)$; \qquad (symmetry)

(4) $\delta(x, y) \le \delta(x, z) + \delta(z, y)$. \qquad (triangle-inequality)

The pair $(L, \delta)$ is called a *metric space*.

A classic metric example is the Euclidean distance measuring the distance between two real values as the absolute value of their difference.

Due to their axioms, metrics are among the strongest types of distances. However, depending on what we want to measure and on which domain, a distance function may not satisfy all axioms of a metric, but only, e.g., (non-negativity) and (iff-identity), thereby being a pre-metric instead (cf. Fig. 1). As we will see in Sec. 6, understanding the type of distance function we are manipulating is essential for proving some implications between properties of programs (such as between Partial Completeness and Partial Abstract Non-Interference in Sec. 6).
In particular, a metric that does not satisfy symmetry is called a quasi-metric, while a metric that does not satisfy the $\leftarrow$ implication of (iff-identity) is called a pseudo-metric. Semi-metrics satisfy all the axioms except for the triangle inequality. The function $\delta$ is called a pre-metric [17,8] if it only satisfies (non-negativity) and the $\Rightarrow$ implication of the (iff-identity), i.e., the (if-identity) axiom. All the other metric axioms are not required, making the definition of pre-metric one of the weakest possible distance function. By composing the words pseudo-, quasi- and semi- we obtain different distance flavors by simply keeping the axioms that are satisfied by all the combined words. For instance, a quasisemi-metric is a pre-metric that additionally satisfies the (iff-identity). Fig. 1 summarizes the above distance notions and their properties. We will occasionally use the subscript $\delta_L$ in cases where the set $L$ may not be immediately clear from the context. From this point forward, whenever we say that a function $\delta$ is a distance, we assume that it satisfies, at least, the axioms of a pre-metric.

**Example 3 (Size Distance).** Consider the powerset $\wp(L)$ of a set $L$. We write $\text{Count}(S)$ for the number of elements in the set $S \in \wp(L)$. We define the distance $\delta_{\text{siz}}: \wp(L) \times \wp(L) \to \mathbb{R}^{\infty}$ between two sets $S_1, S_2 \in \wp(L)$ as the absolute value of the difference in their size, i.e., $\delta_{\text{siz}}(S_1, S_2) \stackrel{\text{def}}{=} |\text{Count}(S_2) - \text{Count}(S_1)|$. Note that $\delta_{\text{siz}}$ is not a metric, but a pseudo-metric since it does not satisfy the (iff-identity) axiom: two sets may have the same size yet being different.

In program analysis, $\delta_{\text{siz}}$ could be used to count, for instance, the number of spurious elements added by an abstract sound computation with respect to the abstraction of a concrete computation. For instance, if $[0, 0]$ is the (interval abstraction of the) strongest numerical invariant of a program variable $x$ at certain program point, while $[0, 10]$ is the abstract invariant generated by an abstract interpretation over $\text{Int}$, then $\delta_{\text{siz}}^{\text{Int}}([0, 0], [0, 10]) = 10$ indicates that the abstract interpretation added 10 spurious values with respect to the (interval abstraction of the) concrete execution. A similar example can be considered when counting the false positives generated by a static analysis while checking an abstract specification (e.g, whether $x \in [0, 0]$). $\triangleleft$

**Example 4 (Volume Distance).** Let us consider the ordered domain of convex octagons ($\text{Oct}, \le_{\text{oct}}$) [39]. We define the distance

$$ \delta_{\text{Vol}}(o_1, o_2) \stackrel{\text{def}}{=} \text{Av}(\text{Vol}(o_1) - \text{Vol}(o_2)) $$

calculating the absolute value of the difference between the volume of two convex octagons $o_1, o_2 \in \text{Oct}$. The volume function $\text{Vol}: \text{Oct} \to \mathbb{R}_{\ge 0}^{\infty}$ could be a monotone (namely, if $\gamma(o_1) \subseteq \gamma(o_2)$ then $\text{Vol}(o_1) \le \text{Vol}(o_2)$) overapproximation of the exact volume computation. $\delta_{\text{Vol}}$ satisfies all the axioms of a metric except for (iff-identity) since two octagons may have the same volume yet not representing the same octagon. Thus, $\delta_{\text{Vol}}$ qualifies as a pseudo-metric. In program analysis, $\delta_{\text{Vol}}$ could be used to quantify the difference between the (numerical) invariants of program variables generated by the abstraction of a concrete computation with respect to an abstract computation. $\triangleleft$
For additional examples of pre-metrics and their applications in domains used
within the context of program analysis, we refer to [8].

We formally define quantitative approximations via pre-metrics as follows:

**Definition 4 (Quantitative Approximation).** *Given a pre-metric space $(\mathcal{C}, \delta)$ and a fixed constant $\varepsilon \in \mathbb{R}_{\ge 0}^{\infty}$, an element $x \in \mathcal{C}$ is quantitatively approximated by any element in the set $\{y \in \mathcal{C} \mid \delta(x, y) \le \varepsilon\}$.*

*Example 5.* Continuing Ex. 2, we may approximate sets of integer numbers by the size distance $\delta_{siz}$ defined in Ex. 3. For instance, $\{0, 1, 4\}$ can be quantitatively approximated by any set of integers whose maximum distance from it is at most $\varepsilon = 1$. Examples of such approximations include sets $\{0, 1\}$ and $\{5, 6, 8, 10\}$. $\triangleleft$

Here, the admitted noise concerns elements that are topologically close to
the original one but that may share no semantic property.

3 From Pre-Metrics to Upper Closure Operators

Semantic and quantitative approaches offer distinct perspectives on the problem of approximation, relying on different formal frameworks to capture its nuances. This naturally raises the question: are these two perspectives entirely orthogonal, or is there a deeper relation between them? Understanding this connection is the main goal of this section. Specifically, in the following, we establish a formal relation between quantitative and semantic approximations—formalized by pre-metrics and ucos, respectively—by means of Galois connections.

Let us start by assuming to work with a complete lattice $\langle \mathcal{C}, \le_c, \vee_c, \wedge_c, \top_c, \bot_c \rangle$. Pre-metrics provide a quantitative measure of the difference between elements in $\mathcal{C}$. Such distances cannot be derived from the order structure alone, they must be explicitly defined. As a result, the only viable approach to relate pre-metrics and ucos is to derive the latter as abstractions of the former. The abstraction process moves from pre-metrics to ucos by passing through equivalence relations:

Pre-Metrics —> Equivalence Relations —> Uco

More in detail, we first identify a subset of pre-metrics (called 0-pseudo-metrics) on which we can obtain equivalence relations as an abstraction. The underlying intuition is that we can represent a semantic approximation $\rho \in Uco(\mathcal{C})$ by means of a pre-metric $\delta$ that assigns distance 0 to elements $x, y \in \mathcal{C}$ with the same abstraction $\rho(x) = \rho(y)$, and assigns distance $\infty$ otherwise. Elements assigned with a distance of zero are the equivalence classes of the equivalence relation induced by the 0-pseudo-metrics. On the other hand, ucos satisfy structural properties—monotonicity, extensivity, idempotence—that are not automatically satisfied by pre-metrics, 0-pseudo-metrics, or equivalence relations. These properties have to be enforced through suitable constraints imposed by the abstractions. We derive ucos in two further steps: forcing extensivity first, and monotonicity and idempotence afterward, leveraging [15].
## 3.1 The Domain $M(C)$ of Pre-Metrics

The first step in formalizing the abstraction process from pre-metrics to ucos is to define the underlying domain on which the construction operates. In the following, we introduce the domain of pre-metrics. In the next subsections, we progressively derive the domain of ucos as an abstraction.

Let $M(C)$ be the set of all pre-metrics $\delta: C \times C \to \mathbb{R}^{\infty}$ defined on $C$, i.e, $M(C) \stackrel{\text{def}}{=} \{\delta | \delta \text{ is a pre-metric on } C\}$. We equip $M(C)$ with a partial order $\sqsubseteq_m$ that compares pre-metrics based on the cardinality of sets of pairs of elements with a distance of zero. Formally, for $\delta_1, \delta_2 \in M(C)$, we define:

$$ \delta_1 \sqsubseteq_m \delta_2 \stackrel{\text{def}}{\Leftrightarrow} \forall x, y \in C. \delta_2(x, y) = 0 \lor (\delta_1(x, y) \neq 0 \land \delta_1(x, y) \leq \delta_2(x, y)) $$

Intuitively, moving upward in the ordering corresponds to enlarging the sets of pairs of elements that are assigned a distance of zero: pairs of elements that are distinguished (assigned a non-zero distance) by a more concrete pre-metric $\delta_1$ may become indistinguishable (assigned a zero distance) by a more abstract pre-metric $\delta_2$. The distance between elements that remain distinguishable in $\delta_2$ may stretch, possibly to $\infty$, reflecting the underlying intuition mentioned above.

**Example 6.** Suppose $C = \wp(\{1, 2, 3, 4\})^3$. Let $\delta$ and $\delta'$ be pre-metrics on $C$ such that $\delta(1, 3) = \delta(13, 12) = \delta(2, 12) = \delta(34, 234) = 0$, $\delta(12, 14) = 2$, $\delta(12, 34) = 2$ while all the other elements are at distance $\infty$, and $\delta' = \delta$ except for $\delta'(1, 23) = 0$ ($\delta(1, 23) = \infty$) and $\delta'(12, 34) = 3 > 2 = \delta(12, 34)$, graphically:

$$ \delta: \begin{array}{r@{\;}c@{\;}l@{\quad}l@{\quad}l} 1 & \xrightarrow{0} & 3 & 13 & \xrightarrow{0} & 12 & \xrightarrow{2} & 34 & \xrightarrow{0} & 234 \\ & & \searrow & & \searrow & & \searrow & & \searrow & \\ & & \multicolumn{6}{c}{\text{2}} & \multicolumn{2}{c}{14} \end{array} $$

$$ \delta': \begin{array}{r@{\;}c@{\;}l@{\quad}l@{\quad}l} 1 & \xrightarrow{0} & 3 & 13 & \xrightarrow{0} & 12 & \xrightarrow{3} & 34 & \xrightarrow{0} & 234 \\ & & \searrow & & \searrow & & \searrow & & \searrow & \\ & & \multicolumn{6}{c}{\text{23}} & \multicolumn{2}{c}{14} \end{array} $$

(The distances not depicted above are $\infty$. The differences are colored in red.) We clearly have $\delta \sqsubseteq_m \delta'$. $\triangleleft$

Let $N \subseteq \mathbb{N}$ and $x, y \in C$. We define the join and meet operators, $\sqcup_m$ and $\sqcap_m$, over sets of pre-metrics $\{\delta_i(x, y) \in M(C) | i \in N\}$ as follows:

$$ \begin{array}{l} \sqcup_m \{\delta_i\}_{i \in N} \stackrel{\text{def}}{=} \lambda(x, y). \quad \left\{ \begin{array}{ll} \max\{\delta_i(x, y) | i \in N\} & \forall i \in N: \delta_i(x, y) \neq 0 \\ 0 & \text{otherwise} \end{array} \right. \\ \\ \sqcap_m \{\delta_i\}_{i \in N} \stackrel{\text{def}}{=} \lambda(x, y). \quad \left\{ \begin{array}{ll} m & m = \min\{\delta_i(x, y) | i \in N\} \neq \perp \\ \text{undefined} & \text{otherwise} \end{array} \right. \end{array} $$

<footnote n="3">³ For the sake of readability, in the following, we represent sets of numbers by the sequences of their elements without separators, e.g., $\{1, 2\}$ is represented by 12.</footnote>
where the max and min operators:

$$
\begin{align*}
\max \{\delta_i(x, y) \mid i \in N\} &\stackrel{\text{def}}{=} \begin{cases}
d & \exists m \in N: \forall i \in N: \infty \neq d = \delta_m(x, y) \ge \delta_i(x, y) \\
\infty & \text{otherwise}
\end{cases} \\
\min \{\delta_i(x, y) \mid i \in N\} &\stackrel{\text{def}}{=} \begin{cases}
0 & \forall i \in N: \delta_i(x, y) = 0 \\
d & \exists m \in N: \forall i \in N: 0 < d = \delta_m(x, y) \le \delta_i(x, y) \\
\perp & \text{otherwise}
\end{cases}
\end{align*}
$$

find the distances within the given set of pre-metrics that are largest (but dif-
ferent from $\infty$) and smallest (possibly equal to $\infty$), respectively. It is clear that
the bottom element of $M(\mathcal{C})$ does not exist in general. It is $\delta_{\perp}$ such that $\forall x, y \in
\mathcal{C}: \delta_{\perp}(x, y) \stackrel{\text{def}}{=} 1$, if pre-metrics are restricted to assign discrete distances over nat-
ural numbers. The top element of $M(\mathcal{C})$ is $\delta_{\top}$ such that $\forall x, y \in \mathcal{C}: \delta_{\top}(x, y) \stackrel{\text{def}}{=} 0$.

**Proposition 1.** $\langle \mathcal{M}(\mathcal{C}), \sqsubseteq_m, \sqcup_m, \sqcap_m, \delta_\top \rangle$ is a join-complete semi-lattice.

3.2 The Domain $M_0(\mathcal{C})$ of 0-Pseudo-Metrics

<figure><img src="image_4.png" /></figure>

We observe that not all pre-metrics in M(C) are meaningful representations of se-
mantic approximations. For instance, the pre-metric in Ex. 6 is not a meaningful
semantic approximation because it is neither symmetric nor transitive between
elements at distance zero, e.g., δ identifies a semantic equivalence between 1 and
3 (δ(1, 3) = 0) but not between 3 and 1 (δ(3, 1) = ∞).

The domain $M_0(\mathcal{C})$. We define a restriction of pre-metrics—called 0-pseudo-metrics—satisfying symmetry and transitivity between elements that are assigned a distance of zero.

**Definition 5 (0-Pseudo-Metrics).** A 0-pseudo-metric $\delta: \mathcal{C} \times \mathcal{C} \to \mathbb{R}^{\infty}$ is a pre-metric that additionally satisfies the following conditions, for all $x, y, z \in \mathcal{C}$:

$$
1. \delta(x, y) = 0 \Rightarrow \delta(y, x) = 0; \qquad (0\text{-distance symmetry})
$$

$$
2. (\delta(x, y) = 0 \land \delta(y, z) = 0) \Rightarrow \delta(x, z) = 0 \quad (0\text{-distance transitivity})
$$

Let $M_0(\mathcal{C})$ be the set of all 0-pseudo-metrics defined on $\mathcal{C}$. It is clear that, by definition, $M_0(\mathcal{C}) \subset \mathcal{M}(\mathcal{C})$, hence $\langle M_0(\mathcal{C}), \sqsubseteq_m \rangle$, i.e., the domain of 0-pseudo-metrics, is still a poset preserving the same characteristics as $\mathcal{M}(\mathcal{C})$.

**Proposition 2.** $\langle \mathcal{M}_0(\mathcal{C}), \sqsubseteq_m, \sqcup_m, \sqcap_m, \delta_\top \rangle$ is a join-complete semi-lattice.
At this point we can observe that 0-pseudo-metrics naturally induce an equivalence relation between elements with a distance of zero. In this section, we thus abstract 0-pseudo-metrics into the equivalence relations induced by them.

Let $Rel(\mathbf{C})$ be the set of equivalence relations on $\mathbf{C}$. In the following, given an element $x \in \mathbf{C}$ and an equivalence relation $\mathbf{R} \in Rel(\mathbf{C})$, $[x]_{\mathbf{R}}$ denotes the equivalence class of $x$ induced by $\mathbf{R}$, i.e., $[x]_{\mathbf{R}} \stackrel{\text{def}}{=} \{y \in \mathbf{C} \mid y \mathbf{R} x\}$. We define a partial order $\preceq$ on $Rel(\mathbf{C})$ such that, for any $\mathbf{R}, \mathbf{S} \in Rel(\mathbf{C})$, $\mathbf{R} \preceq \mathbf{S}$ if and only if $\forall x \in \mathbf{C}: [x]_{\mathbf{R}} \subseteq [x]_{\mathbf{S}}$. We have the following Galois insertion

$$ \langle \mathbf{M}_0(\mathbf{C}), \sqsubseteq_{\mathbf{R}} \rangle \underset{\alpha_{\mathbf{R}}}{\overset{\gamma_{\mathbf{R}}}{\leftarrow}} \langle \mathrm{Rel}(\mathbf{C}), \preceq \rangle $$

where the abstraction function $\alpha_{\mathbf{R}}: \mathbf{M}_0(\mathbf{C}) \to Rel(\mathbf{C})$ is

$$ \alpha_{\mathbf{R}}(\delta) \stackrel{\text{def}}{=} \{(x, y) \in \mathbf{C} \times \mathbf{C} \mid \delta(x, y) = 0\} $$

and the concretization function $\gamma_{\mathbf{R}}: Rel(\mathbf{C}) \to \mathbf{M}_0(\mathbf{C})$ is

$$ \gamma_{\mathbf{R}} \stackrel{\text{def}}{=} \lambda(x, y). \begin{cases} 0 & x \mathbf{R} y \\ \infty & \text{otherwise} \end{cases} $$

Thus, the domain $\langle Rel(\mathbf{C}), \preceq \rangle$ is an abstraction of $\langle \mathbf{M}_0(\mathbf{C}), \sqsubseteq_{\mathbf{R}} \rangle$. Let $\rho_{\mathbf{R}} \stackrel{\text{def}}{=} \gamma_{\mathbf{R}} \circ \alpha_{\mathbf{R}}$, we have that $\rho_{\mathbf{R}}$ is a uco on $\mathbf{M}_0(\mathbf{C})$.

**Theorem 2.** $\rho_{\mathbf{R}} \in Uco(\mathbf{M}_0(\mathbf{C}))$.

Note that $\rho_{\mathbf{R}}$ is not an isomorphism since a 0-pseudo-metric $\delta$ may also assign non-zero distances between elements. However, through the abstraction, these distances are stretched to $\infty$ in $\rho_{\mathbf{R}}(\delta)$. More generally, $\rho_{\mathbf{R}}$ abstracts 0-pseudo-metrics into pseudo-metrics, ignoring all non-zero distances between elements.

Let $\mathbf{M}_{\mathbf{R}}(\mathbf{C}) \stackrel{\text{def}}{=} \rho_{\mathbf{R}}(\mathbf{M}_0(\mathbf{C})) = \rho_{\mathbf{R}} \circ \rho_0(\mathbf{M}(\mathbf{C}))$ and let $\delta_{\infty} \in \mathbf{M}_{\mathbf{R}}(\mathbf{C})$ be defined as:

$$ \delta_{\infty} \stackrel{\text{def}}{=} \lambda(x, y). \begin{cases} 0 & x = y \\ \infty & \text{otherwise} \end{cases} $$

**Proposition 3.** $\langle \mathbf{M}_{\mathbf{R}}(\mathbf{C}), \sqsubseteq_{\mathbf{R}}, \sqcup_{\mathbf{R}}, \sqcap_{\mathbf{R}}, \delta_{\infty} \rangle$ is a complete lattice.

Note that $\delta_{\top} = \gamma_{\mathbf{R}}(\top)$, where $\top \in Rel(\mathbf{C})$ is such that $\forall x, y \in \mathbf{C}: x \top y$, and $\delta_{\infty} = \gamma_{\mathbf{R}}(\mathrm{id})$, where $\mathrm{id} \in Rel(\mathbf{C})$ is such that $x \mathrm{id} y \stackrel{\text{def}}{\iff} x = y$. Thus, $\mathbf{M}_{\mathbf{R}}(\mathbf{C}) \subseteq \mathbf{M}_0(\mathbf{C}) \subseteq \mathbf{M}(\mathbf{C})$ is the complete sub-lattice of $\mathbf{M}(\mathbf{C})$ uniquely identifying equivalence relations.

*Example 8.* Let us consider $\delta_t$ of Ex. 7. Its abstraction $\delta_r \stackrel{\text{def}}{=} \rho_{\mathbf{R}}(\delta_t)$ is such that $\delta_r = \delta_t$ except for $\delta_r(12, 14) = \delta_r(12, 34) = \infty$.

$$ \delta_r: \begin{array}{rcl} 1 & \leftarrow & \mathbf{0} \rightarrow 3 \\ & \multicolumn{2}{c}{\mathbf{13} \leftarrow \mathbf{0} \rightarrow \mathbf{12}} \\ & \multicolumn{2}{c}{\mathbf{\Phi} \leftarrow \mathbf{0} \rightarrow \mathbf{2}} \\ & & \end{array} \quad \begin{array}{c} \equiv \\ \boxed{1 \ 3} \\ \boxed{2 \ 12 \ 13} \\ \boxed{34 \ 234} \end{array} $$

In the depiction above on the right, we show an equivalent representation of $\delta_r$ where different elements inside the same box are assigned with a distance of zero, while all other distances between elements in different boxes or between the other, not depicted, elements of $\mathbf{C}$ are $\infty$. $\triangleleft$
### 3.4 From Equivalence Relations to Upper Closure Operators

<figure><img src="image_5.png" /></figure>

The next step in the abstraction process is to move from equivalence relations towards (extensive) functions and afterward to upper closure operators.

Let $Fun(\mathbb{C})$ be the set of total functions on $\mathbb{C}$ ordered point-wise, i.e., $f \stackrel{\text{def}}{\leq_c} g \quad \forall x \in \mathbb{C} \cdot f(x) \leq_c g(x)$.

**Proposition 4.** $\langle Fun(\mathbb{C}), \stackrel{\text{def}}{\leq_c}, \dot{v}_c, \dot{\Lambda}_c, \lambda x. \top_c, \lambda x. \bot_c \rangle$ is a complete lattice.

Given an equivalence relation $\mathbb{R} \in Rel(\mathbb{C})$ we can construct a total function $f: \mathbb{C} \to \mathbb{C}$ that maps each element in $\mathbb{C}$ to a representative element of its equivalence class under $\mathbb{R}$. Various choices are possible for this representative element, but since our ultimate goal is to characterize ucos, which in particular are extensive functions, we define $f$ such that each equivalence class is mapped to its least upper bound, thus ensuring that $f$ is extensive.

Formally, let $Ext(\mathbb{C}) \stackrel{\text{def}}{=} \{f: \mathbb{C} \to \mathbb{C} \mid \forall x \in \mathbb{C} \cdot x \leq_c f(x)\} \subset Fun(\mathbb{C})$ be the set of all extensive functions on $\mathbb{C}$. Clearly $Ext(\mathbb{C})$ forms a complete sub-lattice of $Fun(\mathbb{C})$. Note that $\lambda x. \bot_c$ is the smallest function with respect to the point-wise order in $Fun(\mathbb{C})$ but, not being extensive, it cannot be the smallest function in $Ext(\mathbb{C})$, where the bottom element is the identity function $\iota$.

**Proposition 5.** $\langle Ext(\mathbb{C}), \stackrel{\text{def}}{\leq_c}, \dot{v}_c, \dot{\Lambda}_c, \lambda x. \top_c, \iota \rangle$ is a complete lattice.

We define the following function $\alpha_e: Rel(\mathbb{C}) \to Ext(\mathbb{C})$ as

$$ \alpha_e(\mathbb{R}) \stackrel{\text{def}}{=} \lambda x \in \mathbb{C}. \bigvee([x]_\mathbb{R}) $$

Note that $\alpha_e$ is not surjective since an extensive function could lead the elements to be greater than the least upper bound.

**Example 9.** Suppose $\mathbb{C} = \wp(\{1, 2, 3, 4\})$ and consider $\delta_r$ of Ex. 8. Let $\mathbb{R}$ the corresponding equivalence relation depicted in Ex. 8. Its abstraction $f \stackrel{\text{def}}{=} \alpha_e(\mathbb{R})$ is the identity function except for $f(1) = f(3) = 13$, $f(2) = f(12) = f(13) = 123 = f(123)$, $f(34) = f(234) = 234$. Hence, $f$ collapses the image of 123 with the one of 2, 12, and 13, since, for instance, $f(12) = \bigvee([12]_\mathbb{R}) = \bigvee\{2, 12, 13\} = 123$. $\triangleleft$

From the domain of extensive function $Ext(\mathbb{C})$, we can use the construction in [15] to further enforce monotonicity and idempotence thus characterizing the complete sub-lattice of ucos on $\mathbb{C}$, i.e., $\langle Uco(\mathbb{C}), \stackrel{\text{def}}{\leq_c}, \dot{v}_c, \dot{\Lambda}_c, \lambda x. \top_c, \iota \rangle$, where the point-wise order $\stackrel{\text{def}}{\leq_c}$ reflects the relative precision between ucos.

Let $Mon(\mathbb{C}) \stackrel{\text{def}}{=} \{f \in Ext(\mathbb{C}) \mid \forall x, y \in \mathbb{C} \cdot x \leq_c y \Rightarrow f(x) \leq_c f(y)\}$ be the set of monotone extensive functions. To enforce monotonicity, we leverage the operator $\mathbb{M}: Ext(\mathbb{C}) \to Mon(\mathbb{C})$ [15] defined as

$$ \mathbb{M}(f) \stackrel{\text{def}}{=} \lambda x. \bigvee \{f(y) \mid y \leq_c x\} $$
which, given an extensive function $f \in \mathrm{Ext}(\mathcal{C})$, yields the least monotone extensive function greater than $f$. This means that $\mathbb{M} \in \mathrm{Uco}(\mathrm{Ext}(\mathcal{C}))$, identifying the sub-lattice of monotone and extensive functions [15].

To enforce idempotence, we leverage $\mathbb{I} : \mathrm{Mon}(\mathcal{C}) \to \mathrm{Uco}(\mathcal{C})$ [15] defined as

$$ \mathbb{I}(f) \stackrel{\mathrm{def}}{=} \mathrm{Ifp}_f^{\dot{\leq}_c} (\lambda g.g \circ g) $$

which, given a monotone and extensive function $f \in \mathrm{Mon}(\mathcal{C})$, yields the smallest idempotent function greater than $f$. Thus, $\mathbb{I} \in \mathrm{Uco}(\mathrm{Mon}(\mathcal{C}))$ and, by defining $\rho_{\mathrm{Im}} \stackrel{\mathrm{def}}{=} \mathbb{I} \circ \mathbb{M} \in \mathrm{Uco}(\mathrm{Ext}(\mathcal{C}))$, we have $\mathrm{Uco}(\mathcal{C}) = \rho_{\mathrm{Im}}(\mathrm{Ext}(\mathcal{C}))$.

We now define the following Galois insertion

$$ \langle \mathrm{Rel}(\mathcal{C}), \llangle \rangle \stackrel{\gamma_{\mathbb{I}}}{\leftarrow} \underset{\alpha_{\mathbb{I}}}{\stackrel{\gamma_{\mathbb{I}}}{\Rightarrow}} \langle \mathrm{Uco}(\mathcal{C}), \dot{\leq}_c \rangle $$

where the abstraction $\alpha_{\mathbb{I}} : \mathrm{Rel}(\mathcal{C}) \to \mathrm{Uco}(\mathcal{C})$ is

$$ \alpha_{\mathbb{I}}(\mathbb{R}) \stackrel{\mathrm{def}}{=} \rho_{\mathrm{Im}} \circ \alpha_e(\mathbb{R}) $$

and the concretization $\gamma_{\mathbb{I}} : \mathrm{Uco}(\mathcal{C}) \to \mathrm{Rel}(\mathcal{C})$ is

$$ \gamma_{\mathbb{I}}(\rho) \stackrel{\mathrm{def}}{=} \{(x, y) \in \mathbb{C} \times \mathbb{C} \mid \rho(x) = \rho(y)\} $$

We have that $\rho_{\mathbb{I}} \stackrel{\mathrm{def}}{=} \gamma_{\mathbb{I}} \circ \alpha_{\mathbb{I}}$ defines a uco on $\mathrm{Rel}(\mathcal{C})$.

**Theorem 3.** $\rho_{\mathbb{I}} \in \mathrm{Uco}(\mathrm{Rel}(\mathcal{C}))$.

*Example 10.* Consider $\mathcal{C} = \wp(\{1, 2, 3, 4\})$ and $f$ of Ex. 9. Then $f_m \stackrel{\mathrm{def}}{=} \mathbb{M}(f)$ is such that $f_m = f$ except for $f_m(14) = 134$, $f_m(23) = 123$, and $f_m(24) = f_m(124) = f_m(134) = f_m(1234) = 1234 = f_m(34) = f_m(234)$ (since $f_m(3)$ adds 1 and 3, while $f_m(34)$ adds 2 and 4). Finally, $\rho = \mathbb{I}(f_m)$ is such that $\rho = f_m$ except for $\rho(1) = \rho(3) = 123$ (since $f_m(1) = f_m(3) = 13$ and $f_m(13) = 123 = f_m(123)$) and $\rho(14) = 1234$ (since $f_m(14) = 134$ and $f_m(134) = 1234 = f_m(1234)$). The corresponding equivalence relation $\mathbb{R}_{\rho} \stackrel{\mathrm{def}}{=} \gamma_{\mathbb{I}}(\rho)$ is

$$ \mathbb{R}_{\rho} : \begin{array}{ccccccc} \color{red}{1} & \color{red}{2} & \color{red}{3} & \color{red}{12} & \color{red}{13} & \color{red}{23} & \color{red}{123} \\ \hline \color{red}{14} & \color{red}{24} & \color{red}{34} & \color{red}{124} & \color{red}{134} & \color{red}{234} & \color{red}{1234} \end{array} $$

representing a uco over $\mathcal{C} = \wp(\{1, 2, 3, 4\})$ with fix points $\emptyset, 4, 123, 1234$. $\triangleleft$

## 3.5 Upper Closure Operators as Pre-Metrics: The Domain $M_u(\mathcal{C})$

<figure><img src="image_6.png" /></figure>
The last step consists of identifying the pre-metrics that can be uniquely associated with a uco. We define the following Galois insertion

$$ \langle \mathcal{M}_0(\mathbf{C}), \sqsubseteq_{\mathbf{m}} \rangle \stackrel{\gamma_u}{\underset{\alpha_u}{\rightleftarrows}} \langle Uco(\mathbf{C}), \dot{\leq}_{\mathbf{c}} \rangle $$

where the abstraction $\alpha_u: \mathcal{M}_0(\mathbf{C}) \to Uco(\mathbf{C})$ is

$$ \alpha_u \stackrel{\text{def}}{=} \alpha_{\mathfrak{f}} \circ \alpha_{\mathfrak{r}} $$

and the concretization $\gamma_u: Uco(\mathbf{C}) \to \mathcal{M}_0(\mathbf{C})$ is

$$ \gamma_u(\rho) \stackrel{\text{def}}{=} \gamma_{\mathfrak{r}} \circ \gamma_{\mathfrak{f}} = \lambda(x, y). \begin{cases} 0 & \rho(x) = \rho(y) \\ \infty & \text{otherwise} \end{cases} $$

We have that $\rho_u \stackrel{\text{def}}{=} \gamma_u \circ \alpha_u$ defines a uco on $\mathcal{M}_0(\mathbf{C})$ forcing all the properties described in the previous sections on the collections of elements with 0-distance and forgetting (setting to $\infty$) all the other distances.

**Theorem 4.** $\rho_u \in Uco(\mathcal{M}_0(\mathbf{C}))$.

$$ \text{Let } \mathcal{M}_u(\mathbf{C}) \stackrel{\text{def}}{=} \rho_u(\mathcal{M}_0(\mathbf{C})) = \rho_u \circ \rho_0(\mathcal{M}(\mathbf{C})). $$

**Proposition 6.** $\langle \mathcal{M}_u(\mathbf{C}), \sqsubseteq_{\mathbf{m}}, \sqcup_{\mathbf{m}}, \sqcap_{\mathbf{m}}, \delta_{\top}, \delta_{\infty} \rangle$ is a complete lattice.

We finally have the following increasing chain between pre-metric domains:

$$ \mathcal{M}_u(\mathbf{C}) \subset \mathcal{M}_r(\mathbf{C}) \subset \mathcal{M}_0(\mathbf{C}) \subset \mathcal{M}(\mathbf{C}) $$

In particular, $\mathcal{M}_u(\mathbf{C})$ is the sub-lattice of pre-metrics uniquely identifying ucos on the complete lattice $\mathbf{C}$.

<figure><img src="image_7.png" /><figcaption>Fig. 2: From pre-metrics to ucos, and back.</figcaption></figure>

Fig. 2 illustrates the full abstraction process from pre-metrics to ucos developed in this section. It shows that ucos can, in general, be viewed as specific instances of pre-metrics (via $\gamma_u$). However, ucos are far from trivial: deriving one from a pre-metric requires that the distance satisfy specific and often stringent conditions. As a result, ucos obtained through abstraction ($\alpha_{\mathfrak{f}}\alpha_{\mathfrak{r}}\rho_u$) retain a distinct identity, reflecting structural properties of the underlying domain $\mathbf{C}$.
## 4 Combining Distances (and Abstractions)

In this section, building on our view of ucos as abstractions of pre-metrics, we study a way to compose pre-metrics—akin to how compositions of ucos can be defined. Specifically, we define a combination of pre-metrics that enables a *layered abstraction*: a first pre-metric determines how to aggregate elements (at distance zero)—to select the domain of comparison—and a second pre-metric measures distances within this selected domain between the identified aggregations.

Let us consider $\delta_1, \delta_2 \in \mathbb{M}(\mathbb{C})$, and let $f[\delta_1]$ be a selector map $f[\delta_1] : \mathbb{C} \to \mathbb{C}$ associating with each element $z \in \mathbb{C}$ a unique element $f_z \in \mathbb{C}$ at distance of zero from $z$ with respect to $\delta_1$, i.e., such that if $f_z \stackrel{\text{def}}{=} f[\delta_1](z)$ then $\delta_1(f_z, z) = 0$. Then, we can combine $\delta_1$ and $\delta_2$, leveraging $f[\delta_1]$, as follows:

$$ \delta_1 \triangleright_f \delta_2 \stackrel{\text{def}}{=} \lambda(x, y). \begin{cases} 0 & \delta_1(x, y) = 0 \\ \delta_2(f[\delta_1](x), f[\delta_1](y)) & \text{otherwise} \end{cases} $$

**Proposition 7.** Let $\delta_1, \delta_2 \in \mathbb{M}(\mathbb{C})$. Then also $\delta_1 \triangleright_f \delta_2 \in \mathbb{M}(\mathbb{C})$.

*Example 11.* Let $\Sigma$ be a chosen alphabet (finite set of characters) and let $\Sigma^*$ be the Kleene closure of $\Sigma$, i.e., the set of all strings of finite length over $\Sigma$. We consider the poset $\langle \wp(\Sigma^*), \subseteq \rangle$. Let us define $\delta_{\Sigma} : \wp(\Sigma^*) \times \wp(\Sigma^*) \to \mathbb{N}^{\infty}$ to compute the absolute difference between the number of string lengths between two sets of strings $W_1, W_2 \in \wp(\Sigma^*)$. Formally:

$$ \delta_{\Sigma}(W_1, W_2) \stackrel{\text{def}}{=} \delta_{\text{siz}}(\{\text{length}(w_1) \mid w_1 \in W_1\}, \{\text{length}(w_2) \mid w_2 \in W_2\}) $$

where $\delta_{\text{siz}}$ is the size distance of Ex. 3 and length($w$) is the number of characters composing the (finite) string $w$.

The composition $\delta_{\text{siz}} \triangleright_f \delta_{\Sigma}$, with $f[\delta_{\text{siz}}] = \iota$, computes the distance between the cardinality of string lengths only when the string sets have different cardinality. For instance, given $W_1 = \{a\}$ and $W_2 = \{bb\}$, then $\delta_{\text{siz}}(W_1, W_2) = 0$ and therefore $\delta_{\text{siz}} \triangleright_f \delta_{\Sigma}(W_1, W_2) = 0$. Instead, given $W_1$ and $W_3 = \{a, bb, cc\}$, we have $\delta_{\text{siz}} \triangleright_f \delta_{\Sigma}(W_1, W_2) = 2$ and thus $\delta_{\text{siz}} \triangleright_f \delta_{\Sigma}(W_1, W_3) = \delta_{\Sigma}(W_1, W_3) = 1$.

Vice versa, $\delta_{\Sigma} \triangleright_f \delta_{\text{siz}}$, with $f[\delta_{\Sigma}] = \iota$, computes the distance between the cardinality of the string sets only when the sets of their strings lengths have different lengths. For instance, $\delta_{\Sigma}(W_1, W_2) = 0$ and thus $\delta_{\Sigma} \triangleright_f \delta_{\text{siz}}(W_1, W_2) = 0$, while $\delta_{\Sigma}(W_1, W_3) = 1$ and therefore $\delta_{\Sigma} \triangleright_f \delta_{\text{siz}}(W_1, W_3) = \delta_{\text{siz}}(W_1, W_3) = 2$. $\triangleleft$

At this point, we can use the operation $\triangleright_f$ for combining a distance $\delta_{\rho} \in \mathbb{M}_{\omega}(\mathbb{C})$ characterizing a semantic abstraction $\rho \in \text{Uco}(\mathbb{C})$ (cf. Sec. 3.5), and another distance $\delta_{\mathcal{C}} \in \mathbb{M}(\mathbb{C})$ that we want to use for measuring the distances between abstract elements, i.e. elements in $\rho(\mathbb{C})$. As for selector function $f[\delta_{\rho}]$, we can exploit precisely the structure of the elements assigned with a distance of zero in $\delta_{\rho}$. Namely, we can take the least upper bound of the elements at distance zero, which by construction is at distance zero (cf. Sec. 3.4). Formally, let us define $\delta_{\mathcal{C}}^{\text{def}} \stackrel{\text{def}}{=} \delta_{\rho} \triangleright_f \delta_{\mathcal{C}}$ with $f[\delta_{\rho}] \stackrel{\text{def}}{=} \lambda x. \bigvee \{w \mid \delta_{\rho}(x, w) = 0\}$. Note that the definition of $f[\delta_{\rho}]$ satisfies the condition to be a selector function since, by construction of
$\delta_{\rho} \in \mathbb{M}_{u}(\mathbb{C})$, we have that: $\forall x \in \mathbb{C}$. $\delta_{\rho}(f[\delta_{\rho}](x), x) = 0$. The combination distance $\delta_{\rho} \triangleright_{f} \delta_{\mathbb{C}}$ is the conjunction of a semantic approximation $\rho$ (cf. Def. 2) and a quantitative approximation $\delta_{\mathbb{C}}$ (cf. Def. 4):

**Proposition 8.** Let $\delta_{\rho} \in \mathbb{M}_{u}(\mathbb{C})$ characterize $\rho \in \text{Uco}(\mathbb{C})$ and let $\delta_{\mathbb{C}} \in \mathbb{M}(\mathbb{C})$. Let $f[\delta_{\rho}] = \lambda x. \bigvee \{w | \delta_{\rho}(x, w) = 0\}$ on $\mathbb{C}$, then

$$ \forall x, y \in \mathbb{C}. (\delta_{\rho} \triangleright_{f} \delta_{\mathbb{C}})(x, y) = \delta_{\mathbb{C}}(\rho(x), \rho(y)) $$

We formally define this general notion of approximation below.

**Definition 6 (General Approximation).** Let $\langle \mathbb{C}, \leq_{\mathbb{C}} \rangle$ be a poset and $\langle \mathbb{C}, \delta_{\mathbb{C}} \rangle$ be a pre-metric space, and let $\rho \in \text{Uco}(\mathbb{C})$. We define the general approximation as follows for any $x, y \in \mathbb{C}$:

$$ \delta_{\mathbb{C}}^{\rho}(x, y) \stackrel{\text{def}}{=} \delta_{\mathbb{C}}(\rho(x), \rho(y)) $$

An element $x \in \mathbb{C}$ is semantically approximated with $\rho$ and quantitatively approximated by $\delta_{\mathbb{C}}$, up to $\varepsilon \in \mathbb{R}_{\geq 0}^{\infty}$, by any element in the set $\{y \in \mathbb{C} | \delta_{\mathbb{C}}^{\rho}(x, y) \leq \varepsilon\}$.

That is, $\delta_{\mathbb{C}}^{\rho}(x, y)$ calculates the distance between the semantic approximations of $x$ and $y$ with $\rho$. Clearly, when considering the identity function $\iota \in \text{Uco}(\mathbb{C})$ as abstraction, it holds that $\delta_{\iota} \triangleright_{f} \delta_{\mathbb{C}} = \delta_{\mathbb{C}}^{\rho}(x, y) = \delta_{\mathbb{C}}(x, y)$ for any $x, y \in \mathbb{C}$.

*Example 12.* Continuing Ex. 2 and Ex. 5, the set $\{0, 1, 4\}$ can be semantically and quantitatively approximated by $\delta_{\text{Int}} \triangleright_{f} \delta_{\text{siz}} = \delta_{\text{siz}}^{\text{Int}}$ and $\varepsilon = 1$ in any set in

$$ \{S \in \wp(\mathbb{Z}) | \delta_{\text{siz}}^{\text{Int}}(\{0, 1, 4\}, S) \leq 1\} = \{S \in \wp(\mathbb{Z}) | \text{Int}(S) = [-1, 4] \lor \text{Int}(S) = [0, 5]\} \triangleleft $$

In the following sections, we build on this general approximation framework a new confidentiality property—based on the notion of Abstract Non-Interference—that quantifies semantic variations in the output domain. This leads to a novel property we call *Partial Abstract Non-Interference*. We prove that it has a strong relation with Partial Completeness [5,7,8], a property modeling imprecision of an abstraction in the context of abstract interpretation, but it provides a novel perspective on precision, as it happens for the (not partial) corresponding notions.

# 5 (Partial) Completeness and Abstract Non-Interference

We briefly recall the notions of Completeness and Partial Completeness in abstract interpretation, as well as Abstract Non-Interference (ANI).

**Completeness.** Given a monotone function $f: \mathbb{C} \to \mathbb{D}$ over posets $\langle \mathbb{C}, \leq_{\mathbb{C}} \rangle$ and $\langle \mathbb{D}, \leq_{\mathbb{D}} \rangle$, the abstractions $\eta \in \text{Uco}(\mathbb{C})$ and $\rho \in \text{Uco}(\mathbb{D})$ can be used to approximate computations, thus defining an abstract version $f^{\mathbb{D}}: \eta(\mathbb{C}) \to \rho(\mathbb{D})$ of $f$. An abstract function $f^{\mathbb{D}}$ is *sound* when $\rho \circ f \leq_{\mathbb{D}} f^{\mathbb{D}} \circ \eta$ [14]. A sound by construction approximation is $f^{\mathbb{D}} \stackrel{\text{def}}{=} \rho \circ f \circ \eta$, called the best correct approximation (bca) [14]
of $f$. Any $f^\sharp$ soundly approximating $f$ is, in fact, equal or less precise than the bca, formally: $\rho \circ f \le_D f^\alpha \le_D f^\sharp \circ \eta$ [14].

A sound abstract computation $f^\sharp: \eta(C) \to \rho(D)$ performs a *precise approximation* of a (concrete) monotone function $f: C \to D$ whenever $\rho \circ f = f^\sharp \circ \eta$. It has been proved that for a precise abstract approximation to exist, the bca $f^\alpha$ must also be precise [13,26]. In particular, if $f^\sharp$ is a precise abstract approximation of $f$ then $f^\sharp = f^\alpha$. *Completeness* [13,26] in abstract interpretation is a desirable property that ensures the existence of a precise abstract approximation of a (concrete) monotone function $f$. Formally$^4$:

**Definition 7 (Completeness [13,26]).** Let $\langle C, \le_C \rangle$ and $\langle D, \le_D \rangle$ be posets, and let $\eta \in Uco(C)$ and $\rho \in Uco(D)$ be the input and output abstractions, respectively. A monotone function $f: C \to D$ satisfies Completeness w.r.t. $\langle \eta, \rho \rangle$ when the following condition holds: $\forall x \in C. \rho \circ f(x) = \rho \circ f \circ \eta(x)$.

In other words, proving the Completeness of $f$ w.r.t. the input and output abstractions $\langle \eta, \rho \rangle$ means proving the bca $\rho \circ f \circ \eta$ is precise.

**Partial Completeness.** In practice, Completeness is rarely satisfied. For this reason, Campion et al. [5,7,8] introduced a weaker notion of completeness, called *Partial Completeness*, by the use of pre-metrics compatible with the ordering of the underlying poset.

**Definition 8 (Order-Compatible Distance [8]).** Let $\langle L, \le_L \rangle$ be a poset. A distance $\delta: L \times L \to \mathbb{R}^\infty$ is said to be compatible with the ordering $\le_L$ or, in short, $\le_L$-compatible, if and only if it also satisfies the following property $\forall x, y, z \in L$:

$$x \le_L y \le_L z \Rightarrow \delta(x, y) \le \delta(x, z) \wedge \delta(y, z) \le \delta(x, z). \quad (\text{chains-order})$$

A poset $\langle L, \le_L \rangle$ equipped with a $\le_L$-compatible distance $\delta$ is called a distance compatible space and is denoted by the triple $\langle L, \le_L, \delta \rangle$.

The purpose of the (*chains-order*) axiom is to give a meaning to distances between comparable elements. Notably, let $f_1^\sharp$ and $f_2^\sharp$ be sound abstract approximations of a concrete monotone function $f: C \to D$, i.e., $\rho \circ f \le_D f_1^\sharp \circ \eta$ and $\rho \circ f \le_D f_2^\sharp \circ \eta$. If $f_1^\sharp$ is more precise than $f_2^\sharp$, i.e., $f_1^\sharp \le_D f_2^\sharp$, we expect a decrease in the imprecision (distance) with respect to the concrete computation when using $f_1^\sharp$ rather than $f_2^\sharp$, i.e., $\forall x \in D: \delta(\rho \circ f(x), f_1^\sharp \circ \eta(x)) \le \delta(\rho \circ f(x), f_2^\sharp \circ \eta(x))$.

**Example 13.** The poset $\langle \wp(L), \subseteq \rangle$ and the size distance $\delta_{siz}$ from Ex. 3 form a pseudo-metric compatible space. $\triangleleft$

For additional examples of order-compatible pre-metrics and their applications in domains used within the context of program analysis, we refer to [8].

<footnote n="4">⁴ This definition of Completeness is also called Backward-Completeness [26].</footnote>
Def. 8 is general enough to be instantiated with other definitions of distances used in the literature of abstract interpretation (see, e.g., [5,30,31,19,41]).

We can now recall the definition of ε-Partial Completeness, adapted here in the context of ucos and by leveraging Def. 6 for rewriting the condition.

**Definition 9 (ε-Partial Completeness [5,8]).** Let $\langle C, \le_c \rangle$ be a poset and $\langle D, \le_D, \delta_D \rangle$ be a pre-metric compatible space, let $\eta \in Uco(C)$ and $\rho \in Uco(D)$ be the input and output abstractions, respectively. Let $\varepsilon \in \mathbb{R}_{\ge 0}^{\infty}$. A monotone function $f: C \to D$ satisfies $\varepsilon$-Partial Completeness w.r.t. $\langle \eta, \delta_D^\rho \rangle$ if and only if the following condition holds: $\forall x \in C. \delta_D^\rho(f(x), f \circ \eta(x)) \le \varepsilon$.

The equality requirement of Def. 7 is relaxed by admitting a bounded imprecision, i.e. a bounded distance, between $\rho \circ f(x)$ and the bca $\rho \circ f \circ \eta(x)$ for all $x \in C$, which must not exceed $\varepsilon$. The imprecision to be measured and bounded is encoded in the pre-metric $\le_D$-compatible $\delta_D$ defined on the output domain $D$.

**Example 14.** We consider the pre-metric compatible space $\langle \wp(Z), \subseteq, \delta_{siz} \rangle$ where $\delta_{siz}$ is the size distance defined in Ex. 3, the complete lattice $\langle \wp(Z), \subseteq, \cup, \cap, Z, \emptyset \rangle$, and the standard denotational collecting semantics over it $[[Q]]: \wp(Z) \to \wp(Z)$ of the following program $Q \in \text{Prog}$:

$$ \textbf{while } x > 1 \textbf{ do } x := x - 2 $$

Let us set $\rho = \eta = \text{Int}$. Then $[[Q]]$ does not satisfy Completeness for $\langle \text{Int}, \text{Int} \rangle$ because for the input $\{2, 4\}$ we get:

$$ \text{Int}([Q]\{2, 4\}) = [0, 0] \subset [0, 1] = \text{Int}([Q]\{2, 3, 4\}) = \text{Int}([Q]\text{Int}(\{2, 4\})) $$

However, if we allow an imprecision quantified by $\varepsilon = 1$, which for $\delta_{siz}$ corresponds to accepting one spurious element between the two results, we get:

$$ \delta_{siz}^{\text{Int}}([Q]\{2, 4\}, [Q]\text{Int}(\{2, 4\})) = \delta_{siz}([0, 0], [0, 1]) \le 1 $$

In particular, it is easy to note that $\delta_{siz}^{\text{Int}}([Q]S, [Q]\text{Int}(S)) \le 1$, for all input sets $S \in \wp(Z)$, which implies that $[[Q]]$ satisfies 1-Partial Completeness w.r.t. $\langle \text{Int}, \delta_{siz}^{\text{Int}} \rangle$. $\triangleleft$

It is worth noting that, if a function $f$ is proved to satisfy Completeness for abstractions $\langle \eta, \rho \rangle$, then $f$ is also 0-Partial Complete for $\langle \eta, \delta_D^\rho \rangle$ with respect to any pre-metric order-compatible $\delta$ (thanks to the (if-identity) axiom). However, the converse does not hold if the (iff-identity) axiom is not satisfied by $\delta$, e.g., when $\delta$ is a pseudo-metric.

**Abstract Non-Interference.** Non-Interference [27] is a confidentiality policy that safeguards sensitive input information from affecting observable computation results. This concept has been relaxed to encompass variations in properties that might influence computations [21,32,24,22,33]. Additionally, the distinction between secret/relevant and public/observable data can be interpreted as an abstraction of data. In particular, Non-Interference has been extended and refined
through abstract interpretation, yielding a confidentiality policy called Abstract Non-Interference [24]. Following [35], we will focus on the flavor of Abstract Non-Interference considering an input data property to protect, when assuming an abstract observation of computations (this notion is called narrow in [24]).

**Definition 10 (Abstract Non-Interference [24]).** Let $\langle C, \le_c \rangle$ and $\langle D, \le_D \rangle$ be posets, and let $\eta \in Uco(C)$ and $\rho \in Uco(D)$ be abstractions. A function $f: C \to D$ satisfies Abstract Non-Interference (ANI for short) w.r.t. $\langle \eta, \rho \rangle$ when:

$$ \forall x, y \in C. \eta(x) = \eta(y) \Rightarrow \rho \circ f(x) = \rho \circ f(y) $$

*Example 15.* Consider the complete lattice $\langle \wp(Z), \subseteq, \cup, \cap, Z, \emptyset \rangle$, the standard collecting semantics $\llbracket P \rrbracket: \wp(Z) \to \wp(Z)$, and the following program P:

$$ \mathbf{if} \ (x \bmod 2=0 \land x \neq 0) \ \mathbf{then} \ x := (x/2)^2 \ \mathbf{else} \ x := -x^2 + (1-|x|) $$

where $\bmod$ is the modulo operation. Let $\mathrm{Par} \in Uco(\wp(Z))$ be the parity abstraction over input values, and $\mathrm{Sign} \in Uco(\wp(Z))$ the sign abstraction over output values (cf. Ex. 1). In this program, for any even value, we return a positive number; for 0, we return 1 (hence a positive value), while for odd numbers, we return a negative value. Formally, for all $N, M \in \wp(Z)$, if $\mathrm{Par}(N) = \mathrm{Par}(M)$ then we have $\mathrm{Sign}(\llbracket P \rrbracket N) = \mathrm{Sign}(\llbracket P \rrbracket M)$, thus $\llbracket P \rrbracket$ satisfies ANI w.r.t. $\langle \mathrm{Par}, \mathrm{Sign} \rangle$. It should be clear that, if we consider as input abstractions any convex abstract domain other than $\mathrm{Par}$ (mixing in the same abstract value even and odd values) such as $\mathrm{Sign}$ or $\mathrm{Int}$, then ANI w.r.t. $\mathrm{Sign}$ as output abstraction (e.g., $\langle \mathrm{Sign}, \mathrm{Sign} \rangle$ or $\langle \mathrm{Int}, \mathrm{Sign} \rangle$) does not hold anymore. $\triangleleft$

Although Abstract Non-Interference and Completeness may initially appear to be distinct notions, they have been proved to be equivalent in [35]. This equivalence enables the reuse of verification mechanisms for ANI to verify Completeness. Conversely, domain transformers that induce Completeness (e.g., [26,3]) can also be repurposed to enforce ANI.

# 6 A General Approximated Confidentiality Property

Non-Interference [27] has been widely adopted to model various security properties, particularly confidentiality, which concerns the control of information flow within a computer system. Despite its widespread use in academic research, Non-Interference is rarely achievable in real-world systems for two main reasons: first, it is a very strong property that requires complete indistinguishability of data; second, practical systems often need to reveal some information to function—for example, a password checker necessarily leaks some information about the input when indicating whether access is granted. As a result, several weakened variants of Non-Interference have been proposed. Broadly, these relaxations fall into two categories, which correspond to the two types of approximation discussed in Sec. 4: semantic approximation and quantitative approximation.
Abstract Non-Interference (cf. Def. 10) adopts a semantic approach, replacing indistinguishability between data with indistinguishability between properties of data. This constitutes a semantic approximation, as it requires the abstraction of the program semantics to be indistinguishable whenever the inputs are indistinguishable with respect to a given abstract property. In language-based security, it means that if the observable output remains within the group of all acceptable outputs (modeled as an abstraction), the system is deemed secure.

Approximate Non-Interference [18] follows a quantitative approach, where indistinguishability between data is replaced by similarity. Originally introduced in the context of probabilistic process algebras, this notion requires that the observable behaviors of two agents differ by no more than a threshold $\epsilon$, rather than being strictly identical as in standard Non-Interference [27].

Our idea is to combine the two approximation strategies (cf. Sec. 4)—semantic and quantitative—while keeping the two types of approximation explicitly distinct. This leads to a new notion called *Partial Abstract Non-Interference*, where indistinguishability between data is replaced by similarity between properties of data. In security, Partial ANI would offer a more refined modeling capability. Instead of requiring outputs to be indistinguishable under a coarse abstraction, it allows outputs to vary, as long as the variation remains within a specified quantitative bound. This enables a more nuanced treatment of security policies, especially when small, bounded differences in outputs are tolerable.

## 6.1 Partial Abstract Non-Interference

Partial Abstract Non-Interference is a novel relaxation of Non-Interference that combines both semantic and quantitative approximations. Specifically, it observes properties of data (as in ANI) rather than raw data, while allowing for a bounded distance between these observed properties.

**Definition 11 (ε-Partial Abstract Non-Interference).** Let $\langle C, \preceq_C \rangle$ be the input domain and $\langle D, \preceq_D \rangle$ be the output one (posets), respectively. Let $\langle C, \delta_C \rangle$ and $\langle D, \delta_D \rangle$ be pre-metric spaces. Let $\eta \in Uco(C)$, $\rho \in Uco(D)$ be the abstractions of the input and output domains, respectively, and $\epsilon \in \mathbb{R}_{\ge 0}^\infty$. A function $f: C \to D$ satisfies $\epsilon$-Partial Abstract Non-Interference ($\epsilon$-Partial ANI for short) w.r.t. $\langle \delta_C^\eta, \delta_D^\rho \rangle$ when the following implication holds:

$$ \forall x, y \in C. \delta_C^\eta(x, y) = 0 \Rightarrow \delta_D^\rho(f(x), f(y)) \le \epsilon $$

Starting from inputs whose property distance is zero according to $\delta_C^\eta$, i.e., $\delta_C^\eta(x, y) = 0$, Partial ANI allows the function to produce different outputs, potentially with different properties under $\delta_D^\rho$, as long as the variation remains bounded, specifically not exceeding a given threshold $\epsilon$, i.e. $\delta_D^\rho(f(x), f(y)) \le \epsilon$. It is important to note that the condition $\delta_C^\eta(x, y) = 0$ does not imply $\eta(x) = \eta(y)$ (as required for ANI, cf. Def. 10) since $\delta_C$ is a pre-metric and may therefore violate the (iff-identity) axiom. As a result, on the left-hand side of the implication, Partial ANI allows inputs to be mapped by $\eta$ to different abstract properties, while still being indistinguishable with respect to $\delta_C$.
Example 16. Consider the program R: if $x > 0$ then $x := x-1$ else $x := x+1$. and the standard collecting denotational semantics $\llbracket R \rrbracket: \wp(Z) \to \wp(Z)$. Let us consider the counting distance $\delta_{siz}$, defined in Ex. 3 and the abstract domain of intervals $\mathit{Int} \in \mathit{Uco}(\wp(Z))$. In this program, if we start from an interval composed by positive values only (e.g. $[1, 8]$), then $\llbracket R \rrbracket$ decreases all the values by one (i.e., $[0, 7]$). Something similar happens when all the elements in the interval are negative, e.g., $[-5, -2]$ returning $[-4, -1]$. The only case in which the dimension of an input interval changes is when the lower bound is non-positive (and thus increased by one) and the upper bound is positive (and thus decreased by one), e.g., $[-2, 5]$ becomes $[-1, 4]$. This means that starting from two sets $S_1, S_2 \in \wp(Z)$ whose interval abstraction has the same number of values (i.e., $\delta_{siz}^{\mathit{Int}}(S_1, S_2) \le 0$), e.g. $\delta_{siz}^{\mathit{Int}}(\{-9, -2\}, \{1, 3, 5, 8\}) = 0$, we obtain as output two respective intervals with the same number of elements, e.g. $\delta_{siz}^{\mathit{Int}}(\{-8, -1\}, \{0, 2, 4, 7\}) = \delta_{siz}([0, -1], [0, 7]) = 0$, or, in the worst case, with a difference of two, i.e., $\delta_{siz}^{\mathit{Int}}(\llbracket R \rrbracket S_1, \llbracket R \rrbracket S_2) \le 2$. For instance, $\delta_{siz}^{\mathit{Int}}(\{-5, 0, 2\}, \{1, 8\}) = 0$ in input, and $\delta_{siz}^{\mathit{Int}}(\{-4, 1\}, \{0, 7\}) = 2$ in output. Hence, we can say that the collecting semantics of the program R satisfies 2-Partial ANI w.r.t. $\langle \delta_{siz}^{\mathit{Int}}, \delta_{siz}^{\mathit{Int}} \rangle$.

Conversely, consider this time the program $R^*$ where $*$ is the Kleene closure of regular commands [40] whose semantics is defined as follows: $\forall S \in \wp(Z)$. $\llbracket R^* \rrbracket S \stackrel{\mathrm{def}}{=} \bigcup \{\llbracket R \rrbracket^n S \mid n \in \mathbb{N}\}$ and where $\llbracket R \rrbracket^n$ is the composition of program R $n$ times. Then Partial ANI does not hold for any $\varepsilon$ (except for the trivial case $\varepsilon = \infty$). In particular, for any input whose interval abstraction has bounds of opposite sign, e.g., $[-2, 4]$, the result is precisely the same interval since the collecting semantics keeps the greater collection; if the lower bound is not negative, e.g., $[2, 6]$, then it is pushed to 0 in the output, i.e., $[0, 6]$; while if the upper bound is not positive, e.g., $[-4, -2]$, then this is pushed to 1, i.e., $[-4, 1]$. This means that for instance $\delta_{siz}([2, 6], [21, 25]) \le 0$ but $\delta_{siz}^{\mathit{Int}}(\llbracket R^* \rrbracket[2, 6], \llbracket R^* \rrbracket[21, 25]) = \delta_{siz}([0, 6], [0, 25]) = 19$, and this difference may increase without limit. $\triangleleft$

By fixing the bound on the difference between output properties to $\varepsilon = 0$, Partial ANI reduces to the following slight generalization of ANI:

$$ \forall x, y \in \mathbb{C} . \delta_{\mathbb{C}}^{\eta}(x, y) = 0 \Rightarrow \delta_{\mathbb{D}}^{\rho}(f(x), f(y)) \le 0 $$

This notion collapses to ANI (cf. Def. 10) when both $\delta_{\mathbb{C}}$ and $\delta_{\mathbb{D}}$ satisfy the (iff-identity) axiom, namely when both are quasisemi-metrics.

On the other hand, if we move into the field of process algebra, if we consider $\eta = \top$ (i.e., we do not have constraints on the input processes), $\delta_{\mathbb{C}}$ is any quasisemi-metric, and we consider as $\rho$ the observation of the processes, then Partial ANI (cf. Def. 11) collapses to Approximate Non-interference [18].

## 6.2 On the Relation with Partial Completeness

In the last decade, it has been proved that there is a strong relation between the property of Completeness in abstract interpretation and Abstract Non-Interference [35]. Specifically, we know that requiring Completeness of a function
w.r.t. an input and output abstractions, is equivalent to requiring that function inputs sharing the same property are mapped to outputs that also share the same property (i.e., ANI).

In this section, we study the relation between Partial Completeness (cf. Def. 9) and Partial ANI (cf. Def. 11). When generalizing ANI to Partial ANI by combining semantic and quantitative approximations, the equivalence between Completeness and ANI (proved in [35]) becomes an implication between ε-Partial ANI and ε-Partial Completeness. Vice versa, when we are considering a quasisemi-metric space and a pseudo-metric space for the input and output domains, respectively, there is an implication between ε-Partial Completeness and 2ε-Partial ANI. These statements are proved in the following two theorems:

**Theorem 5 (ε-Partial ANI) ⇒ ε-Partial Completeness).** Let $\langle C, \preceq_C \rangle$ be a poset equipped with a pre-metric (not necessarily order-compatible) $\delta_C$, and $\langle D, \preceq_D, \delta_D \rangle$ be a pre-metric compatible space. Let $\eta \in Uco(C)$, $\rho \in Uco(D)$ be abstractions and $\varepsilon \in \mathbb{R}_{\ge 0}^\infty$. If a monotone function $f: C \to D$ satisfies $\varepsilon$-Partial ANI w.r.t. $\langle \delta_C^\eta, \delta_D^\rho \rangle$ then $f$ satisfies $\varepsilon$-Partial Completeness w.r.t. $\langle \eta, \delta_D^\rho \rangle$, namely:

$$[\forall x, y \in C. \delta_C^\eta(x, y) \le 0 \Rightarrow \delta_D^\rho(f(y), f(x)) \le \varepsilon] \Rightarrow [\forall x \in C. \delta_D^\rho(f(x), f \circ \eta(x)) \le \varepsilon]$$

*Example 17.* Consider again the pre-metric compatible space $\langle \wp(Z), \subseteq, \delta_{siz} \rangle$ and the abstraction $\mathrm{Int} \in Uco(\wp(Z))$. From Ex. 16, we know that $\llbracket \mathbb{R} \rrbracket$ satisfies 2-Partial ANI w.r.t. $\langle \delta_{siz}^{\mathrm{Int}}, \delta_{siz}^{\mathrm{Int}} \rangle$, i.e., $\delta_{siz}^{\mathrm{Int}}(X, Y) \le 0 \Rightarrow \delta_{siz}^{\mathrm{Int}}(\llbracket \mathbb{R} \rrbracket X, \llbracket \mathbb{R} \rrbracket Y) \le 2$ for any $X, Y \in \wp(Z)$. Thus, by Thm. 5, it satisfies 2-Partial Completeness w.r.t. $\langle \mathrm{Int}, \delta_{siz}^{\mathrm{Int}} \rangle$, i.e., $\delta_{siz}^{\mathrm{Int}}(\llbracket \mathbb{R} \rrbracket X, \llbracket \mathbb{R} \rrbracket \mathrm{Int}(X)) \le 2$ for any $X \in \wp(Z)$. In fact, the bound 2 for Partial Completeness is not tight as $\llbracket \mathbb{R} \rrbracket$ also satisfies 1-Partial Completeness w.r.t. $\langle \mathrm{Int}, \delta_{siz}^{\mathrm{Int}} \rangle$. Indeed, given $X = \{-1, 1\}$, we have $\delta_{siz}^{\mathrm{Int}}(\llbracket \mathbb{R} \rrbracket \{-1, 1\}, \llbracket \mathbb{R} \rrbracket \mathrm{Int}(\{-1, 1\})) = \delta_{siz}(\llbracket 0, 0 \rrbracket, \llbracket 0, 1 \rrbracket) \le 1$, while for any $Y \in \wp(Z) \setminus \{-1, 1\}$ we have $\delta_{siz}^{\mathrm{Int}}(\llbracket \mathbb{R} \rrbracket Y, \llbracket \mathbb{R} \rrbracket \mathrm{Int}(Y)) \le 0$. $\triangleleft$

**Theorem 6 (ε-Partial Completeness ⇒ 2ε-Partial ANI).** Let $\langle C, \preceq_C \rangle$ be a poset equipped with a quasisemi-metric (not necessarily order-compatible) $\delta_C$, and $\langle D, \preceq_D, \delta_D \rangle$ be a pseudo-metric compatible space. Let $\eta \in Uco(C)$, $\rho \in Uco(D)$ be the input and output abstractions, respectively, and $\varepsilon \in \mathbb{R}_{\ge 0}^\infty$. If a monotone function $f: C \to D$ satisfies $\varepsilon$-Partial Completeness w.r.t. $\langle \eta, \delta_D^\rho \rangle$ then $f$ satisfies 2ε-Partial ANI w.r.t. $\langle \delta_C^\eta, \delta_D^\rho \rangle$, namely:

$$[\forall x \in C. \delta_D^\rho(f(x), f \circ \eta(x)) \le \varepsilon] \Rightarrow [\forall x, y \in C. \delta_C^\eta(x, y) \le 0 \Rightarrow \delta_D^\rho(f(y), f(x)) \le 2\varepsilon]$$

Thm. 5 shows that having a proof of $\varepsilon$-Partial ANI of $f$ w.r.t. $\langle \delta_C^\eta, \delta_D^\rho \rangle$, implies that $f$ is partial complete w.r.t. $\langle \eta, \delta_D^\rho \rangle$ with the same bound of imprecision $\varepsilon$. In other words, if $f$ maps distinct inputs but having a zero distance according to $\delta_C$, to corresponding outputs that differ by an $\varepsilon$ amount according to $\delta_D$ (i.e., $f$ satisfies $\varepsilon$-Partial ANI), then there exists a sound abstract approximation of $f$ over $\langle \eta, \rho \rangle$, namely $\rho \circ f \circ \eta$, capable of producing a results with an imprecision, measured by $\delta_D$, not greater than the bound $\varepsilon$.

On the other hand, the use of $\delta_C^\eta$ and $\delta_D^\rho$ in the definitions of Partial ANI (cf. Def. 11) and Partial Completeness (cf. Def 9) amplifies the bound on the
output error by a constant factor in Thm. 6. This is because Partial ANI bounds the distance between $\rho \circ f(x)$ and $\rho \circ f(y)$, for all $x, y \in C$ that have distance smaller or equal than zero through the abstraction $\eta$, but Partial Completeness only guarantees a bound on the distance between $\rho \circ f(x)$ and $\rho \circ f(y)$, for all $x \in C$ with $y = \eta(x)$. We thus bound the output error for Partial ANI by adding up the distance between $\rho \circ f(x)$ and $\rho \circ f \circ \eta(x) = \rho \circ f \circ \eta(y)$, and between $\rho \circ f \circ \eta(x) = \rho \circ f \circ \eta(y)$ and $\rho \circ f(y)$.

Note also that Thm. 6 imposes stronger requirements than Thm. 5 on $\delta_C$ and $\delta_D$. Its applicability is more limited and strongly depends on which imprecision we are interested to measure, i.e. the type of distances used over the input and output domains, as shown by the following example.

**Example 18.** Consider again the pre-metric compatible space $\langle \wp(Z), \subseteq, \delta_{siz} \rangle$ and the abstraction $\mathbf{Int} \in Uco(\wp(Z))$. The collecting semantics $\llbracket \mathbb{R} \rrbracket$ from Ex. 16 satisfies 1-Partial Completeness w.r.t. $\langle \mathbf{Int}, \delta_{siz}^{\mathbf{Int}} \rangle$ (cf. Ex. 17). However, we cannot apply Thm. 6 to derive that $\llbracket \mathbb{R} \rrbracket$ also satisfies 2-Partial ANI w.r.t. $\langle \delta_{siz}^{\mathbf{Int}}, \delta_{siz}^{\mathbf{Int}} \rangle$ because $\delta_{siz}$ is not a quasisemi-metric (it does not satisfy the (iff-identity) axiom).

C

The relation between 0-Partial ANI and Completeness (cf. Def. 7) is a straight-
forward corollary of Thm. 5 and Thm. 6.

**Corollary 1 (0-Partial ANI ⇔ Completeness).** Let $\langle C, \preceq_C \rangle$ be a poset that is equipped with a (not necessarily order-compatible) pre-metric $\delta_C$, and let $\langle D, \preceq_D$, $\delta_D \rangle$ be a quasisemi-metric order-compatible space. Let $\eta \in Uco(C)$, $\rho \in Uco(D)$ be abstractions, and $\varepsilon \in \mathbb{R}_{\ge 0}^\infty$. A monotone function $f: C \to D$ satisfies 0-Partial ANI w.r.t. $\langle \delta_C^\eta, \delta_D^\rho \rangle$ if and only if $f$ satisfies Completeness w.r.t. $\langle \eta, \rho \rangle$, namely:

$$
[\forall x, y \in C. \delta_C^{\eta}(x, y) \le 0 \Rightarrow \delta_D^{\rho}(f(y), f(x)) \le 0] \Leftrightarrow [\forall x \in C. \rho f(x) = \rho \circ f \circ \eta(x)]
$$

7 Related Work

The approach we propose, transitioning from pre-metrics to ucos, involves prov-
ing a non-trivial abstraction relation between equivalence relations and ucos.
This is not the first work in this direction; indeed, in the literature [29], it has
been shown that equivalence relations on a domain C correspond to ucos on ϱ(C)
(and more generally, the most concrete uco associated with an equivalence re-
lation R, has R as its kernel). In the present work, we needed to associate any
equivalence relation on C with a uco defined directly on C, rather than on ϱ(C).
This shift in the domain where the uco is formalized introduces a significant
difference and makes the correspondence notably less straightforward. Indeed,
defining a uco on ϱ(C) can be done straightforwardly by mapping each x ∈ C to
its equivalence class (a subset of C) as shown in [29]. In contrast, our approach
requires defining a uco directly on C, which means selecting a representative el-
ement within C for each equivalence class. This selection is nontrivial, as there
is no canonical or optimal choice that naturally leads to a well-defined uco.
Another strongly related work is [15], where the authors define the function transformers making any total function in $Fun(C)$ a uco. In particular, they define the monotonicity transformer $M$ and an extensivity transformer, let us call it $\mathbb{E}$, on generic total functions $Fun(C)$, showing also that $M \circ \mathbb{E} = \mathbb{E} \circ M$. In our work, we start from $Rel(C)$ (instead of $Fun(C)$), and we observed that it was possible to move from $Rel(C)$ to $Ext(C)$ directly, avoiding so far the application of $\mathbb{E}$ and applying $M$ to extensive functions, thanks to the commutativity between the two transformers [15]. Finally, $\mathbb{1}$ is applied precisely to monotone and extensive functions, as it happens in [15], inhering so far all the results.

When considering the general approximation based on the combination of pre-metrics and abstractions, we can identify related ideas in other existing works. Partial Completeness (discussed in Sec. 5 and 6.2) is such an example. More recently, a similar idea has been explored in the context of Deep Neural Networks (a multi-layered machine learning model) robustness, where resistance to adversarial attacks is modeled by combining a distance over inputs with an abstraction of the outputs [25].

We also have a correspondence between ANI and Input Data (Non-)Usage [42] when $f$ is deterministic, i.e., Input Data (Non-)Usage is an instance of ANI [36].

Although Partial ANI is a novel notion, Thm. 6 (and Cor. 1) ensures that verification mechanisms developed for Partial Completeness can be reused to verify Partial ANI. For example, in [5], the authors introduced a proof system for deriving triples of the form $[Pre]P[Post, \varepsilon]$, meaning that the distance $\delta_D^\rho([P](Pre), Post) \le \varepsilon$ holds. In light of Thm. 6, a proof of $[Pre]P[[P]]\rho(Pre), \varepsilon]$, that is, $[P]$ satisfies $\varepsilon$-Partial Completeness w.r.t. $\langle\iota, \delta_D^\rho\rangle$, implies that $[P]$ also satisfies $2\varepsilon$-Partial ANI with respect to $\langle\delta_C^\iota, \delta_D^\rho\rangle$, assuming $\delta_C^\iota$ is a quasi-metric. A similar reasoning applies to the proof system proposed in [23] to derive Completeness, which, under the premises of Cor. 1, also yield a proof of 0-Partial ANI. Moreover, existing (and potentially future) domain transformer techniques developed to enforce Completeness (e.g., [26,2]) and Partial Completeness can similarly be adapted to enforce Partial ANI.

# 8 Conclusion

We established a formal relation between quantitative approximations, formalized by pre-metrics, and semantic approximations, captured by upper closure operators, through a chain of Galois connections. This result shows that, under certain structural conditions on a pre-metric, a corresponding semantic abstraction can be derived via Galois connections. Conversely, abstractions defined via ucos can be interpreted as specific instances of pre-metrics, highlighting a bidirectional connection between the two frameworks. We then formalized a composition of pre-metrics that first selects the domain of comparison and then measures distances within this selected domain, thereby enabling a form of layered abstraction. Such a composition, when involving a distance characterizing a semantic abstraction and a distance characterizing a quantitative abstraction, defines a new form of approximation, called general approximation, combining
semantic and quantitative approaches while keeping the two types of approxi-
mations distinct. This general approximation captures the idea of allowing an
approximate observation of data through abstraction, while also tolerating a cer-
tain error in the observation, quantified by a distance between abstractions. We
believe that this is a promising approach to approximation, already used in some
way in the literature, as we have seen in Sec. 7. In particular, we exploit this
approach for defining a new partial form of ANI, where we accept an error in the
observed output properties. We showed that this notion is strongly connected to
the well-established property of Partial Completeness in abstract interpretation,
mirroring the relation between the standard versions of ANI and Completeness.

As future work, we plan to formalize a deductive system specialized for prov-
ing Partial ANI of programs. Other deductive systems for the verification of Com-
pleteness [23] (and its local version [3]), Partial Completeness [5] and ANI [35]
have already been formalized in the literature. As already discussed in Sec. 6,
a verification mechanism for Partial ANI could build upon the framework de-
veloped for Partial Completeness and ANI [21], particularly in light of Thm. 6.
This connection is promising, even though the approach in [5] focuses on a local
variant of the property. Moreover, this future direction could inspire the de-
velopment of an abstract interpretation-based static analyzer for verifying the
Partial ANI property of programs. The challenge here lies in the fact that Partial
ANI is a hyperproperty [12], and thus the standard abstract interpretation-based
overapproximations of sets of traces cannot be directly applied.

The proposed Partial ANI notion is a *global* property, in the sense that it
is universally quantified over all inputs. As a future work, we plan to formal-
ize its *local* version, namely requiring Partial ANI over a strict subset of the
input domain, and study its relation with other local properties in the context
of abstract interpretation [1,3,6,34]. Dropping the universal quantification may
invalidate the correlation already established between the global counterparts.

We formalized abstractions as ucos, which have been proven to be equivalent
to Galois insertions [16]. In the future, we would like to consider weaker abstrac-
tion notions able to formalize properties that do not necessarily admit a best
abstraction, such as the domain of convex polyhedra [28] or formal languages [4].
In this direction, the notion of weak closures defined in [35] could be considered.

Finally, in the literature there are numerous quantitative program properties
under various formalisms (e.g. Quantitative Data Usage [38,37], Approximated
Non-Interference [18], etc.) and other could be obtained by applying the general
approximation mechanism of Sec. 4 (e.g. a quantitative general version of pro-
gram monotonicity [6] or program continuity [9,11]). It could be interesting to
build a taxonomy of quantitative program properties, in which the quantification
mechanisms are expressed within a unified formalism, such as the combination of
pre-metrics and abstractions presented in Sec. 4, and to study the assumptions
under which one property implies another.

**Acknowledgements** This work was partially supported by the project SERICS (PE00000014) under the MUR National Recovery and Resilience Plan funded
by the European Union - NextGenerationEU; by PRIN2022PNRR "RAP-ARA"
(PE6) - codice MUR: P2022HXNSC; by the SAIF project, funded by the "France
2030" government investment plan managed by the French National Research
Agency, under the reference ANR-23-PEIA-0006.

References

1. Bruni, R., Giacobazzi, R., Gori, R., Ranzato, F.: A logic for locally complete abstract interpretations. In: 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021. pp. 1–13. IEEE (2021). https://doi.org/10.1109/LICS52264.2021.9470608

2. Bruni, R., Giacobazzi, R., Gori, R., Ranzato, F.: Abstract interpretation repair. In: Jhala, R., Dillig, I. (eds.) PLDI ’22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. pp. 426–441. ACM (2022). https://doi.org/10.1145/3519939.3523453

3. Bruni, R., Giacobazzi, R., Gori, R., Ranzato, F.: A correctness and incorrectness program logic. J. ACM 70(2), 15:1–15:45 (2023). https://doi.org/10.1145/3582267

4. Campion, M., Dalla Preda, M., Giacobazzi, R.: Abstract interpretation of indexed grammars. In: Chang, B.E. (ed.) 26th Static Analysis Symposium (SAS 2019). Lecture Notes in Computer Science, vol. 11822, pp. 121–139. Springer (2019). https://doi.org/10.1007/978-3-030-32304-2_7

5. Campion, M., Dalla Preda, M., Giacobazzi, R.: Partial (in)completeness in abstract interpretation: limiting the imprecision in program analysis. Proc. ACM Program. Lang. 6(POPL), 1–31 (2022). https://doi.org/10.1145/3498721

6. Campion, M., Dalla Preda, M., Giacobazzi, R., Urban, C.: Monotonicity and the precision of program analysis. Proc. ACM Program. Lang. 8(POPL), 1629–1662 (2024). https://doi.org/10.1145/3632897

7. Campion, M., Preda, M.D., Giacobazzi, R.: On the properties of partial completeness in abstract interpretation. In: Lago, U.D., Gorla, D. (eds.) Proceedings of the 23rd Italian Conference on Theoretical Computer Science, ICTCS 2022, Rome, Italy, September 7-9, 2022. CEUR Workshop Proceedings, vol. 3284, pp. 79–85. CEUR-WS.org (2022), https://ceur-ws.org/Vol-3284/8665.pdf

8. Campion, M., Urban, C., Preda, M.D., Giacobazzi, R.: A formal framework to measure the incompleteness of abstract interpretations. In: Hermenegildo, M.V., Morales, J.F. (eds.) Static Analysis - 30th International Symposium, SAS 2023. Lecture Notes in Computer Science, vol. 14284, pp. 114–138. Springer (2023). https://doi.org/10.1007/978-3-031-44245-2_7

9. Chaudhuri, S., Gulwani, S., Lublinerman, R.: Continuity Analysis of Programs. In: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 57–70. POPL ’10, Association for Computing Machinery (2010). https://doi.org/10.1145/1706299.1706308

10. Chaudhuri, S., Gulwani, S., Lublinerman, R.: Continuity and Robustness of Programs 55(8), 107–115 (2012). https://doi.org/10.1145/2240236.2240262

11. Chaudhuri, S., Gulwani, S., Lublinerman, R., NavidPour, S.: Proving Programs Robust. In: Gyimóthy, T., Zeller, A. (eds.) SIGSOFT/FSE’11 19th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-19). pp. 102–112. ACM (2011). https://doi.org/10.1145/2025113.2025131

12. Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157–1210 (2010). https://doi.org/10.3233/JCS-2009-0393
13. Cousot, P.: Principles of Abstract Interpretation. The MIT Press, Cambridge, Mass. (2021)

14. Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977. pp. 238–252. ACM (1977). https://doi.org/10.1145/512950.512973

15. Cousot, P., Cousot, R.: A constructive characterization of the lattices of all retractions, preclosure, quasi-closure and closure operators on a complete lattice. Portugaliae Mathematica 38(1-2), 185–198 (1979), http://eudml.org/doc/115380

16. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Aho, A.V., Zilles, S.N., Rosen, B.K. (eds.) Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages. pp. 269–282. ACM Press (1979). https://doi.org/10.1145/567752.567778

17. Deza, M.M., Laurent, M.: Geometry of cuts and metrics, Algorithms and combinatorics, vol. 15. Springer (1997). https://doi.org/10.1007/978-3-642-04295-9

18. Di Pierro, A., Hankin, C., Wiklicky, H.: Approximate non-interference. J. Comput. Secur. 12(1), 37–82 (2004). https://doi.org/10.3233/JCS-2004-12103

19. Di Pierro, A., Wiklicky, H.: Measuring the precision of abstract interpretations. In: Lau, K. (ed.) 10th Logic Based Program Synthesis and Transformation (LOP-STR’00). LNCS, vol. 2042, pp. 147–164. Springer (2000)

20. Dwork, C., McSherry, F., Nissim, K., Smith, A.D.: Calibrating noise to sensitivity in private data analysis. In: Halevi, S., Rabin, T. (eds.) Theory of Cryptography, Third Theory of Cryptography Conference, TCC 2006. LNCS, vol. 3876, pp. 265–284. Springer (2006). https://doi.org/10.1007/11681878_14

21. Giacobazzi, R., Mastroeni, I.: Proving abstract non-interference. In: J. Marcinkowski, A.T. (ed.) Annual Conf. of the European Association for Computer Science Logic (CSL ’04). vol. 3210, pp. 280–294. Springer-Verlag (2004)

22. Giacobazzi, R., Mastroeni, I.: Adjoining classified and unclassified information by abstract interpretation. Journal of Computer Security 18(5), 751–797 (2010)

23. Giacobazzi, R., Logozzo, F., Ranzato, F.: Analyzing program analyses. In: Rajamani, S.K., Walker, D. (eds.) Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015. pp. 261–273. ACM (2015). https://doi.org/10.1145/2676726.2676987

24. Giacobazzi, R., Mastroeni, I.: Abstract non-interference: A unifying framework for weakening information-flow. ACM Trans. Priv. Secur. 21(2), 9:1–9:31 (2018). https://doi.org/10.1145/3175660

25. Giacobazzi, R., Mastroeni, I., Perantoni, E.: Adversities in abstract interpretation - accommodating robustness by abstract interpretation. ACM Trans. Program. Lang. Syst. 46(2), 5 (2024). https://doi.org/10.1145/3649309

26. Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. ACM 47(2), 361–416 (2000). https://doi.org/10.1145/333979.333989

27. Goguen, J.A., Meseguer, J.: Security policies and security models. In: 1982 IEEE Symposium on Security and Privacy, Oakland, CA, USA, April 26-28, 1982. pp. 11–20. IEEE Computer Society (1982). https://doi.org/10.1109/SP.1982.10014

28. Grünbaum, B., Klee, V., Perles, M.A., Shephard, G.C.: Convex polytopes, vol. 16. Springer (1967)

29. Hunt, S., Mastroeni, I.: The PER model of abstract non-interference. In: Hankin, C., Siveroni, I. (eds.) Static Analysis, 12th International Symposium, SAS 2005, London, UK, September 7-9, 2005, Proceedings. Lec-
ture Notes in Computer Science, vol. 3672, pp. 171–185. Springer (2005).
https://doi.org/10.1007/11547662_13

30. Liew, D., Cogumbreiro, T., Lange, J.: Sound and partially-complete static analysis of data-races in GPU programs. Proc. ACM Program. Lang. 8 (OOPSLA2), 2434–2461 (2024). https://doi.org/10.1145/3689797

31. Logozzo, F.: Towards a quantitative estimation of abstract interpretations. In: Workshop on Quantitative Analysis of Software. Microsoft (June 2009), https://www.microsoft.com/en-us/research/publication/towards-a-quantitative-estimation-of-abstract-interpretations/

32. Mastroeni, I.: On the role of abstract non-interference in language-based security. In: Yi, K. (ed.) 3rd Asian Symp. on Programming Languages and Systems (APLAS ’05). Lecture Notes in Computer Science, vol. 3780, pp. 418–433. Springer

33. Mastroeni, I.: Abstract interpretation-based approaches to security - a survey on abstract non-interference and its challenging applications. Electronic Proceedings in Theoretical Computer Science 129, 41–65 (Sep 2013).
https://doi.org/10.4204/eptcs.129.4, http://dx.doi.org/10.4204/EPTCS.129.4

34. Mastroeni, I.: Abstract local completeness - A local form of abstract non-interference. In: Krishna, S., Sankaranarayanan, S., Trivedi, A. (eds.) 26th Verification, Model Checking, and Abstract Interpretation (VMCAI 2025). Lecture Notes in Computer Science, vol. 15530, pp. 3–25. Springer (2025).
https://doi.org/10.1007/978-3-031-82703-7_1

35. Mastroeni, I., Pasqua, M.: Domain precision in galois connection-less abstract interpretation. In: Hermenegildo, M.V., Morales, J.F. (eds.) Static Analysis - 30th International Symposium, SAS 2023, Cascais, Portugal, October 22-24, 2023, Proceedings. Lecture Notes in Computer Science, vol. 14284, pp. 434–459. Springer (2023). https://doi.org/10.1007/978-3-031-44245-2_19

36. Mazzucato, D.: Static Analysis by Abstract Interpretation of Quantitative Program Properties. (Analyse Statique par Interprétation Abstraite de Propriétés Quantitatives de Programmes). Ph.D. thesis, École Normale Supérieure, Paris, France (2024), https://tel.archives-ouvertes.fr/tel-04886659

37. Mazzucato, D., Campion, M., Urban, C.: Quantitative input usage static analysis. In: Benz, N., Gopinath, D., Shi, N. (eds.) NASA Formal Methods - 16th International Symposium, NFM 2024, Moffett Field, CA, USA, June 4-6, 2024, Proceedings. Lecture Notes in Computer Science, vol. 14627, pp. 79–98. Springer (2024). https://doi.org/10.1007/978-3-031-60698-4_5

38. Mazzucato, D., Campion, M., Urban, C.: Quantitative static timing analysis. In: Giacobazzi, R., Gorla, A. (eds.) Static Analysis - 31st International Symposium, SAS 2024, Pasadena, CA, USA, October 20-22, 2024, Proceedings. Lecture Notes in Computer Science, vol. 14995, pp. 268–299. Springer (2024).
https://doi.org/10.1007/978-3-031-74776-2_11

39. Miné, A.: The octagon abstract domain. In: Burd, E., Aiken, P., Koschke, R. (eds.) Proc. of the 8th Working Conf. on Reverse Engineering, WCRE’01. p. 310. IEEE Computer Society (2001). https://doi.org/10.1109/WCRE.2001.957836

40. O'Hearn, P.W.: Incorrectness logic. Proc. ACM Program. Lang. 4 (POPL), 10:1–10:32 (2020). https://doi.org/10.1145/3371078

41. Sotin, P.: Quantifying the Precision of Numerical Abstract Domains. Research report (Feb 2010), https://inria.hal.science/inria-00457324

42. Urban, C., Müller, P.: An abstract interpretation framework for input data usage. In: Ahmed, A. (ed.) 27th European Symposium on Programming, ESOP 2018. Lecture Notes in Computer Science, vol. 10801, pp. 683–710. Springer (2018).
https://doi.org/10.1007/978-3-319-89884-1_24