# Complete Abstractions for Verification of Polymorphic Functions with Equality – extended version

Malo Revel, Thomas Genet, Thomas Jensen

► To cite this version:

Malo Revel, Thomas Genet, Thomas Jensen. Complete Abstractions for Verification of Polymorphic Functions with Equality – extended version. IRISA. 2026. hal-05454439v2

HAL Id: hal-05454439

https://inria.hal.science/hal-05454439v2

Submitted on 13 Jan 2026

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_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
Complete Abstractions for Verification of
Polymorphic Functions with Equality
extended version

Malo REVEL¹, Thomas GENET¹ ID, and Thomas JENSEN² ID

¹ Université de Rennes, IRISA, France

² Inria, Université de Rennes, France

**Abstract.** This paper is concerned with automatically proving properties on polymorphic programs over algebraic data types by reducing the verification of such properties to the verification of properties on monomorphised, abstract programs. For programs without polymorphic equality, the reduction exploits Wadler's "Theorem for Free". For programs using polymorphic equality, we provide a sufficient condition for the reduction to hold. The condition relies on the existence of a locally *complete* abstraction function whose image is a finite set of arbitrary constants chosen for abstracting primitive values. When such a condition exists, the number of arbitrary constants depends on the functions under concern and the properties to prove. We present an implementation that automatically computes the number of constants and, thus, ensures that proving the polymorphic case with equality can be reduced to the proof carried out on a monomorphic instance of the program. Experimental results show that this reduction is indeed possible with small abstract domains. Target programs support user-defined recursive ADTs and recursive first-order functions.

# 1 Introduction

This paper is concerned with the automatic verification of *polymorphic first-order* programs supporting a polymorphic equality primitive. The programs we consider manipulate polymorphic recursive algebraic data types (ADTs for short). Even without the polymorphic equality, analyzing such programs is, in itself, difficult. For non-recursive ADTs that contain numerical values, it has been showed [2] how to lift *relational* abstract domains for integers to such ADTs. Recursive ADTs on the other hand define unbounded data structures that require specific abstract domains to be modeled precisely. In this case, combining an abstract domain handling the ADT part (e.g. tree automata) and a numerical abstract domain is also possible [9, 11, 14].

These techniques work for monomorphic programs. The aim of this paper is to open new ways of proving properties on parametric polymorphic programs and polymorphic programs with polymorphic equality. We automatically *reduce* the verification of a polymorphic problem (with or without polymorphic equality)
to the verification of a monomorphic version of this problem. More specifically, we prove that if a polymorphic problem is true when instantiated on a certain finite abstract type, then the problem is true in general. With this principle we can e.g. prove that any polymorphic binary tree is equal to the mirroring of its mirroring, by proving that this property holds on trees where the set of labels is restricted to a set of cardinal 2.

The verification problems that we consider are boolean open terms of our language, e.g., eq_tree(t, mirror(mirror(t))). Since the functions are polymorphic, the verification problems also take a type as an argument (e.g. the type of the labels of the polymorphic tree t). A problem is considered to be true if it evaluates to the boolean true for any well-typed instance of its free variables.

Wadler’s “Theorems for Free” [17] provide a collection of examples where any abstract domain provides a complete abstraction for a given verification problem. However, this technique is not applicable as soon as the program to verify uses the polymorphic equality predicate. This is a significant restriction. To overcome this restriction, we propose to view this as a problem of polymorphic invariance [1]: is it possible to verify a property of all instances of a polymorphic function by just verifying it on one instance of the function over a finite domain? We show that this amounts to computing a finite locally complete abstract domain [5]. Locally complete means that the abstract domain is fixed, but the complete abstraction function depends on the arguments of the program. For instance, if A₂ is an abstract domain of size 2, then for all trees t, there exists an abstraction function α whose co-domain is A₂ and such that

$$ \alpha(\text{eq\_tree}(t, \text{mirror}(\text{mirror}(t)))) = \text{eq\_tree}(\alpha(t), \text{mirror}(\text{mirror}(\alpha(t)))) $$

The main contribution of this paper is an algorithm that can determine the size of the abstract domains necessary for constructing a complete abstraction that solves a polymorphic verification problem. The method works by analysing a symbolic execution of the program whose language is defined in Section 4. In Section 5 we introduce the class of abstract domains that we use, and we show how to execute programs on abstract values. A symbolic execution on concrete or abstract values is represented in the form of an execution tree (Section 6). In Section 7 we determine when it is possible to fold such an execution tree into a finite graph that unfolds to the original execution tree. The folding is found by solving a collection of inequality constraints. The main theoretical results of the paper is that the cardinality of the solution to these constraints determines the size of the complete abstract domain. We provide a worked example of the method in Section 8, a way to combine the results of the analysis of several functions occurring in a verification problem in Section 9, and details about implementation and experiments in Section 10.

## Contributions

- A fully automatic technique to prove properties on polymorphic functions with polymorphic equality that does not require annotations, intermediate lemmas or induction.
- A novel algorithm for automatically showing the existence of locally complete abstractions with constraint solving. To the best of our knowledge, this is the first use of locally complete abstractions for analysing polymorphic functions.

- An implementation of the constraint-solving method that has been integrated into an analyser of first-order polymorphic functional programs.

- Successful verification of polymorphic problems extracted from several benchmarks.

# 2 Overview of our method

## 2.1 An example without polymorphic equality

Let $P$ be the program defining $oddL(l)$, a parametric polymorphic function checking if the length of list $l$ is odd, $evenL(l)$ a parametric polymorphic function checking if the length of $l$ is even, and $conc(l_1, l_2)$ a parametric polymorphic function concatenating $l_1$ and $l_2$. We also assume that $P$ contains the definitions of $'∧'$ and $'⇒'$ as boolean functions. Assume that we want to prove that $P$ satisfies the verification problem:

$$ \phi_1 \stackrel{\text{def}}{=} \forall l_1 \ l_2. \ oddL(l_1) \land oddL(l_2) \implies evenL(conc(l_1, l_2)) $$

For any $k > 0$, we write $A_k$ for a finite type whose inhabitants are some constants $\{A_1, \dots, A_k\}$. Let $\phi_1[A_1]$ be the restriction of $\phi_1$ where $l_1, l_2$ are lists of arbitrary lengths whose elements are the constant $A_1$. The techniques described in [16, 8, 10, 13] are able to prove that $\phi_1[A_1]$ holds. They first infer an abstract model (a tree automaton) separating all the lists into two possible abstract values (regular tree languages): $L_{even}$ lists of even size and $L_{odd}$ lists of odd size. They also infer the abstractions for all the functions w.r.t this abstract domain:

$$ \begin{align*} oddL(L_{even}) &= \{\text{false}\} & conc(L_{even}, L_{even}) &= L_{even} \\ oddL(L_{odd}) &= \{\text{true}\} & conc(L_{odd}, L_{even}) &= L_{odd} \\ evenL(L_{even}) &= \{\text{true}\} & conc(L_{even}, L_{odd}) &= L_{odd} \\ evenL(L_{odd}) &= \{\text{false}\} & conc(L_{odd}, L_{odd}) &= L_{even} \end{align*} $$

With these values for the functions, the formula $\phi_1[A_1]$ is true. To prove that the verification $\forall X.\phi_1[X]$ (i.e. the verification of $\phi_1[X]$ for all types $X$) can be reduced to $\phi_1[A_1]$ we can exploit the paper “Theorems for free” by Wadler [17] to perform this reduction, i.e., prove that $\phi_1[A_1]$ entails $\phi_1$. Wadler shows that given the type of a polymorphic function, it is possible to derive a property that is satisfied by all functions of that type. In the following, we denote by TFF this property. In the original paper, Wadler denotes the application of any function $\alpha$ to each element of a list by $\alpha^*$. Since $oddL$, $evenL$ and $conc$ are parametric polymorphic functions, their TFF are the following (for all types $C$ and $A$):

1. $\forall l : list(C), \forall \alpha : C \to A. oddL(l) = oddL(\alpha^*(l))$

2. $\forall l : list(C), \forall \alpha : C \to A. evenL(l) = evenL(\alpha^*(l))$
3. $\forall l_1, l_2 : list(\mathbb{C}), \forall \alpha : \mathbb{C} \to \mathbb{A}. \alpha^*(conc(l_1, l_2)) = conc(\alpha^*(l_1), \alpha^*(l_2))$

If we choose $\mathbb{A}_1 = \{A_1\}$ as $\mathbb{A}$ and as the abstraction function $\alpha$ the function that maps every element to the constant $A_1$,

4. $\alpha^*$ maps any list to a list of $A_1$'s of the same length.

Using the theorems above, we have the following equivalences and implication:

$$
\begin{align*}
\phi_1[\mathbb{A}_1] &\stackrel{\text{def}}{=} \forall l_1 : \text{list}(\mathbb{A}_1) \quad l_2 : \text{list}(\mathbb{A}_1). \quad \text{oddL}(l_1) \wedge \text{oddL}(l_2) \Rightarrow \text{evenL}(\text{conc}(l_1, l_2)) \\
&\Downarrow \mathbf{4}. \\
&\forall l_1 \ l_2 \ \alpha : \mathbb{C} \to \mathbb{A}_1. \quad \text{oddL}(\alpha^*(l_1)) \wedge \text{oddL}(\alpha^*(l_2)) \Rightarrow \text{evenL}(\text{conc}(\alpha^*(l_1), \alpha^*(l_2))) \\
&\Uparrow \mathbf{3}. \\
&\forall l_1 \ l_2 \ \alpha : \mathbb{C} \to \mathbb{A}_1. \quad \text{oddL}(\alpha^*(l_1)) \wedge \text{oddL}(\alpha^*(l_2)) \Rightarrow \text{evenL}(\alpha^*(\text{conc}(l_1, l_2))) \\
&\Uparrow \mathbf{1}. \text{ and } \mathbf{2}. \\
\phi_1 &\stackrel{\text{def}}{=} \forall l_1 \ l_2. \quad \text{oddL}(l_1) \wedge \text{oddL}(l_2) \Rightarrow \text{evenL}(\text{conc}(l_1, l_2))
\end{align*}
$$

Thus, from the proof of $\phi_1[\mathbb{A}_1]$ on lists of $A_1$'s and the above equivalence, we get the proof of $\forall X.\phi_1[X]$ for lists of any type. Such reduction can be applied to any property proved on an abstract ADT manipulated by polymorphic functions.

## 2.2 An example with polymorphic equality

This is powerful and automatic for parametric polymorphic functions, but how to reduce properties when the programming language supports an *external* polymorphic equality predicate? This is the case in programming languages, like OCaml, where it is possible to define functions with a polymorphic type though they use the structural equality predicate. For such functions, we cannot directly apply TFF to obtain a reduction as above. To see an example of this short-coming, assume that we have a function $mem(x, l)$ checking if an element $x$ appears in a list $l$. We assume that $mem$ is defined using an external polymorphic equality primitive. Let $\phi_2 \stackrel{\text{def}}{=} \forall x. l. \ mem(x, l) \Rightarrow mem(x, \text{rev}(l))$.

TFF fails to reduce $\forall X.\phi_2[X]$. Wadler [17] and Day & al. [7] have shown that, by providing an equality predicate as an additional argument to a function $f$, it is possible to obtain a new TFF for $f$. However, as shown by Day & al. [7], this is of no help for our purpose, because it requires $\alpha$ to be one-to-one.

Reducing $\forall X.\phi_2[X]$ to $\phi_2[\mathbb{A}_2]$. In Section 2.1, in order to reduce the verification of $\forall X.\phi_1[X]$, we used TFF properties of the form $\forall \alpha. \alpha^* \circ f = f \circ \alpha^*$ (for all $\alpha$, $f$ and $\alpha$ "commute") for the functions $f$ appearing in $\phi_1$. Here $\alpha^*$ applies $\alpha$ not only to every element of a list, but to every element of an arbitrary term (this is formally defined in Definition 11). Unfortunately such properties do not hold when we allow the use of polymorphic equality. Indeed, let $x = 0$ and $l = [1]$ (the list whose only element is 1). The function $\alpha : \text{nat} \to \mathbb{A}_1$ does not satisfy $mem(0, [1]) = mem(\alpha(0), \alpha^*([1]))$. However, as we show below, we can reduce
$\forall X.\phi_2[X]$ to $\phi_2[\mathbb{A}_2]$ (i.e. $\phi_2$ where $x$ is either the constant $A_1$ or the constant $A_2$, and $l$ is a list of $A_1$'s and $A_2$'s), with the help of local completeness.

Here is a global overview of our workflow applied to the verification problem $\phi_2$. First, we independently analyse the code of mem and rev. Our algorithm answers that 2 constants are enough for mem. This means that the domain $\mathbb{A}_2$ is big enough to build locally complete abstractions for mem. Locally complete abstractions were studied by Bruni et al. [5]. Here, locally complete means that (a) for all types $\mathbb{C}$ and for all $x: \mathbb{C}$ and $l: list(\mathbb{C})$ there exists an abstraction function $\alpha: \mathbb{C} \to \mathbb{A}_2$ such that $mem(x, l) = mem(\alpha(x), \alpha^*(l))$. Let $\alpha$ be such that $\alpha(x) = A_1$ and $\forall x' \neq x, \alpha(x') = A_2$. At every position $i$ of $l$, the $i$th element of $l$ is equal to $x$ iff the $i$th element of $\alpha^*(l)$ is equal to $A_1 = \alpha(x)$. Thus $mem(x, l)$ and $mem(\alpha(x), \alpha^*(l))$ follow the same "evaluation path", and yield the same boolean: $mem(x, l) = mem(\alpha(x), \alpha^*(l))$.

Moreover, rev is a parametric polymorphic function, and its TFF is the following: (b) for all types $\mathbb{C}$ and $\mathbb{A}$, for all $\alpha: \mathbb{C} \to \mathbb{A}$, $rev \circ \alpha^* = \alpha^* \circ rev$. Besides, note that (c) if $\phi_2[\mathbb{A}_2]$ is true, then $mem(\alpha'(x), \alpha'^*(l)) \implies mem(\alpha'(x), rev(\alpha'^*(l)))$ holds for any choice of $x, l$ and $\alpha'$ with two constants. Now let us merge all these results together:

$$ \phi_2[\mathbb{A}_2] \stackrel{\text{def}}{=} \forall x : \mathbb{A}_2. \forall l : list(\mathbb{A}_2). mem(x, l) \implies mem(x, rev(l)) $$

↓ (c)

$$ \forall x : \mathbb{C} \forall l : list(\mathbb{C}). \forall \alpha'. mem(\alpha'(x), \alpha'^*(l)) \implies mem(\alpha'(x), rev(\alpha'^*(l))) $$

↑ (b)

$$ \forall x : \mathbb{C}. \forall l : list(\mathbb{C}). \forall \alpha'. mem(\alpha'(x), \alpha'^*(l)) \implies mem(\alpha'(x), \alpha'^*(rev(l))) $$

↓ We choose $\alpha$ appearing in (a) for $\alpha'$

$$ \forall x : \mathbb{C}. \forall l : list(\mathbb{C}). mem(\alpha(x), \alpha^*(l)) \implies mem(\alpha(x), \alpha^*(rev(l))) $$

↓ (a)

$$ \phi_2[\mathbb{C}] \stackrel{\text{def}}{=} \forall x : \mathbb{C}. \forall l : list(\mathbb{C}). mem(x, l) \implies mem(x, rev(l)) $$

Thus, proving that $\phi_2[\mathbb{A}_2]$ is true entails that the polymorphic problem $\phi_2$ in general is true. Using the afore-mentioned verification techniques [16, 8, 10, 13] we can prove that $\phi_2[\mathbb{A}_2]$ is true and, thus, that $\forall X.\phi_2[X]$ is true.

The most challenging part of our workflow is to automatically compute a finite abstract domain that is large enough to build a locally complete abstraction of a polymorphic function with equality. Our algorithm explores a symbolic *evaluation tree* of the function that represents every possible small-step evaluation path of this function. This algorithm is described in Sections 6 and 7.

## 3 Polymorphic problems and the reduction lemma

We first define the class of polymorphic problems that we consider and the lemma that permits to reduce the verification of a polymorphic problem to the verification of a monomorphic case. This lemma is our first contribution. It states that the reduction is legal if there exist locally complete abstraction functions for all functions of the polymorphic problem. Proving the existence of such abstractions is the difficult part that will be studied in detail in the next section.
A polymorphic verification problem is a term

$$ \phi = \lambda X. \lambda x_1 : I_1(X). \dots \lambda x_n : I_n(X). \psi(x_1, \dots, x_n) $$

where $I_i(X)$ are non-function types (possibly ADTs) that are parameterised by a type $X$ and $\psi(x_1, \dots, x_n)$ is a non-function term of type $\mathit{Bool}$ whose free variables are $x_1, \dots, x_n$. Note that in this paper we only consider verification problems and functions with at most one type variable, that we write $X$. For instance, $\phi_2$ may be written as $\lambda X. \lambda x : X. \lambda l : \mathit{list}(X). \mathit{mem}(x, l) \implies \mathit{mem}(x, \mathit{rev}(l))$.

We write $\phi[\mathbb{C}]$ for the verification problem $\phi$ monomorphised to a type $\mathbb{C}$, and we write $\phi[\mathbb{C}](t_1, \dots, t_n)$ for $\phi[\mathbb{C}]$ instantiated to the terms $t_i$ of types $I_i(\mathbb{C})$. The substitution $\sigma : x_i \mapsto t_i$ is called an *instantiation* of $\phi$ on $\mathbb{C}$, and we write $\sigma(\phi)$ for $\phi[\mathbb{C}](t_1, \dots, t_n)$. A verification problem $\phi$ is *true* if for all types $\mathbb{C}$, $\phi[\mathbb{C}]$ is true, i.e., for all instantiations $\sigma$ of $\phi$ on $\mathbb{C}$, $\sigma(\phi)$ evaluates to *true*.

For any $k > 0$, we write $\mathbb{A}_k$ for a type with $k$ distinct constants, whose inhabitants are written $A_1, \dots, A_k$. We consider the set $\mathbb{A}_k = \{A_1, \dots, A_k\}$ as an abstract domain: an abstraction function $\alpha : \mathbb{C} \to \mathbb{A}_k$ partitions $\mathbb{C}$ into $k$ classes $\alpha^{-1}(A_1), \dots, \alpha^{-1}(A_k)$.

**Example 1.** $\mathit{mem}$ has the polymorphic type $\forall X. X \times \mathit{list}(X) \to \mathit{Bool}$ and $\mathit{rev}$ has the polymorphic type $\forall X. \mathit{list}(X) \to \mathit{list}(X)$. Let $\sigma : x \mapsto 2, l \mapsto [4, 2, 1]$. The substitution $\sigma$ instantiates $\phi_2$ on the type $\mathit{Nat}$ of natural numbers. Let $\alpha : \mathit{Nat} \to \mathbb{A}_2$ be the abstraction function defined by $\alpha(2) = A_1$ and $\alpha(n) = A_2$ for all naturals $n \neq 2$. Thus, $\alpha^* \circ \sigma$ instantiates $\phi_2$ on $\mathbb{A}_2$ and $\sigma(\phi_2)$ and $(\alpha^* \circ \sigma)(\phi_2)$ both yield the same result.

**Lemma 1 (Reduction).** Let $\phi$ be a terminating polymorphic verification problem and $k > 0$ a number of constants. If for all instantiations $\sigma$ of $\phi$ on a type $\mathbb{C}$ there exists an abstraction function $\alpha : \mathbb{C} \to \mathbb{A}_k$ such that $\sigma(\phi)$ and $(\alpha^* \circ \sigma)(\phi)$ evaluate to the same result (we write this condition $R_k(\phi)$), then $\phi[\mathbb{A}_k] \implies \forall X. \phi[X]$ (If $\phi[\mathbb{A}_k]$ is true then $\phi$ is true in general).

*Proof.* Suppose that $\phi[\mathbb{A}_k]$ is true and $R_k(\phi)$ holds. We show that $\phi$ is true. Let $\sigma$ be an instantiation of $\phi$ on some type $\mathbb{C}$. By $R_k(\phi)$, there exists $\alpha : \mathbb{C} \to \mathbb{A}_k$ such that $\sigma(\phi)$ and $(\alpha^* \circ \sigma)(\phi)$ evaluate to the same result. $(\alpha^* \circ \sigma)$ is an instantiation of $\phi$ on $\mathbb{A}_k$, therefore $(\alpha^* \circ \sigma)(\phi)$ evaluates to true since $\phi[\mathbb{A}_k]$ is true. Therefore $\sigma(\phi)$ also evaluates to true.

Note that if a verification problem $\phi$ does not terminate on some inputs, then $\phi[\mathbb{A}_k]$ and $R_k(\phi)$ cannot both be true. Since $\phi[\mathbb{A}_k]$ is an abstracted version of the problem $\phi$ on a type with $k$ constants, verifying $\phi[\mathbb{A}_k]$ can be performed using any program verification tool like [16, 8, 10, 13] and is outside of the scope of this paper.

In the following, given a problem $\phi$, our goal is to find a $k > 0$ such that $R_k(\phi)$ is verified. To do so, for every function $f$ that is called in $\phi$ we compute
independently a $k_f > 0$ such that for all instantiations $\sigma$ of $f(x_1, \dots, x_n)$ there exists an abstraction function $\alpha$ on $A_{k_f}$ such that

$$ \alpha(f(\sigma(x_1), \dots, \sigma(x_n))) = f(\alpha(\sigma(x_1)), \dots, \alpha(\sigma(x_n))). $$

If $f$ does not rely on the polymorphic equality then TFF ensures that this property holds for $\alpha$ with $k = 1$. Instead, if $f$ uses polymorphic equality directly, we propose to analyse the code of the function to derive such a number of constants $k$ if it exists. In the following section we first define the programming language and its semantics.

# 4 The programming language

We define a polymorphic functional first-order language with polymorphic equality and we define a call-by-value small-step semantics for this language.

## 4.1 Syntax

In the following, we write $\bar{t}$ for the tuple $(t_1, \dots, t_n)$ when $n$ is clear from the context.

**Definition 1 (Types).** We write $TVar$ for a set of type variables, written $X, Y, Z, \dots$ Let ADT be a fixed finite set of ADT type names, written $\theta_1, \theta_2, \dots$, where every $\theta \in \text{ADT}$ is associated with an arity $a(\theta) \ge 0$. The **types** $\tau$ are defined by: $\tau ::= \text{Bool} \mid X \mid \theta(\bar{\tau})$. We write **Type** for the set of types.

**Definition 2.** A **type declaration** $D_{\text{types}}$ is a set of ADT definitions, where every ADT symbol $\theta$ has one definition: $\theta(\bar{Y}) = C_1 \text{ of } \bar{\psi}_1 \mid \dots \mid C_m \text{ of } \bar{\psi}_m$, where

- The $C_j$ are **ADT constructors** associated with an arity $a(C_j) \ge 0$. All ADT constructors that appear in $D_{\text{types}}$ must be distinct. We write $\text{Constr}(\theta)$ for $\{C_1, \dots, C_m\}$ and $\text{Constr}$ for $\bigcup_{\theta \in \text{ADT}} \text{Constr}(\theta)$.

- $\psi_i^j \in \text{Type}$, and $TVar(\psi_i^j) \subseteq \{Y_1, \dots, Y_{a(\theta)}\}$. We write $\text{sig}(C_j) = \bar{\psi}_j \to \theta(\bar{Y})$ for the signature of $C_j$.

In the following we consider a fixed type declaration $D_{\text{types}}$.

**Definition 3 (Terms).** Let $\mathcal{F}$ be a fixed finite set of function symbols, where every $f \in \mathcal{F}$ is associated with an arity $a(f) \ge 0$. The syntax of the terms (which depends on $D_{\text{types}}$) is the following.

$$ t ::= x \mid \text{true} \mid \text{false} \mid \textbf{if} t_1 \textbf{ then } t_2 \textbf{ else } t_3 \mid (t_1 = t_2) \mid C(\bar{t}) \mid f(\bar{t}) \mid \textbf{match} t \textbf{ with } C_1(\bar{y}) \Rightarrow t_1, \dots, C_m(\bar{y}) \Rightarrow t_m $$

where $C \in \text{Constr}$, $y_i$ are distinct variables and there exists $\theta \in \text{ADT}$ such that $\text{Constr}(\theta) = \{C_1, \dots, C_m\}$. We write **Term** for the set of terms. We also write
**match t with** {$C_j(\bar{y}) \Rightarrow t_j$}$_{j=1}^m$ for **match t with** $C_1(\bar{y}) \Rightarrow t_1, \dots, C_m(\bar{y}) \Rightarrow t_m$. The only variable binder in the terms is **match t with** {$C_j(\bar{y}) \Rightarrow t_j$}$_{j=1}^m$, which binds $y_1, \dots, y_{a(C_j)}$ in $t_j$. For any $t \in \mathcal{Term}$ we write $FV(t)$ for the set of all free variables of t.

**Definition 4 (Function declaration).** A function declaration $D_{fun}$ is a set of function definitions, where every function symbol $f \in \mathcal{Fun}$ has one definition:

$$f(x_1 : \tau_1, \dots, x_{a(f)} : \tau_{a(f)}) : \tau = d_f$$

where $x_j$ are distinct variables, $\tau_j, \tau \in \mathcal{Type}$ are respectively the input and output types of $f$, $d_f \in \mathcal{Term}$ is the body of $f$ and $FV(d_f) \subseteq \{x_1, \dots, x_{a(f)}\}$. The **signature** of $f$ w.r.t $D_{fun}$ is $\text{sig}(f) = \tau_1 \times \dots \times \tau_{a(f)} \to \tau$.

Type variables range over all types in our language. Since our language is first-order and does not contain abstract types, then all types admit equality. Two values of the same type are considered equal iff they are **structurally equal**.

**Definition 5.** A declaration is the pair $D = (D_{types}, D_{fun})$ of a type declaration $D_{types}$ and a function declaration $D_{fun}$. It defines both algebraic data types and functions.

*Example 2.* The declaration $D = (D_T, D_F)$ defines the function mem:

$$D_T: \text{list}(Y) = \text{Nil} \text{ of } () \mid \text{Cons of } (Y, \text{list}(Y))$$

$$D_F: \text{mem}(x: X, l: \text{list}(X)) : \text{Bool} =$$

**match l with**

$$\text{Nil}() \Rightarrow \text{false},$$

$$\text{Cons}(y, l') \Rightarrow \text{if } (x = y) \text{ then } \text{true} \text{ else } \text{mem}(x, l')$$

**Definition 6.** A **substitution** (resp. **type substitution**) is a mapping from variables (type variables) to terms (types). The substitution $\sigma$ that maps $x$ to $t$ is written $\{t/x\}$. The term $u$ where all free occurrences of $x$ are replaced with $t$ is written $u\{t/x\}$ or $\sigma(u)$. We write $\{\bar{t}/\bar{x}\}$ for the substitution that maps $x_i$ to $t_i$ for all $i$.

In the following we only consider substitutions whose images do not contain free variables that are bound in any term that we consider.

## 4.2 Typing rules

**Definition 7 (Typing rules).** A type instantiation $\Sigma$ is a type substitution whose images are ground types. A type environment $\Gamma$ is a mapping from term variables to types. The typing relation $\vdash_D$ w.r.t a global declaration $D$ (or simply $\vdash$ when $D$ is clear) is inductively defined as follows:
$$
\begin{align*}
\frac{\Gamma(x) = \tau}{\Gamma \vdash_D x : \tau} \quad \frac{\Gamma \vdash_D \text{true} : \text{Bool}}{\Gamma \vdash_D \text{false} : \text{Bool}}
& \qquad \frac{\Gamma \vdash_D t_1 : \text{Bool} \quad \Gamma \vdash_D t_2 : \tau \quad \Gamma \vdash_D t_3 : \tau}{\Gamma \vdash_D \text{if } t_1 \text{ then } t_2 \text{ else } t_3 : \tau} \\
& \qquad \frac{\Gamma \vdash_D t_1 : \tau \quad \Gamma \vdash_D t_2 : \tau}{\Gamma \vdash_D (t_1 = t_2) : \text{Bool}} \\
& \qquad \frac{\frac{\text{sig}(f) = \bar{\tau} \to \tau \quad \forall i. \Gamma \vdash_D t_i : \tau_i \Sigma}{\Gamma \vdash_D f(t_1, \dots, t_n) : \tau \Sigma}}{\text{sig}(C) = \bar{\psi} \to \theta \quad \forall i. \Gamma \vdash_D t_i : \psi^i \{\bar{\tau}/\bar{Y}\}} \tag{1} \\
& \qquad \frac{\Gamma \vdash_D t : \theta(\bar{\tau}) \quad \text{Constr}(\theta) = \{C_1, \dots, C_m\} \quad \forall j. \Gamma[y_i \mapsto \psi_j^i \{\bar{\tau}/\bar{Y}\}]_{i=1}^n \vdash_D t_j : \tau'}{\Gamma \vdash_D \text{match } t \text{ with } \{C_j(\bar{y}) \Rightarrow t_j\}_{j=1}^m : \tau'} \tag{2}
\end{align*}
$$

(1) For all ADTs $\theta$ whose input type variables $\bar{Y}$ are instantiated with $\bar{\tau}$, in order to type $C(\bar{t})$ as $\theta(\bar{\tau})$, all $t_i$ must be typed as the type of the ith parameter of the constructor C, instantiated with $\bar{\tau}$.

(2) In order to type a pattern-matching of a term $t$ of type $\theta(\bar{\tau})$ with type $\tau'$, every branch $t_j$ must be typed as $\tau'$ once the variables $y_i$ representing the arguments of the constructor have been instantiated according to the signature of the constructor and the type instantiation $\bar{\tau}$.

A function definition is *well formed* if for all $f \in \mathcal{F}un$ of signature $\bar{\tau} \to \tau$, $[x_1 \mapsto \tau_1, \dots, x_{a(f)} \mapsto \tau_{a(f)}] \vdash_D d_f : \tau$. In the following, we assume that all function definitions in $D_{fun}$ and $D$ are well-formed.

## 4.3 Small-step operational semantics

Values are the result of the execution of a function. Unlike usual small-step semantics, our values may contain variables. This will be used, in the following, for building symbolic execution trees of functions with unknown input values. A global declaration $D$ defines a set of **partial values**. Since partial values may contain typed variables, they also depend on a type environment $\Gamma$. Given $D$ and $\Gamma$, a term $t$ is a partial value belonging to $\mathcal{V}_{\tau}$ if $\Gamma \vdash_D t \in \mathcal{V}_{\tau}$, which is defined as follows.

**Definition 8 (Partial values and values).** The relation $\Gamma \vdash_D t \in \mathcal{V}_{\tau}$ that defines the set of partial values is inductively defined by:

$$
\frac{\overline{\Gamma \vdash_D \text{true} \in \mathcal{V}_{\text{Bool}}} \quad \overline{\Gamma \vdash_D \text{false} \in \mathcal{V}_{\text{Bool}}} \quad \frac{\Gamma(x) = \tau}{\Gamma \vdash_D x \in \mathcal{V}_{\tau}}}{\forall i. \Gamma \vdash_D v_i \in \mathcal{V}_{\psi^i \{\bar{\tau}/\bar{Y}\}} \quad \text{sig}(C) = \bar{\psi} \to \theta(\bar{Y})} \quad \Gamma \vdash_D C(\bar{v}) \in \mathcal{V}_{\theta(\bar{\tau})}
$$

$\mathcal{V}_{\tau}$ is the set of terms $t$ such that there exists a type environment $\Gamma$ such that $\Gamma \vdash_D t \in \mathcal{V}_{\tau}$. The set of partial values $\mathcal{V}$ is the union of the $\mathcal{V}_{\tau}$ for all types $\tau$. **Values** are ground partial values.

Example 3. `Nil()` is a value, `v = Cons(x, Cons(x, l))` is a partial value, with `[x ↦ X, l ↦ list(X)] \vdash_D v : list(X)`, and `mem(x, l)` is not a partial value.
We define a small-step semantics relation $\rightarrow$ for our language as follows. We write $t, t_i$ for terms and $v, v_i$ for partial values. The semantic rules are standard and call-by-value, except for conditionals and pattern-matching where the conditions/patterns are fully evaluated and resolved before evaluating any branch. The relation $\equiv_{\mathcal{T}_{\text{term}}}$ is the structural equality on ground terms.

$$ \frac{t \rightarrow t'}{\text{if } t \text{ then } t_1 \text{ else } t_2 \rightarrow \text{if } t' \text{ then } t_1 \text{ else } t_2} $$

$$ \frac{\text{if true then } t_1 \text{ else } t_2 \rightarrow t_1 \quad \text{if false then } t_1 \text{ else } t_2 \rightarrow t_2}{\text{if true then } t_1 \text{ else } t_2 \rightarrow t_1} $$

$$ \frac{t_i \rightarrow t'_i}{C(v_1, \dots, v_{i-1}, t_i, \dots, t_n) \rightarrow C(v_1, \dots, v_{i-1}, t'_i, \dots, t_n)} $$

$$ \frac{t_i \rightarrow t'_i}{f(v_1, \dots, v_{i-1}, t_i, \dots, t_n) \rightarrow f(v_1, \dots, v_{i-1}, t'_i, \dots, t_n)} \quad \overline{f(v) \rightarrow d_f \{v/x\}} $$

$$ t \rightarrow t' $$

$$ \frac{\text{match } t \text{ with } \{C_j(\bar{y}) \Rightarrow t_j\}_{j=1}^m \rightarrow \text{match } t' \text{ with } \{C_j(\bar{y}) \Rightarrow t_j\}_{j=1}^m}{\text{Constr}(\theta) = \{C_1, \dots, C_m\}} $$

$$ \text{Constr}(\theta) = \{C_1, \dots, C_m\} $$

$$ \frac{\text{match } C_i(\bar{v}) \text{ with } \{C_j(\bar{y}) \Rightarrow t_j\}_{j=1}^m \rightarrow t_i \{\overline{v/y}\}}{t_1 \rightarrow t'_1} $$

$$ \frac{t_1 \rightarrow t'_1}{(t_1 = t_2) \rightarrow (t'_1 = t_2)} \quad \frac{t_2 \rightarrow t'_2}{(v_1 = t_2) \rightarrow (v_1 = t'_2)} $$

$$ \frac{FV(v_1) = FV(v_2) = \emptyset \quad v_1 \neq \tau_{\text{term}} v_2}{(v_1 = v_2) \rightarrow \text{false}} \quad \frac{FV(v_1) = FV(v_2) = \emptyset \quad v_1 = \tau_{\text{term}} v_2}{(v_1 = v_2) \rightarrow \text{true}} $$

Again, note that our semantics operates on partial values that may contain variables. For example

$$ \textbf{match } \mathit{Pair}(x_1, x_2) \textbf{ with } \mathit{Pair}(y_1, y_2) \Rightarrow y_1 \rightarrow x_1 $$

As a consequence not all normal forms are (partial) values (e.g., **if x then y else z** and ($x = x$) are normal forms but not partial values).

# 5 Abstracting polymorphic atoms

We extend our language to abstract types and terms, and we define abstraction functions. Our concrete domain is the instance of the type variable $X$, and our abstract domain is $A_k$ for some $k$, a finite type with $k$ constants.

**Definition 9 (Abstract types and terms).** The abstract types $\tau^\sharp$ are defined as the following: $\tau^\sharp ::= A_k | \mathit{Bool} | X | \theta_i(\tau^\sharp_1, \dots, \tau^\sharp_{a(\theta_i)})$, where $k > 0$, and $A_k$ is the type of the $k$ constants $A_1, \dots, A_k$. By adding the constant terms $A_i$ to our language we obtain a set $\mathcal{T}_{\text{term}}^\sharp$ of abstract terms.
We extend the relation $\rightarrow$ to $Term^\sharp \times Term^\sharp$ by adding the following rules:

$$ \frac{\overline{(A_j = A_j) \rightarrow true}}{\overline{(A_j = A_i) \rightarrow false}} \qquad i \neq j $$

We now define the abstraction functions $\alpha$ used to map the values of type $\mathbb{C}$ (instantiating the polymorphic type $X$ of the program) to values of type $A_k$.

**Definition 10 (Abstraction function on atoms).** An abstraction function is a function $\alpha : \mathbb{C} \rightarrow A_k$ where $\mathbb{C}$ is any ground type. An element of the concrete domain $\mathbb{C}$ is called an **atom**.

We often need to apply $\alpha$ to all atoms that appear in some term (e.g. all elements of a list of $\mathbb{C}$). To do so, we first annotate each subterm $t$ of every function body with its type (written $t.type$). When a term $t$ is instantiated by some $\sigma$, its type annotation stays unchanged: $\sigma(t).type = t.type$. This way, even if $\sigma$ instantiates $t$ on a type $\tau$ that is also used in the program, we can still discriminate the terms that contain an atom and the ones that do not. Now, we extend $\alpha$ to the function $\alpha^*$ which takes as input an annotated term $t$.

**Definition 11 (Abstraction function on terms).** An abstraction function on terms is a function $\alpha^* : Term \rightarrow Term^\sharp$, where

- $\alpha^*(t) = t$ if $t.type$ is a ground type.

- $\alpha^*(y) = y$ if $y \in \mathcal{V}ar$.

- $\alpha^*(t) = \alpha(t)$ if $t$ is a ground term and $t.type = X$, where $X$ is the unique type variable appearing in all function signatures. This means that $t$ is an atom.

- $\alpha^*(C(t_1, \dots, t_n)) = C(\alpha^*(t_1), \dots, \alpha^*(t_n))$ if $C \in \text{Constr}$.

- $\alpha^*(f(t_1, \dots, t_n)) = f(\alpha^*(t_1), \dots, \alpha^*(t_n))$ if $f \in \mathcal{F}un$.

- $\alpha^*(\mathbf{if} t_1 \mathbf{then} t_2 \mathbf{else} t_3) = \mathbf{if} \alpha^*(t_1) \mathbf{then} \alpha^*(t_2) \mathbf{else} \alpha^*(t_3)$.

- $\alpha^*(\mathbf{match} t \mathbf{with} \{C_j(\bar{y}) \Rightarrow t_j\}_{j=1}^m, \tau) = \mathbf{match} \alpha^*(t) \mathbf{with} \{C_j(\bar{y}) \Rightarrow \alpha^*(t_j)\}_{j=1}^m$

In the following we suppose that all terms are implicitly annotated as soon as the functions are defined, and $\alpha^*(t)$ is always well defined.

In Section 2, to prove the reduction of $\forall X.\phi_1[X]$ to $\phi_1[A_1]$ we used the properties provided by Theorems For Free [17] for some functions. In general, when a function $f$ is first-order, i.e., $f$ does not take a function as an argument, the TFF of $f$ can be written as follows: for all types $\mathbb{C}$ and $A$, for all $\alpha : \mathbb{C} \rightarrow A$, $\alpha^* \circ f = f \circ \alpha^*$. In particular, when instantiating $A$ with our one-constant abstract domain $A_1$, TFF yields the following proposition for our language.

**Proposition 1.** Let $f$ be a polymorphic function (without equality). For all types $\mathbb{C}$, for the abstraction function $\alpha : \mathbb{C} \rightarrow A_1$ and for all instantiations $\sigma$ on $\mathbb{C}$, if $f(\sigma(\bar{x})) \rightarrow^* v$ for some $v \in \mathcal{V}$ then $f(\alpha^*(\sigma(\bar{x}))) \rightarrow^* \alpha^*(v)$.

As a consequence, given a first-order polymorphic function $f$, the task of automatically finding a locally complete abstract domain (i.e., a number of constants) for $f$ is simple when $f$ does not use the polymorphic equality. In this case the domain $A_1$ of 1 constant is complete. The difficulty comes when $f$ is allowed to compare atoms. This is the topic of the following sections.
# 6 Evaluation trees

Our goal here is to automatically compute the "number of constants" for a function $f$, that is, the smallest $k > 0$ such that for all well-typed inputs $t$ of $f$, there exists an abstraction function $\alpha$ on the abstract domain $A_k$ such that $\alpha^*(f(t)) = f(\alpha^*(t))$. To do so, we symbolically compute all evaluation paths resulting of calls to $f$ on any input values. The evaluation tree of $f$ is the tree of all these small-step evaluation paths. Each term $t$ in the tree is associated with a constraint $E$ containing all the equalities and inequalities between variables that need to be true in order to reach this node. Given the evaluation tree of $f$, the number of constants of $f$ is the smallest $k$ such that all constraints in the tree can be satisfied by a mapping from variables to elements of abstract domain $A_k$.

**Definition 12.** The Evaluation Tree (ET) of a term $t_0 \in \mathcal{Term}$ is a tree $ET(t_0)$ where the nodes are of the form $t \parallel E$ where $t \in \mathcal{Term}$ and $E$ is a constraint. A constraint is a finite set of assertions of the form $x = y$ or $x \neq y$, with $x, y \in \mathcal{Var}$. We write $N_1 \stackrel{l}{\to} N_2$ when the node $N_2$ is a child of the node $N_1$, and the edge between $N_1$ and $N_2$ has the label $l$.

In an evaluation tree, we have an edge between a node $t_1 \parallel E_1$ and $t_2 \parallel E_2$ if, by symbolically evaluating $t_1$ under constraint $E_1$ w.r.t. the small-step semantics (section 4.3), we obtain $t_2$ with constraint $E_2$. Such a symbolic evaluation may be non-deterministic. To define edges in evaluation tree, we first define critical positions, i.e., the position in $t_1$ where a reduction may occur to generate a possible $t_2$.

**Definition 13 (Position).** Let $\varepsilon$ be the empty word and $\cdot$ the concatenation operation on $\mathbb{N}^*$. A position in a term $t \in \mathcal{Term}$ is a sequence of integers pointing to a subterm of $t$. It is defined by:

$$
\begin{array}{l@{\qquad}l}
t|_{\varepsilon} = t & C(\bar{t})|_{i \cdot p} = t_i|_p \\
\mathbf{if} \ t \ \mathbf{then} \ t_1 \ \mathbf{else} \ t_2|_{0 \cdot p} = t|_p & (t_1 = t_2)|_{1 \cdot p} = t_1|_p \\
\mathbf{if} \ t \ \mathbf{then} \ t_1 \ \mathbf{else} \ t_2|_{1 \cdot p} = t_1|_p & (t_1 = t_2)|_{2 \cdot p} = t_2|_p \\
\mathbf{if} \ t \ \mathbf{then} \ t_1 \ \mathbf{else} \ t_2|_{2 \cdot p} = t_2|_p & \mathbf{match} \ t \ \mathbf{with} \ \{C_j(\bar{y}) \Rightarrow t_j\}_{j=1}^m|_{0 \cdot p} = t|_p \\
f(\bar{t})|_{i \cdot p} = t_i|_p & \mathbf{match} \ t \ \mathbf{with} \ \{C_j(\bar{y}) \Rightarrow t_j\}_{j=1}^m|_{i \cdot p} = t_i|_p
\end{array}
$$

The term $t$ where the subterm at the position $p$ is replaced by the term $u$ is written $t[u]_p$.

**Definition 14.** The critical position $CP(t)$ of a term $t$ is the position of the deepest subterm of $t$ that needs to be reduced by $\to$ in order for the evaluation of $t$ to progress. It is only defined for terms that are not partial values. $CP(t)$ is defined as follows, where $u \in \mathcal{Term} \setminus \mathcal{V}$, $t, t_i \in \mathcal{Term}$ and $v, v_i \in \mathcal{V}$:

$$
\begin{align*}
CP(\mathbf{if} \ u \ \mathbf{then} \ t_1 \ \mathbf{else} \ t_2) &= 0 \cdot CP(u) & CP(\mathbf{if} \ v \ \mathbf{then} \ t_1 \ \mathbf{else} \ t_2) &= \varepsilon \\
CP(\mathbf{match} \ u \ \mathbf{with} \ \{C_j(\bar{y}) \Rightarrow t_j\}_{j=1}^m) &= 0 \cdot CP(u) & CP(u = t) &= 1 \cdot CP(u) \\
CP(\mathbf{match} \ v \ \mathbf{with} \ \{C_j(\bar{y}) \Rightarrow t_j\}_{j=1}^m) &= \varepsilon & CP(v_1 = u) &= 2 \cdot CP(u) \\
CP(C(v_1, \dots, v_{i-1}, u, t_{i+1}, \dots, t_n)) &= i \cdot CP(u) & CP(v_1 = v_2) &= \varepsilon \\
CP(f(v_1, \dots, v_{i-1}, u, t_{i+1}, \dots, t_n)) &= i \cdot CP(u) & CP(f(v_1, \dots, v_n)) &= \varepsilon
\end{align*}
$$
**Definition 15 (Edges of an ET).** The outgoing edges of any node $t \parallel E$ are defined as follows (all cases are mutually exclusive).

- If $t \to t'$, then $t \parallel E \stackrel{\emptyset}{\to} t' \parallel E$.

- If $t|_{CP(t)} = \mathbf{if} \ x \ \mathbf{then} \ t_1 \ \mathbf{else} \ t_2$ with $x \in \mathcal{V}ar$, then

• $t \parallel E \underset{\to}{x:\mathbf{true}} (t[t_1]_{CP(t)})\{\mathbf{true}/x\} \parallel E$

• $t \parallel E \underset{\to}{x:\mathbf{false}} (t[t_2]_{CP(t)})\{\mathbf{false}/x\} \parallel E$

- If $t|_{CP(t)} = \mathbf{match} \ x \ \mathbf{with} \ \{C_j(\bar{y}) \Rightarrow t_j\}_{j=1}^m$ with $x \in \mathcal{V}ar$, then for all $j \in [1, m]$,

• $t \parallel E \underset{\to}{x:C_j(\bar{z})} (t[t_j\{\bar{z}/\bar{y}\}]_{CP(t)})\{C_j(\bar{z})/x\} \parallel E$, where $z_i$ are fresh variables,

- If $t|_{CP(t)} = (x = y)$ with $x, y \in \mathcal{V}ar$, then

• $t \parallel E \underset{\to}{x=y} t[\mathbf{true}]_{CP(t)} \parallel E \cup \{x = y\}$

• $t \parallel E \underset{\to}{x \neq y} t[\mathbf{false}]_{CP(t)} \parallel E \cup \{x \neq y\}$

$ET(t_0)$ is the tree built with $\to$, starting from the root node $t_0 \parallel \emptyset$. We write $ET(t \parallel E)$ for the tree built with $\to$, starting from the root node $t \parallel E$.

Note that evaluation trees are not defined for programs that compare two non-atomic terms with the polymorphic equality, e.g., $(\mathit{Cons}(x_1, l_1) = \mathit{Cons}(x_2, l_2))$ or $(l_1 = l_2)$ with $\vdash l_1 : \mathit{list}(X), \vdash l_2 : \mathit{list}(X)$. In the following, to simplify the presentation of evaluation trees, we compress paths of the form $N_1 \stackrel{\emptyset}{\to} N_2 \stackrel{l}{\to} N_3$ with $l \neq \emptyset$ into $N_1 \stackrel{l}{\to} N_3$, e.g., edges corresponding to the unfolding of a function definition or resolution of a trivial if-then-else are abstracted away.

**Example 4.** Consider the declaration $D = (D_T, D_F)$ with:

$D_T: \mathbf{Tuple}(X) = \mathit{None} \ \mathbf{of} \ () \mid \mathbf{Triple} \ \mathbf{of} \ (X, X, X)$

$D_F: \mathit{not}(b : \mathbf{Bool}) : \mathbf{Bool} = \mathbf{if} \ b \ \mathbf{then} \ \mathbf{false} \ \mathbf{else} \ \mathbf{true}$

$\mathit{allDiff}(t : \mathbf{tuple}(X)) : \mathbf{Bool} = \mathbf{match} \ t \ \mathbf{with}$

$\mathit{None()} \Rightarrow \mathbf{true},$

$\mathbf{Triple}(x, y, z) \Rightarrow \mathbf{if} \ (x = y) \ \mathbf{then} \ \mathbf{false} \ \mathbf{else}$

$\mathbf{if} \ (x = z) \ \mathbf{then} \ \mathbf{false} \ \mathbf{else} \ \mathit{not}(y = z)$

The evaluation tree of function `allDiff` is given in Fig. 1.

Evaluation trees are finitely branching, but their depth may be infinite even when $f$ terminates. Thus a naive exploration may not terminate. We will see later, in Section 7, how to finitely represent and explore such unbounded trees.

From the evaluation tree of a function, we can infer the number of constants necessary to completely abstract the evaluation of this function. We call this number a *model*. A substitution $\sigma : \mathcal{V}ar \to \mathbb{C}$ satisfies a set of constraints $E$, written $\sigma \models E$ if for all $x \sim y \in E$ (with $\sim \in \{=, \ne\}$), $\sigma(x) \sim \sigma(y)$ is true.
<figure><img src="image_2.png" /><figcaption>Fig. 1. Evaluation tree for the function allDiff</figcaption></figure>

**Definition 16 (Model).** Let $E$ be a constraint. A number of constants $k > 0$ is a model of $E$ if for all types $\mathcal{C}$ and for all $\sigma : \mathcal{Var} \to \mathcal{C}$ such that $\sigma \models E$, there exists $\alpha : \mathcal{C} \to \mathcal{A}_k$ such that $\alpha \circ \sigma$ satisfies $E$. This is written $k \models E$. We write $\mathcal{M}(E)$ for the smallest $k$ such that $k \models E$.

Given a function $f \in \mathcal{F}un$ and $ET(f(\bar{x}))$ its execution tree, we write $\mathcal{M}(f)$ for the maximum of all the $\mathcal{M}(E)$ for all constraints $E$ in $ET(f(\bar{x}))$.

**Lemma 2.** Models can be over-approximated, i.e., if $k \ge k' > 0$ and $k' \models E$ then $k \models E$.

*Proof.* Ignore the constants $A_{k'+1}, \dots, A_k$ when choosing $\alpha$.

For instance, in Fig. 1, $k=3$ is a model of all the constraints but $k=2$ is not since $2 \not\models \{x \neq y, x \neq z, y \neq z\}$. However, evaluation trees are not always finite, as the one for function *allDiff*. When evaluation trees are not finite, we need a finite representation of such evaluation trees to perform the same reasoning.

*Example 5.* Consider the declaration *D* in Example 2. The ET of the function *mem* is represented in Fig. 2.

# 7 Folding evaluation trees

Given an evaluation tree, our goal is to find a model, i.e. a finite number of constants that satisfies the constraints of all the nodes of the tree. Since an ET may be unbounded, we need a finite representation of the tree to collect all
<figure><img src="image_3.png" /><figcaption>**Fig. 2.** Evaluation tree for the function mem</figcaption></figure>

the possible constraints and infer (or over-approximate) this model. The finite representation is called a Folded Evaluation Tree (Section 7). Folded Evaluation Trees are ETs where we identify some nodes and, thus, fold a part of the tree. In practice, when we consider a node $t \parallel E$ during the breadth-first exploration of the ET, we search for another node $\hat{t} \parallel \hat{E}$ already encountered such that $t$ is unifiable with $\hat{t}$, and $E$ “does not add any relevant assertions compared to” $\hat{E}$. If such a node exists, then we say that those two nodes **match** (Section 7.3), i.e., exploring $t \parallel E$ would not provide us any additional information compared to the exploration of $\hat{t} \parallel \hat{E}$. Deciding that $E$ does not add any relevant assertions w.r.t. $\hat{E}$ is done, formally, using a specific representation of inequality constraints as graphs, called **star forests** (Section 7.2).

**Example 6.** In the ET of mem (Fig. 2), consider the nodes $\hat{N} = mem(x, l_1) \parallel \{x \neq y_1\}$ and $N = mem(x, l_2) \parallel \{x \neq y_1, x \neq y_2\}$. $mem(x, l_1)$ and $mem(x, l_2)$ are equal up to a variable renaming. Their subtrees thus have a similar shape. Moreover from $\hat{N}$ to $N$ the only new assertion is $x \neq y_2$, which does not increase the minimal model. Indeed, $M(\{x \neq y_1, x \neq y_2\}) = M(\{x \neq y_1\}) = 2$. In fact, if we keep exploring $N$, we only find constraints such as $\{x \neq y_1, x \neq y_2, x \neq y_3\}$, $\{x \neq y_1, x \neq y_2, x \neq y_3, x \neq y_4\}$, etc. whose minimal model is still 2. We thus can safely cut the exploration of the node $N$ and assert that $N$ matches $\hat{N}$. Once this is done, there is no node left to explore. We compute a model for every constraint in the tree and return the biggest one, which would be 2.

## 7.1 Folded Evaluation Trees

A **Folded Evaluation Tree** (FET) of a term $t$ (written $FET(t)$) is a finite subtree of $ET(t)$ with the same root as $ET(t)$, along with a binary **folding** relation $\rightarrow$ between nodes such that:
- $\dasharrow$ is acyclic, i.e. there is no node $N$ such that $N \dasharrow^* N$.

- If $N \dasharrow \hat{N}$ then $N$ has no children.

- For all nodes $N$ in the FET, there exists at most one node $\hat{N}$ such that $N \dasharrow \hat{N}$.

- For a node $N \in \text{FET}(t)$, if there is no outgoing $\dasharrow$ from $N$ (i.e. $N$ is not a folded node), then $N$ has the same children in $\text{FET}(t)$ and in $\text{ET}(t)$.

In the following we describe the criterion for correctly folding the nodes of an
evaluation tree, and the algorithm which computes a model of a given function
(Section 7.4).

## 7.2 Constraints as star forests

Intuitively, a star is a graphical representation of a collection of constraints
{$x \neq y_1, x \neq y_2, \dots$} where one variable $x$ (the center of the star) appears in all
inequality constraints. To justify the focus on this type of constraints, we first show
that equality constraints can be safely ignored. Let $E_{\sim} = \{(x \sim y) | (x \sim y) \in E\}$
with $\sim \in \{=, \neq\}$.

**Proposition 2.** For any constraint $E$, $\mathcal{M}(E) \leq \mathcal{M}(E_{\neq})$.

*Proof.* Let $\sigma$ such that $\sigma \models E$. Since $E_{\neq} \subseteq E$, then $\sigma \models E_{\neq}$. Therefore there exists $\alpha : \mathbb{C} \rightarrow \mathbb{A}_{\mathcal{M}(E_{\neq})}$ such that $\alpha \circ \sigma \models E_{\neq}$. Since $\sigma$ satisfies all equality assertions in $E$ and $\alpha$ is a function, then $\alpha \circ \sigma$ also satisfies all equality assertions in $E$. In other words, $\alpha \circ \sigma \models E_{=}$. Therefore $\alpha \circ \sigma \models E$, and $\mathcal{M}(E) \leq \mathcal{M}(E_{\neq})$.

We then represent the inequality assertions of a constraint by a graph whose
vertices are variables and whose edges are inequality assertions. If two variables $x$
and $y$ are not connected by an inequality $x \neq y$ then they possibly can be merged
by a specific instantiation $\sigma$ s.t. $\sigma(x) = \sigma(y)$. To model the instantiation of a
constraint $E$ by some $\sigma$ in the graph of $E$, we merge together the variables that
are given the same concrete value by $\sigma$. If $\sigma \models E$ then this merging operation is
only performed on vertices that do not share any edge. To account of the merging
operation, we define vertices as sets of variables. Before the merges, each vertex
is a singleton.

**Definition 17.** We write $G_E = (V_E, F_E)$ for the (undirected) **inequality graph** of $E$, where the set of vertices is $V_E = \{\{x\} | x \in \text{Var}(E)\}$ (vertices are sets of variables) and the set of edges is $F_E = \{\{\{x\}, \{y\}\} | (x \neq y) \in E\}$.

Merging two vertices $u$ and $v$ in such a graph replaces $u$ and $v$ with a new vertex $u \cup v$ whose set of neighbors in the graph is the union of the neighbors of $u$ and $v$. This operation may only be performed when $u$ and $v$ are not connected by an edge. We write $[x]_G$ for the vertex $u$ of $G$ such that $x \in u$. We write $G \rightsquigarrow G'$ if the graph $G'$ can be obtained from the graph $G$ by merging two vertices.

An instantiation $\sigma$ may merge vertices in a graph $G_E$ by giving the same
value to two distinct variables. If $\sigma \models E$, we write $G_E^\sigma$ for the graph obtained by
merging in $G_E$ the variables that are given the same value by $\sigma$.
Conversely, if $G_E \rightsquigarrow^* G$ then there exists an instantiation $\sigma : \mathcal{V}ar \to \mathbb{N}$ such that $\sigma \models E$, with $\sigma(x) = \sigma(y)$ iff $[x]_G = [y]_G$. To build $\sigma$, if $\{u_1, \dots, u_n\}$ are the vertices of $G$ then we define $\sigma$ as $\sigma(x) = i$, $i \in [1, n]$, if $x \in u_i$.

**Lemma 3.** If $G \rightsquigarrow^* G'$, then two vertices $u$ and $v$ are connected in $G'$ iff there exist $x \in u$ and $y \in v$ such that $[x]_G$ and $[y]_G$ are connected in $G$.

**Proposition 3.** For any constraint $E$, $\mathcal{M}(E_{\neq})$ is equal to the greatest $k$ such that $G_E$ can be merged into a $k$-complete graph, i.e., a graph with $k$ vertices such that for all vertices $u$ and $v$, $u$ and $v$ are connected.

*Proof. (sketch)* Let $k_{max}$ be the greatest $k$ such that $G_E$ can be merged into a $k$-complete graph. We show $\mathcal{M}(E_{\neq}) = k_{max}$.

- If $G_E \rightsquigarrow^* G$, where $G$ is $k_{max}$-complete, then we can define $\sigma : \mathcal{V}ar \to [1, k_{max}]$ such that $\sigma(x) = \sigma(y)$ iff $[x]_G = [y]_G$ and $\sigma \models E$ (see the above construction). Then there is no abstraction function $\alpha : i \in \mathbb{N} \to A_{k_{max}-1}$ such that $\alpha \circ \sigma \models E$ ($\sigma$ requires $k_{max}$ constants), thus $\mathcal{M}(E_{\neq}) \ge k_{max}$.

- Let $\sigma$ such that $\sigma \models E$. Starting from $G_E^\sigma$, arbitrary merges eventually lead to a $k$-complete graph $G$ for some $k$. By attributing one element of $A_k$ to every vertex of $G$ we obtain an abstraction function $\alpha$ such that $\alpha \circ \sigma \models E$. Since $k \le k_{max}$ and $\sigma$ is arbitrary, then $\mathcal{M}(E_{\neq}) \le k_{max}$.

$\mathcal{M}(E_{\neq})$ is not equal to the chromatic number of $G_E$. Indeed, it would be the case if we were to directly map variables to constants, but variables are instantiated before applying the abstraction function. For example, the graph in Figure 3 is 2-colorable, but if $\sigma(x) = \sigma(v)$ and $\sigma(y) = \sigma(w)$, then $\alpha$ requires 3 constants. We now focus on special graphs called *stars*, that naturally appear in the ET of many functions.

**Definition 18.** A *star* is an inequality graph whose vertices all have exactly one neighbor except for one vertex (called the center) whose degree is at least 1. A *star forest* is a graph whose connected components are all stars. If $G_E$ is a star forest then we write $\|E\|$ for its number of stars.

The graph in Fig. 3 is a star forest with $\|E\| = 2$. In the star on the left, $u$ is the center. In the star on the right, either $v$ or $w$ can be considered as the center. The interest of star graphs w.r.t. general graphs lies in the following result, which bounds the number of constants needed by any star forest.

<figure><img src="image_4.png" /><figcaption>**Fig. 3.** The inequality graph of the constraint $\{u \neq x, u \neq y, u \neq z, v \neq w\}$</figcaption></figure>
**Lemma 4.** For any constraint *E* whose graph is a star forest, $\mathcal{M}(E) \le \|E\| + 1$.

*Proof.* Suppose $\mathcal{M}(E) \ge \|E\| + 2$. Let $S_1, \dots, S_{\|E\|}$ be the stars of $E$, and let $\{c_i\}$ be the center of $S_i$. By Proposition 3 there exists a $\mathcal{M}(E)$-complete graph $G$ such that $G_E \rightsquigarrow * G$. There are $\|E\|$ star centers in $G_E$, and $G$ has $\mathcal{E} \ge \|E\| + 2$ vertices. As a consequence, there exist at least two vertices $u, v$ in $G$ that do not contain any $c_i$. Since $G$ is complete, $u$ and $v$ are connected in $G$. Therefore, by Lemma 3, there exist two variables $x \in u$ and $y \in v$ such that $\{x\}$ and $\{y\}$ are connected in $G_E$ $(\{x \ne y\} \in E)$. However, all edges in $G_E$ are connected to a star center. This contradicts the fact that neither $\{x\}$ nor $\{y\}$ are star centers.

As a consequence, if we are able to bound the number of stars in all descendants of an evaluation tree node, then we do not need to explore this node. This also requires that the constraints of all descendants of the node are star forests, which is not always the case.

## 7.3 Matching criterion

Here we formally describe what it means for two nodes in an evaluation tree to be "similar". To do so we introduce a matching relation between nodes such that every node in an evaluation tree matches at least one node in the "folded" finite version of that tree (if such version can be built).

A node $t \parallel E$ matches a node $\hat{t} \parallel \hat{E}$ if $t$ and $\hat{t}$ are equal up to a variable renaming, if $E$ and $\hat{E}$ are both star forests with the same number of stars, and if $E$ and $\hat{E}$ have the same star centers up to the renaming. As a consequence, the descendants of $t \parallel E$ match the descendants of $\hat{t} \parallel \hat{E}$ and this entails that $\hat{t} \parallel \hat{E}$ simulates $t \parallel E$.

**Definition 19 (Active variable, Stable stars).** A variable $x \in \mathcal{V}ar$ is active in a node $t \parallel E$ if $x \in \mathcal{F}V(t)$ and $x \in \mathcal{V}ar(E)$. Otherwise $x$ is inactive. A star $S$ in $E$ is stable if every non-center vertex of $S$ is inactive.

Given a node $N$, if $x$ is inactive in $N$, then it will never be part of additional constraints of children of $N$. This is illustrated in the following example.

*Example 7.* Consider the node $mem(x, l_1) \parallel \{x \neq y_1\}$ in the ET of mem (Fig. 2). $y_1$ does not appear in $mem(x, l_1)$ thus is inactive. In the descendants of this node some variables are introduced (representing the elements and sublists of $l_1$), but none of them are $y_1$. Thus $y_1$ will never appear again in the evaluated term, thus no new edge connecting $y_1$ will ever be added to the inequality graph.

**Definition 20 (Matching).** Let $t \parallel E$ and $\hat{t} \parallel \hat{E}$ be nodes in an evaluation tree. $t \parallel E$ matches $\hat{t} \parallel \hat{E}$ if

- $E$ and $\hat{E}$ are stable star forests, and

- $\|E\| = \|\hat{E}\|$ where $\|E\|$ is the number of stars of $E$, and

- there exists a bijective renaming $\mu: \mathcal{V}ar \to \mathcal{V}ar$ such that $\mu(t) = \hat{t}$ and for all $x \in \mathcal{V}ar$, $x$ is a star center in $E$ iff $\mu(x)$ is a star center in $\hat{E}$ (in other words, $E$ and $\hat{E}$ have the same star centers up to $\mu$).
In this case, we write $t \parallel E \sim_{\mu} \hat{t} \parallel \hat{E}$, or $t \parallel E \sim \hat{t} \parallel \hat{E}$ when $\mu$ is clear.

If needed, we rename the variables that are bound in the program, so that no variable shadowing may occur. As a consequence, since all variables introduced by our algorithm are fresh, if $\mu(t) = \hat{t}$ then $t$ and $\hat{t}$ have "the same semantics", i.e., applying $\mu$ to $t$ does not capture any additional variable.

## 7.4 The algorithm for analysing a function

Let $f \in \mathcal{F}un$ be a function such that for any instantiation $\sigma$, if $\sigma(f(\bar{x})) \to t$, then $t$ has no subterm of the form $(t_1 = t_2)$ (in other terms, $f$ does not use the polymorphic equality). The constraints in the ET of $f$ thus are all empty. As a consequence, $\mathcal{M}(f) = 1$. In general, inferring if the evaluation of a term can reach a polymorphic equality is hard. For each function $f \in D$, we build a set $B(f)$ that over-approximates the uses of polymorphic equality in $f$. If the over-approximation $B(f)$ is empty then executing $f$ cannot reach any polymorphic equality. The set $B(f)$ is defined as follows.

**Definition 21.** Let $D$ be a declaration and $f$ be a function symbol whose definition in $D$ is $f(x_1 : \rho_1, \dots, x_n : \rho_n) : \rho = d_f$. We write $B(f)$ for the smallest subset of $\mathcal{F}un \cup \{=\}$ such that:

- if there exists a position $p$ such that $d_f|_p = (t_1 = t_2)$ where the type of $t_1$ (and $t_2$) is open then $(=) \in B(f)$.

- if there exists a position $p$ such that $d_f|_p = g(\bar{t})$ and $B(g) \neq \emptyset$ then $g \in B(f)$.

If $B(f) = \emptyset$ then $f$ does not use the polymorphic equality. As a consequence, $f$ is parametric polymorphic and Proposition 1 guarantees that one constant is enough for $f$.

**Algorithm.**

*Input:* $f \in \mathcal{F}un$ a function name, and $D$ a global declaration.

*Output:* A number of constants $k$

(A) If $B(f) = \emptyset$ then the algorithm returns $k = 1$.

(B) Otherwise, we compute a FET of the term $f(\bar{x})$ (written $FET(f(\bar{x}))$) as follows. Starting from the root node $f(\bar{x}) \parallel \emptyset$, we explore the evaluation tree $ET(f(\bar{x}))$ with a breadth-first search. When we explore a node $N$ that matches another previously explored node $\tilde{N}$, we stop the exploration of $N$ without considering its children. In this case $N \dashrightarrow \tilde{N}$ ($N$ is folded to $\tilde{N}$). This computation succeeds iff it terminates, i.e. if $FET(t)$ is finite. In this case, consider the set $S$ of all constraints that appear in the nodes of $FET(f(\bar{x}))$. For every $E \in S$, we compute the number $\|E\| \ge 0$ of stars of $E$. The algorithm returns $k = \max \{\|E\| \mid E \in S\} + 1$. By Proposition 4, $\|E\| + 1 \models E$, therefore by Lemma 2, $k$ satisfies all constraints in $S$.

**Theorem 1 (Soundness of the algorithm).** If this algorithm returns $k > 0$ when given a function $f(\bar{x})$ as input, then for all types $\mathbb{C}$ and for all instantiations $\sigma$ of $f(\bar{x})$ on $\mathbb{C}$, there exists $\alpha : \mathbb{C} \to \mathbb{A}_k$ such that $\sigma(f(\bar{x}))$ and $\alpha$ commute.
## 8 Illustrating the algorithm on the mem function

Using the algorithm presented above, we can build the complete FET for the function mem, Fig. 4. This FET is a finite folding of the ET Fig. 2. On this FET we can check that we need a number of constants $k = 2$ for defining a complete abstraction function on mem. In the following, we denote

<figure><img src="image_5.png" /><figcaption>Fig. 4. Folded evaluation tree of the function mem</figcaption></figure>

by $\alpha_k$ an abstraction function with a domain of $k$ constants. Thus, we have (a) $\forall x \ l. \ \exists \alpha_k. \ mem(x, l) = mem(\alpha_k(x), \alpha_k^*(l))$ with $k = 2$. Assume that we have two additional parametric polymorphic functions: last and makelist. The function last: list(X) → list(X) returns the list containing the last element of the list if it is not empty and the empty list otherwise. The function makelist has type $X \times nat \rightarrow list(X)$ where nat is the ADT of natural numbers, i.e. in our language, nat = Zero of () | S of (nat). A call of the form makelist(x, i) returns a list with exactly i repetitions of x. Assume that we want to prove the property $\phi_3 \stackrel{def}{=}$ $\forall x \ i. \ mem(x, last(makelist(x, S(i))))$. Since last and makelist are polymorphic functions, from TFF we get that (b) $\forall \alpha \ l. \ \alpha^*(last(l)) = last(\alpha^*(l))$ and (c) $\forall \alpha \ x \ i. \ \alpha^*(makelist(x, i)) = makelist(\alpha(x), i)$. Note that using TFF, the $\alpha$ functions are quantified universally and do not depend on $k$. Besides, from the table of results of Timbuk [10], we know that the property $\phi_3$ is true for 2 arbitrary constants, i.e., $\phi_3[A_2] \stackrel{def}{=}$ $\forall x : A_2 \ i : nat. \ mem(x, last(makelist(x, S(i)))))$ holds. This implies that $\forall x \ i \ \alpha'_k. \ mem(\alpha'_k(x), last(makelist(\alpha'_k(x), S(i)))))$, where $\alpha'_k$ is any abstraction mapping values to $A_2$. Note that $k = 2$ is fixed but the quantification on $\alpha'_k$ is universal because, as explained in Section 2, (d) the
property $\phi_3[A_2]$ holds independently of the choice of the abstraction provided
that its domain has the same number of constants. This results into the following
chain of entailments:

$$
\begin{align*}
\phi_3[A_2] &\stackrel{\text{def}}{=} \forall x : A_2 \ i : \text{nat. mem}(x, \text{last}(\text{makelist}(x, S(i)))) \\
&\qquad \Downarrow \text{(d)} \\
&\qquad \forall x \ i : \alpha'_k. \text{mem}(\alpha'_k(x), \text{last}(\text{makelist}(\alpha'_k(x), S(i)))) \\
&\qquad \Downarrow \text{(b) and (c)} \\
&\qquad \forall x \ i. \ \alpha'_k. \text{mem}(\alpha'_k(x), \alpha'^*_{k}(\text{last}(\text{makelist}(x, S(i)))) \\
&\qquad \qquad \Downarrow \text{We choose } \alpha_k \text{ appearing in (a) for } \alpha'_k \\
&\qquad \forall x \ i. \ \exists \alpha_k. \text{mem}(\alpha_k(x), \alpha^*_{k}(\text{last}(\text{makelist}(x, S(i)))) \\
&\qquad \qquad \Downarrow \text{(a)} \\
\phi_3 &\stackrel{\text{def}}{=} \forall x \ i. \text{mem}(x, \text{last}(\text{makelist}(x, S(i))))
\end{align*}
$$

As a result, from the proof of $\phi_3$ specialised with $X = A_2$, we obtain a proof of
$\phi_3$ for any type $X$.

9 Combining function analyses

The algorithm above computes a model that is big enough to precisely abstract a single function. However, verification problems can state properties on several functions at the same time. Since the abstraction function of each function depends on its input value, we need a way to build a combined abstraction for all of them. For instance, consider a polymorphic problem $\forall l. P(f(l))$ where $P : list(X) \to \text{Bool}$ and $f : list(X) \to list(X)$. In the preconditions of the reduction theorem (Theorem 1), we need an abstraction function $\alpha$ that “commutes” with $P$ and $f$, i.e., we want $\forall l. \exists \alpha. P(f(l)) = P(f(\alpha^*(l)))$. Assume that our algorithm has successfully built complete abstractions $\alpha_1$ for $P$ and $\alpha_2$ for $f$, i.e., (1) $\forall l. \exists \alpha_1. P(l) = P(\alpha_1^*(l))$ and (2) $\forall l. \exists \alpha_2. \alpha_2^*(f(l)) = f(\alpha_2^*(l))$. By instantiating (1) with $f(l)$, we obtain $\exists \alpha_1. P(f(l)) = P(\alpha_1(f(l)))$ but we cannot apply commutativity between $f$ and $\alpha_1$ since it only holds for $\alpha_2$, and $\alpha_2$ may abstract values differently. In addition, we cannot check if $\alpha_1$ and $\alpha_2$ coincide because our algorithm only returns a number of constants, and not the abstraction function itself. Thus, as is, we cannot directly use our algorithm to reduce verification problems as a whole.

To analyse a whole verification problem $\phi$, we first run our algorithm on every
function that appears in $\phi$. For all positions $p$ such that $\phi|_p$ is a function call
$f(\bar{x})$, we obtain a number of constants $k_p$ that is the output of our algorithm
with input $f(\bar{x})$. Let $F_\phi$ be the set of all such positions for $\phi$. As a global number
of constants for $\phi$ we then choose $k_\phi \stackrel{\text{def}}{=} \prod_{p \in F_\phi} k_p$.

**Theorem 2 (Whole problem analysis).** Let $\phi$ be a verification problem. For all function call positions $p \in F_\phi$, if the model $k_p$ is finite then for all instantiations $\sigma$ of $\phi$ on some $C$, there exists $\alpha : C \to k_\phi$ such that $\sigma(\phi)$ and $\alpha$ commute.
An outline of the proof is given in Appendix B. The theorem that we actually prove is stronger than Theorem 2. It uses another definition of commutativity (called strong commutativity), which entails regular commutativity.

*Example 8.* Consider the verification problem $\phi \stackrel{def}{=} \neg mem(x, delete(x, l))$. Two function calls appear in $\phi$: a call to $\neg mem$ (which is written as a single function) and a call to *delete*. Our algorithm returns $k = 2$ for both functions $\neg mem$ and *delete*. We thus obtain the number of constants $k_{\phi} = 2 \times 2 = 4$ for the entire verification problem $\phi$.

# 10 Implementation and experiments

We propose an implementation of the algorithm presented in section 7. This implementation is written in the language OCaml and is around 3000 lines long. This implementation takes as input a program, i.e., definitions of polymorphic recursive ADTs and polymorphic functions with equality, written in a simple functional programming language. For a given function *f*, our analyser returns a number of constants $k \ge \mathcal{M}(f)$. The implementation with source of the examples is available in the supplementary material.

The algorithm works by first checking if *f* or any function accessible via a call from *f* uses the polymorphic equality primitive. If it is not the case we return 1. Otherwise we explore a FET for *f* with a breadth-first search. If this exploration terminates before reaching a bound (set to 100 nodes in our experiments), we return a *k* that satisfies all constraints in the FET. Otherwise the algorithm fails, meaning that either *f* requires an infinite number of constants, or the program is too complex for our analysis. Additionally, three optimisations of our algorithm are used in the implementation:

- The first optimisation splits the inequality graphs in the FET such that the inequality graph of every constraint is a stable star forest (which is the form required to fold the nodes).

- The second optimisation generalises the matching relation between nodes. It allows the term of the node that we are trying to fold to be wrapped in constructors and variables. For instance we fold $Cons(x, f(l)) \parallel \emptyset$ to $f(l) \parallel \emptyset$.

- The third optimisation also generalises the matching relation, specifically for functions that return a boolean. It allows some terms made of conditionals, booleans and function calls to match some other function calls. For instance we may fold **if f(x) then f(y) else f(z) || Ø to f(u) || Ø.** This pattern can be found e.g. in the ET of the function *eq_tree* that compares two binary trees.

More details about those optimisations can be found in Appendix A. The following table shows how our algorithm performs for some functions that use the polymorphic equality. The column "Minimal *k*" states the minimal *k* that is sufficient to completely abstract the function and the column "Our *k*" gives the value we obtain with our technique. The *mem_tree* function is membership on trees. The function *count* counts occurrences of an element in a list. The
sorted order. The 0-1 principle states that if the function correctly sorts booleans
(i.e. 0 and 1) then it also correctly sorts integers. Day & al. [7] show that
this result is a particular instance of TFF where the sorting function has type
∀X. ((X × X) → (X × X)) → list(X) → list(X). This result is, thus, limited to
sorting functions having this specific type. In comparison, our technique applies
to more general class of functions, possibly embedding polymorphic equalities. A
generalization to functions embedding a polymorphic comparison operator, like
sorting functions, is part of the future work.

Bernardy et al. [3] address the problem of testing the instances of a poly-
morphic function. They consider a more general class of polymorphic functions,
possibly higher-order, with polymorphic equality or comparison. They show how
to reduce testing of a polymorphic property of all input of a given size (e.g., lists
of length 3) to the test of a specific monomorphic instance (a list of integers of
length 3). Like usual testing techniques, their approach can only check that a
property holds for a subset of polymorphic instances. In particular, it cannot
*prove* that the property holds for all polymorphic instances, as we can.

Bruni et al. [5] introduce *locally complete* abstract interpretation. They first observe that the abstract domains (and abstraction functions) that are complete for *all* inputs are very limited for interesting programs. However, completeness can be achieved in a local way, that is, for *some* inputs only. Our analysis works with a similar notion of local completeness. However, the abstract domain that we automatically build is guaranteed to be locally complete for *all* inputs of the program. In our case, the abstract domain A is fixed but the abstraction function α may depend on the input of the function. A significant difference is that Bruni et al. consider imperative monomorphic programs, while we are interested in the verification of functional polymorphic programs with recursive ADTs.

The principle of polymorphic invariance [1] for analysing parametric polymor-
phic functions aims at determining when it is enough to analyse one instance of
a polymorphic function for a given property. More precisely, the goal is to show
that a property holds for one instance *if and only if* it holds for all instances—in
which case it suffices to analyse the simplest. This was shown to be the case
for strictness analysis whose simplest instance is the two-point abstract domain
that abstracts the integers. Our approach establishes polymorphic invariance
in a more constructive way because we compute an abstract domain of finite
cardinality for which it holds that if the property is verified for that abstract
domain then it holds for all concrete instances.

**12 Conclusion and further work**

*Conclusion* Given a polymorphic verification problem *φ* over functions manipulating ADTs, we propose a theorem that reduces the verification of *φ* to the verification of *φ*[A<sub>*k*</sub>], i.e., one of its instances on a finite set of *k* constants. For parametric polymorphic first-order functions, we observe that this reduction is always possible with 1 constant using TFF [17]. For functions using polymorphic equality, we propose an analysis (Section 7) of the function's code checking if this
reduction is possible. When the analysis succeeds on a function $f$, it provides a number $k \in \mathbb{N}$ and guarantees that for all input values $t$ there exists a complete abstraction function $\alpha : \mathbb{C} \mapsto \mathbb{A}_k$ such that $\alpha(f(t)) = f(\alpha(t))$. Furthermore, we show how to combine several complete abstraction functions (Section 9) in order to prove a collection of polymorphic verification problems (Section 10). For those problems, our implementation of the analysis successfully computes a number $k$ sufficient to reduce the problem $\phi$ to $\phi[\mathbb{A}_k]$, which is verifiable using off-the-shelf tools. To the best of our knowledge, this is the first use of complete abstract interpretation for analysing polymorphic functions.

*Further work* The computed size $k$ of the abstract domain is not always optimal. For instance, to analyse the function `common_elt`, three constants are enough: one constant for elements present in the intersection, one constant for elements occurring only in the first list and one for elements occurring only in the second list. However, the algorithm we propose is not able to infer that $k = 3$ is enough to have a complete abstraction.

In certain cases it is possible to refine the combination of abstractions presented here. For instance, to prove $\neg mem(x, delete(x, l))$, it is enough to use $k = 2$ constants though with our combination technique $k$ is 4 (2 constants for `mem` times 2 constants for `delete`). We do not have a general theory for obtaining the minimal number of constants required by a given polymorphic problem.

Another extension is to deal with polymorphic functions with polymorphic inequalities of the form $x < y$ (and not just $x \neq y$). We conjecture that it is possible to extend the Stars formalism to represent inequalities $x < y$ instead of $x \neq y$. Using this extension, our analysis should be able to compute a $k$ to reduce the verification of polymorphic problems with inequalities such as problems about polymorphic sorting functions.

Our technique should also be useful for disproving properties. Indeed, a corollary of our reduction theorem is that if there exists a counterexample to $\phi$ then there exists a counterexample to $\phi[\mathbb{A}_k]$. Exploiting this property would improve the search for a counterexample in tools such as Nitpick [4], by limiting to $k$ the size of the finite domains used for instantiating the type variable $X$ in the polymorphic problem $\phi$.
Bibliography

[1] Samson Abramsky. Strictness analysis and polymorphic invariance. In H. Ganzinger and N. Jones, editors, *On Programs as Data Objects*, pages 1–23. Springer Verlag, 1986.

[2] S. Bautista, T.P. Jensen, and B. Montagu. Lifting Numeric Relational Domains to Algebraic Data Types. In *SAS'22*, volume 13790 of LNCS, pages 104–134. Springer, 2022.

[3] J.-P. Bernardy, P. Jansson, and K. Claessen. Testing Polymorphic Properties. In *ESOP'10*, volume 6012 of LNCS, pages 125–144. Springer, 2010.

[4] J.-C. Blanchette and T. Nipkow. Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. In *Proc. of ITP'10*, volume 6172 of LNCS, pages 131–146. Springer, 2010.

[5] R. Bruni, R. Giacobazzi, R. Gori, and F. Ranzato. A Logic for Locally Complete Abstract Interpretations. In *LICS'21*, pages 1–13. IEEE, 2021.

[6] Koen Claessen, Moa Johansson, Dan Rosén, and Nicholas Smallbone. Tip: tons of inductive problems. In *International Conference on Intelligent Computer Mathematics*, pages 333–337. Springer, 2015.

[7] Nancy A. Day, J. Launchbury, and J Lewis. Logical abstractions in haskell. In *Haskell Workshop*, 1999.

[8] T. Genet, T. Haudebourg, and T. Jensen. Verifying higher-order functions with tree automata. In *FoSSaCS'18*, volume 10803 of LNCS. Springer, 2018.

[9] T. Genet, T. Le Gall, A. Legay, and V. Murat. A Completion Algorithm for Lattice Tree Automata. In *CIAA'13*, volume 7982 of LNCS, pages 134–145, 2013.

[10] T. Haudebourg, T. Genet, and T. Jensen. Regular Language Type Inference with Term Rewriting. In *ICFP'20*, volume 4, pages 112:1–112:29. ACM, 2020.

[11] M. Journault, A. Miné, and A. Ouadjaout. An Abstract Domain for Trees with Numeric Relations. In *ESOP'19*, volume 11423 of LNCS, pages 724–751. Springer, 2019.

[12] D.-E. Knuth. *The Art of Computer Programming, Volume III: Sorting and Searching*. Addison-Wesley, 1973.

[13] Y. Kostyukov, D. Mordvinov, and G. Fedyukovich. Beyond the elementary representations of program invariants over algebraic data types. In *PLDI '21*, pages 451–465. ACM, 2021.

[14] P. Lermusiaux and B. Montagu. Detection of Uncaught Exceptions in Functional Programs by Abstract Interpretation. In *ESOP'24*, volume 14577 of LNCS, pages 391–420. Springer, 2024.

[15] T. Losekoot, T. Genet, and T. Jensen. Verification of Programs with ADTs Using Shallow Horn Clauses. In *SAS'2024*, volume 14995 of LNCS, pages 242–267. Springer, 2024.
[16] Y. Matsumoto, N. Kobayashi, and H. Unno. Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs. In *APLAS'15*, volume 9458 of LNCS, pages 295-312. Springer, 2015.

[17] Philip Wadler. Theorems for free! In *Proc. of FPCA'89*, pages 347-359. ACM, 1989.
# A Optimisations of the analysis of FET

In this section we propose three optimisations of our algorithm. The first optimisation ensures that all constraints in the FET are stable star forests, and the other optimisations extend our definition of matching to more complex nodes.

## A.1 First optimisation: preservation of the star forests

Our matching criterion requires the constraints to be stable star forests, but it is not always the case with our definition of evaluation trees. Here are two examples.

**Example 9.** If $C$ is a constructor, one of the descendants of the node $C(x = y, y = z, z = x) \parallel \emptyset$ is $C(\mathit{false}, \mathit{false}, \mathit{false}) \parallel \{x \neq y, y \neq z, z \neq x\}$, whose graph is a triangle and is not a star forest. Similarly, if $f$ is a function, one of the children of the node **if** $x = y$ **then** $f(x, y)$ **else** $f(x, y) \parallel \emptyset$ is the node $f(x, y) \parallel \{x \neq y\}$. The constraint $\{x \neq y\}$ is a star forest, but both $x$ and $y$ are active, thus the star $x \neq y$ is not stable.

We propose an operation on the constraints that ensures that all constraints are stable star forests. When we add a new assertion $x \neq y$ to the constraint, we now may split this assertion by replacing $x$ or $y$ with a fresh variable. We modify the last case of the definition of the transition relation $\to$ as follows.

If $t|_{CP(t)} = (x = y)$ with $x, y \in \mathcal{V}ar$, then

$$ - t \parallel E \xrightarrow{x=y} t[\mathit{true}]_{CP(t)} \parallel E \cup \{x = y\} \text{ (though we will ignore equality assertions)} $$

$$ - t \parallel E \xrightarrow{x \neq y} t[\mathit{false}]_{CP(t)} \parallel E \cup \mathit{split}(E, t[\mathit{false}]_{CP(t)}, x, y). $$

Where $\mathit{split}(E, t', x, y)$ is defined as follows (where $u, v$ are fresh variables):

1. If $x, y \in \mathcal{V}ar(E)$ then $\mathit{split}(E, t', x, y) = \{x \neq u, u = y\}$

2. If $x \in \mathcal{V}ar(E)$, $y \notin \mathcal{V}ar(E)$ and $y \in \mathit{FV}(t')$ then $\mathit{split}(E, t', x, y) = \{x \neq u, u = y\}$

3. If $x, y \notin \mathcal{V}ar(E)$ and $x, y \in \mathit{FV}(t')$ then $\mathit{split}(E, t', x, y) = \{x \neq u, u = y\}$

4. If $x \in \mathcal{V}ar(E)$, $y \notin \mathcal{V}ar(E)$ and $y \notin \mathit{FV}(t')$ then $\mathit{split}(E, t', x, y) = \{x \neq y\}$

5. If $x, y \notin \mathcal{V}ar(E)$, and $x \notin \mathit{FV}(t')$ or $y \notin \mathit{FV}(t')$, then $\mathit{split}(E, t', x, y) = \{x \neq y\}$

## A.2 Second optimisation: matching with a context

Our definition of matching requires that the two matched terms are equal up to a variable renaming, which is rather restrictive. Indeed, consider the nodes $N = \mathit{Cons}(y_1, \mathit{Cons}(y_2, \mathit{delete}(x, l_2))) \parallel \{x \neq y_1, x \neq y_2\}$ and $\hat{N} = \mathit{Cons}(y_1, \mathit{delete}(x, l_1)) \parallel \{x \neq y_1\}$, where *delete* is defined by

$D_F : \mathit{delete}(x : X, l : \mathit{list}(X)) : \mathit{list}(X) = \mathbf{match} \ l \ \mathbf{with}$

$Nil() \Rightarrow Nil(),$

$\mathit{Cons}(y, l') \Rightarrow \mathbf{if} (x = y) \mathbf{then} \mathit{delete}(x, l') \mathbf{else} \mathit{Cons}(y, \mathit{delete}(x, l'))$
With our definition of matching, $N$ does not match $\hat{N}$, because the terms do not have the same shape.

However, note that $y_1$ in the term $\text{Cons}(y_1, \text{Cons}(y_2, \text{delete}(x, l_2)))$ has no impact on the assertions that will be added in the constraint during later evaluation steps. We thus can safely ignore the context $\text{Cons}(y_1, \Box)$, and assert that $N$ matches $\hat{N}$.

**Definition 22.** A multicontext is a term containing special variables called holes, and in which each hole appears at most once. We write $\mathcal{H} \subseteq \mathcal{V}\mathcal{A}\mathcal{R}$ for the set of holes. Holes are written $\Box, \Box_i \in \mathcal{H}$. Holes are supposed to only appear in multicontexts. A fill is a substitution $\delta: \mathcal{H} \to \mathcal{T}\mathem{e}\mathit{r}\mathit{m}$. If $H$ is a multicontext and $\delta$ is a fill then we write $H\delta$ for the term $H$ where every hole $\Box$ is replaced with $\delta(\Box)$.

**Definition 23.** An ADT-context (or simply context) is a multicontext that is a partial value and that has exactly one hole, written $\Box$. If $H$ is a context and $t$ is a term then we write $H[t]$ for $H\delta$ with $\delta(\Box) = t$.

We also want variables that only appear in the ADT-context to be considered as inactive. We redefine active variables as a consequence.

**Definition 24.** A variable $x$ is potentially active in a term $t$ (written $x \in \text{PA}(t)$) if $x \in \text{FV}(t)$ and $x$ appears in a subterm $t'$ of $t$ such that $t' \neq x$ and $t'$ that does not have an ADT constructor as a root. A variable $x \in \text{PA}(t)$ is active in a node $t \parallel E$ if $x \in \text{Var}(E)$. Otherwise $x$ is inactive. A star $S$ in $E$ is stable if every non-center vertex of $S$ is inactive.

We also adapt our definition of the split operator in the first optimisation, by replacing every condition of the form $x \in \text{FV}(t')$ with $x \in \text{PA}(t')$. This is more restrictive but still ensures that all constraints are stable star forest with our new definition of active variables.

**Definition 25 (Matching with contexts).** Let $T \parallel E$ and $\hat{t} \parallel \hat{E}$ be nodes in an ET. The node $T \parallel E$ matches $\hat{t} \parallel \hat{E}$ if there exists a context $H$ and a term $t$ such that $T = H[t]$ and $t \parallel E \sim_{\mu} \hat{t} \parallel \hat{E}$. In this case we write $T \parallel E \sim_{\mu} \hat{t} \parallel \hat{E}$ or $T \parallel E \sim \hat{t} \parallel \hat{E}$ when $H$ and $\mu$ are clear. This matching definition is called ADT-matching.

### A.3 Third optimisation: matching several subterms of a node

Here we propose a different version of the matching criterion, which applies to nested if-then-else structures that appear in the definition of functions whose output type is *Bool* (i.e. *predicate* functions).

Consider for instance a function `eq_tree` that compares two polymorphic binary trees. In the FET of `eq_tree`, two nodes $\hat{N} = (\text{eq\_tree}(t1, t2) \parallel \emptyset)$ and $N = (\text{if } \text{eq\_tree}(l1, l2) \text{ then } \text{eq\_tree}(r1, r2) \text{ else } \text{false} \parallel \{x1 = x2\})$ appear, and we cannot directly fold $N$ to $\hat{N}$ with our previous definition.
However, note that if `eq_tree(l1, l2)` evaluates to `true`, no inequality assertion is added to the constraint when evaluating `eq_tree(l1, l2)`, so the constraint `E` that we obtain still has no inequality. We conclude that when the condition of the if-the-else is true (i.e. `eq_tree(l1, l2)`) then `eq_tree(r1, r2)` associated with `E` matches `N̂`. If `eq_tree(l1, l2)` evaluates to `false` however, an inequality might appear in `E`, but in this case `eq_tree(r1, r2)` is not evaluated. As a consequence, we can always safely ignore the descendants of `N`, and fold `N` to `N̂`. Let us define this extended matching criterion.

**Definition 26 (Ite-context and Ite-terms).** An if-then-else-context (or ite-context) is a multicontext $H ::= \square \in \mathcal{H} | \text{true} | \text{false} | \text{if } H_0 \text{ then } H_1 \text{ else } H_2$. Each hole is meant to be filled with a well-typed predicate function call. An ite-term is a term $Hδ$ of type Bool where $H$ is an ite-context and the images of $δ$ are all well-typed function calls whose arguments are values.

**Critical positions** in ite-contexts are defined the same way as in terms with the following additional rules $CP(\square_i) = \varepsilon$, $CP(\text{if } H_0 \text{ then } H_1 \text{ else } H_2) = 0 \cdot CP(H_0)$ when $H_0 \notin \text{Bool}$, and $CP(\text{if } b \text{ then } H_1 \text{ else } H_2) = \varepsilon$ when $b \in \text{Bool}$. An ite-context $H$ is **reduced** if $H|_{CP(H)}$ is defined and is a hole.

**Definition 27 (H[b] : Ite-Context Tree - IteCT).** Let $H$ be a reduced ite-context and $b \in \text{Bool}$. We define $H[b]$ as the ite-context $H'$ such that $H[b]_{CP(H)} \to^* H'$ and $H'$ is stuck. $H$ thus can be seen as the root of a binary tree, whose left child is $H[\text{false}]$ and whose right child is $H[\text{true}]$. The leaves are booleans. This tree is called the **ite-context tree** (IteCT) of $H$.

*Example 10.* Let $H = \text{if} (\text{if } \square_1 \text{ then } \text{false else true}) \text{ then } \square_2 \text{ else } \square_3$.

$$H[\text{true}]_{CP(H)} = \begin{cases} \text{if} & (\text{if true then false else true}) \text{ then } \square_2 \text{ else } \square_3 \\ \text{if} & (\text{if true then false else true}) \text{ then } \square_2 \text{ else } \square_3 \end{cases} \text{ such that } \to^* \square_3$$

and $\square_3$ is stuck. Thus $H[\text{true}] = \square_3$.

We must also ensure that the constraint remains "uniform" during the evaluation of $Hδ$ from one hole to the next. This uniformity depends on $H$ and the global FET, but not on the arguments of the function calls that fill the holes of $H$.

**Definition 28.** We write $E_1 \sqsubseteq E_2$ when $||E_1|| = ||E_2||$ and the inequality graph of $E_1$ is a subgraph of the inequality graph of $E_2$ (vertex names must be identical).

**Definition 29 (Tree Safety).** Let $N̂ = (\hat{t} || \hat{E})$ be a node in a global FET. $N̂$ in the FET is **safe** on $b \in \text{Bool}$, written safe($N̂, b$), if:

- For all leaves $b || \hat{E}'$ of FET($N̂$), $\hat{E} \sqsubseteq \hat{E}'$,

- For all folded nodes $Hδ || \hat{E}'$ in the subtree of root $N̂$ in the FET,

* $Hδ || \hat{E}'$ is folded to $N̂$,

* $\hat{E} \sqsubseteq \hat{E}'$

* $H$ is reduced, and the only path in the IteCT of $H$ that possibly leads to a leaf labelled with $b$ is $b \cdot b \cdot \dots \cdot b$.
**Definition 30 (Uniformity).** The uniformity of a reduced ite-context H w.r.t a node $\hat{N} = \hat{t} \parallel \hat{E}$, written $uniform_{\hat{N}}(H)$, is defined by:

$$- uniform_{\hat{N}}(H) \stackrel{def}{=} uniform_{\hat{N}}(H, true) \wedge uniform_{\hat{N}}(H, false)$$

$$- uniform_{\hat{N}}(H, b) \stackrel{def}{=} H[b] \in \mathbf{Bool} \lor (safe(\hat{N}, b) \wedge uniform_{\hat{N}}(H[b]))$$

**Definition 31 (Ite-matching).** A node $T \parallel E$ ite-matches a node $\hat{t} \parallel \hat{E}$ if there exists a reduced ite-context $H$ and a fill $\delta$ with $T = H\delta$ such that $uniform_{\hat{t} \parallel \hat{E}}(H)$, and for all holes $\square_i$ in $H$, $\delta(\square_i) \parallel E \sim_{\mu_i} \hat{t} \parallel \hat{E}$ for some $\mu_i$. In this case we write $T \parallel E \approx_{\mu}^{H} \hat{t} \parallel \hat{E}$.

# B Analysis of whole problems

We provide details about our analysis of entire verification problems, described in Section 9. In short, this analysis consists in building an abstract domain that simultaneously refines the abstract domain of every function call in the problem, by considering the Cartesian product of these domains. To do so, we need a stronger notion of commutativity, which will also be used throughout the proof of correctness of the algorithm.

## B.1 Abstraction refinement

We propose a way to combine the results of the analyses of all function calls occurring in the verification problem in order to find a common number of constants $k$ sufficient to precisely abstract the whole problem. The idea is based on *refinement* of abstraction functions. We aim at building a *common* refined abstraction that is equal or more precise than each abstraction of the verification problem, taken separately.

**Definition 32.** An abstraction function $\beta: \mathbb{C} \to \mathbb{A}_k$ is equal or more precise than an abstraction function $\alpha: \mathbb{C} \to \mathbb{A}_{k'}$, written $\beta \preceq \alpha$, if for all $c_1, c_2 \in \mathbb{C}$, $\beta(c_1) = \beta(c_2) \implies \alpha(c_1) = \alpha(c_2)$.

The issue is that even when $\alpha$ commutes with a term $t$, an abstraction function $\beta$ such that $\beta \preceq \alpha$ does not necessarily commute with $t$.

*Example 11.* Let $P$ be the function $P(x_1: X, x_2: X, x_3: X, x_4: X) : \mathbf{Bool} = \text{if } (x_1 = x_2) \text{ then } (x_3 = x_4) \text{ else true.}$ Let $\sigma: \mathcal{Var} \to \mathcal{Nat}$ such that $\sigma(x_i) = i$ for $i = 1...4$. Then $\sigma(P(\bar{x})) \to^* \text{true}$. Let $\alpha$ such that $\alpha(1) = \alpha(2) = A_1$ and $\alpha(3) = \alpha(4) = A_2$. Let $\beta$ such that $\beta(1) = \beta(2) = A_1$, $\beta(3) = A_2$ and $\beta(4) = A_3$. Then $\alpha$ commutes with $\sigma(P(\bar{x}))$ since $(\alpha^* \circ \sigma)(P(\bar{x})) \to^* \text{true}$. Moreover $\beta \preceq \alpha$, yet $\beta$ does not commute with $\sigma(P(\bar{x}))$ since $(\beta^* \circ \sigma)(P(\bar{x})) \to^* \text{false}$.
## B.2 Strong commutativity

To solve this problem, we use a stronger notion of "commutativity". Not only do we require that $t$ and $\alpha^*(t)$ evaluate to the same value up to $\alpha^*$, but we also require that every evaluation step of $t$ and $\alpha^*(t)$ is identical. In other words, $t$ and $\alpha^*(t)$ must follow the same evaluation path.

We formalise strong commutativity with a **double semantics** $\models \subseteq (\mathcal{T}erm \times \mathcal{T}erm) \times (\mathcal{T}erm \times \mathcal{T}erm)$ that evaluates two terms simultaneously. The relation $\models$ is inductively defined by inference rules where the two terms on the left of $\models$ must use the same rule of $\rightarrow$. Since rules for $\models$ and $\rightarrow$ are very similar we do not give them in full details. We simply provide some examples of such rules to fix the ideas:

$$ \frac{\frac{\text{\textbf{(if false then } t_1 \textbf{ else } t_2, \textbf{ if false then } u_1 \textbf{ else } u_2\text{)}} \models (t_2, u_2)}{\frac{(t_i, u_i) \models (t'_i, u'_i)}{(f(\bar{v}, t_i, \dots, t_{a(f)}), f(\bar{w}, u_i, \dots, u_{a(f)})) \models (f(\bar{v}, t'_i, \dots, t_{a(f)}), f(\bar{w}, u'_i, \dots, u_{a(f)}))}} $$

In the rules for the equality check, we only require for the two terms to yield the same boolean.

$$ \frac{\frac{(v_1 = v_2) \rightarrow true \quad (w_1 = w_2) \rightarrow true}{((v_1 = v_2), (w_1 = w_2)) \rightarrow (true, true)}}{\frac{(v_1 = v_2) \rightarrow false \quad (w_1 = w_2) \rightarrow false}{((v_1 = v_2), (w_1 = w_2)) \rightarrow (false, false)}} $$

**Definition 33.** For all terms $t$, if there exists a value $v$ such that $t \to^* v$, then $t$ and $\alpha$ **strongly commute** if $(t, \alpha^*(t)) \models^* (v, \alpha^*(v))$.

The algorithm proposed in Section 7 is also correct for strong commutativity.

**Theorem 3 (Soundness of the algorithm).** If our algorithm returns $k > 0$ when given a function $f(\bar{x})$ as input, then for all types $\mathbb{C}$ and for all instantiations $\sigma$ of $f(\bar{x})$ on $\mathbb{C}$, there exists $\alpha : \mathbb{C} \to \mathbb{A}_k$ such that $\sigma(f(\bar{x}))$ and $\alpha$ **strongly commute**.

## B.3 Combination of abstractions

Unlike commuting abstractions, **strongly commuting abstractions** can be safely refined and combined. Thus, from two strongly commuting abstractions $\alpha_1$ and $\alpha_2$, we can build **one strongly commuting abstraction** $\beta$ that refines both of them.

**Proposition 4 (Abstraction refinement).** If $t \in \mathcal{T}erm$ and $\alpha : \mathbb{C} \to \mathbb{A}_{k'}$ **strongly commute**, then for all $\beta : \mathbb{C} \to \mathbb{A}_k$ such that $\beta \prec \alpha$, $t$ and $\beta$ **strongly commute**.

*Proof.* By induction on $(t, \alpha^*(t)) \models^* (v, \alpha^*(v))$.

Let $f$ and $g$ be two functions and let $\sigma$ be an instantiation of both $f(\bar{x})$ and $g(\bar{y})$ on some $\mathbb{C}$. Suppose there exist two abstraction functions $\alpha_1 : \mathbb{C} \to \mathbb{A}_{k_1}$ and $\alpha_2 : \mathbb{C} \to \mathbb{A}_{k_2}$ for some $k_1, k_2 > 0$ such that $\sigma(f(\bar{x}))$ strongly commutes with
$\alpha_1$ and $\sigma(g(\bar{y}))$ strongly commutes with $\alpha_2$. Let $\beta : \mathbb{C} \to \mathbb{A}_{k_1} \times \mathbb{A}_{k_2}$ defined as $\beta(c) = (\alpha_1(c), \alpha_2(c))$. Then $\beta \leq \alpha_1$ and $\beta \leq \alpha_2$, thus both $\sigma(f(\bar{x}))$ and $\sigma(g(\bar{y}))$ strongly commute with $\beta$, by Proposition 4. Note that, to satisfy our definition of abstract domains we can replace $\mathbb{A}_{k_1} \times \mathbb{A}_{k_2}$ by a set of new constants $\mathbb{A}_{k_1 \times k_2}$ and map every pair in $\mathbb{A}_{k_1} \times \mathbb{A}_{k_2}$ to a constant in $\mathbb{A}_{k_1 \times k_2}$. Theorem 2 is a consequence of these observations.

## B.4 Combining abstractions, the particular case without polymorphic equality

In general, the number of constants increases with each combination of abstractions. The only exception is for parametric polymorphic functions (i.e. without equality checks). Now, we show that parametric polymorphic functions strongly commute with any abstraction function with a single constant.

**Proposition 5.** Let $f \in \mathbf{Fun}$ be a parametric polymorphic function. For all instantiations $\sigma$ of $f(\bar{x})$ on some $\mathbb{C}$, $\sigma(f(\bar{x}))$ and the constant abstraction function $\alpha : \mathbb{C} \to \mathbb{A}_1$ strongly commute.

This ensures the correctness of case (A) of the algorithm 7.4. Note that this proposition generalizes Proposition 1 given by Theorems for Free to strong commutativity. As a consequence, when we analyse the functions appearing in $\phi$ with our algorithm, we can ignore all functions that are parametric polymorphic. We do not need to analyse these functions since all their instances strongly commute with the constant abstraction function of co-domain $\mathbb{A}_1$ by the above proposition.

# C Correctness of the algorithm

The proof of correctness of the algorithm is divided into two: one for functions that return an ADT-type, with the ADT-context optimisation, and another for functions that return a boolean, with the ite-context optimisation. Indeed, functions that return a boolean cannot have ADT-contexts in their ET, and ite-folding is specific to functions that return a boolean. Both proofs also suppose that the "preservation of the star forests" optimisation is used.

## C.1 With ADT-contexts and star preservation

A first key property is Lemma 7, which shows that the matching relation is a "simulation" between the ET and the FET. This entails Lemma 9, that ensures that a FET requires at least as many constants as the ET. As a consequence, to over-approximate the model of the function it is sufficient to compute the models of the constraints in the FET instead of the ET. Finally, this proves (Theorem 4) that our algorithm is correct when matching with ADT-contexts is used.

Proposition 10 ensures that all constraints in the ET and the FET are stable star forests. This is ensured by the "preservation of the star forests" optimisation.
**Proposition 6.** The semantics of our language is safe: if $\Gamma \vdash_D t : \tau$, then either $t$ is a partial value or there exists $t'$ such that $t \to t'$ and $\Gamma \vdash_D t' : \tau$.

**Proposition 7.** Matching is transitive: if $(H[t] \parallel E \sim_H^H \hat{H}[\hat{t}] \parallel \hat{E})$ and $(\hat{H}[\hat{t}] \parallel \hat{E} \sim_{\hat{\mu}}^{\hat{H}} \hat{t} \parallel \hat{E})$ then $(H[t] \parallel E \sim_{\hat{\mu} \circ \mu}^{H[\mu^{-1}(\hat{H})]} \hat{t} \parallel \hat{E})$.

**Proposition 8 (Node instantiation).** For any node $t \parallel E$ such that $t \parallel E \xrightarrow{t'_j} t'_j \parallel E'_j$ for all $j \in [1, m]$, then for all instantiations $\sigma$ such that $\sigma(t)$ is well typed, there exists a unique $j \in [1, m]$ such that $\sigma(t) \to \sigma'(t'_j)$, where $\sigma'$ is an extension of $\sigma$. Moreover, if $\sigma \models E$ then $\sigma' \models E'_j$. In this case we write $\sigma(t \parallel E) \xrightarrow{t'_j} \sigma'(t'_j \parallel E'_j)$. In other words, the $t'_j$ represent a partition of all the terms that are reachable in one evaluation steps by the instantiations of $t$.

**Lemma 5.** If $u\sigma \to t'$, then there exists $u' \in \mathcal{T}erm$ such that for any constraint $E$, $(u \parallel E)\sigma \rightsquigarrow (u' \parallel E')\sigma'$ for some $E'$, $\sigma'$ with $t' = u'\sigma'$.

**Proposition 9.** For all $\sigma$ instantiating $f(\bar{x})$ on some type $\mathbb{C}$, if $\sigma(f(\bar{x}) \parallel \emptyset) \rightsquigarrow^* \sigma_f(v \parallel E_f)$ and if $k \models E_f$, then

$$ \exists \alpha : \mathbb{C} \to \mathbb{A}_k. (\sigma(f(\bar{x})), (\alpha^* \circ \sigma)(f(\bar{x}))) \rightsquigarrow^* (\sigma_f(v), (\alpha^* \circ \sigma_f)(v)) $$

In other words, $\sigma(f(\bar{x}))$ evaluates to $v \parallel E_f$ and $E_f$ is satisfied by $k$ constants, then $\mathbb{A}_k$ is big enough to completely abstract the evaluation of $\sigma(f(\bar{x}))$.

*Proof.* By induction on the length of the evaluation path.

**Lemma 6.** For all nodes $t \parallel E, t' \parallel E'$ and for all contexts $H, t \parallel E \xrightarrow{t'} t' \parallel E'$ iff there exists a substitution $\rho: \mathcal{V}ar \to \mathcal{V}$ such that $H[t] \parallel E \xrightarrow{t} \rho(H)[t'] \parallel E'$.

**Proposition 10.** For all nodes $t \parallel E$ in ET($f(\bar{x})$), $E$ is a stable star forest.

*Proof.* By induction on ET($f(\bar{x})$). The only case that modifies the inequality graph is a transition of the form $t_1 \parallel E_1 \xrightarrow{x \neq y} t_2 \parallel E_2$. In this case, the constraint splitting introduced by the "preservation of star forests" optimisation ensures that if $E_1$ is a stable star forest then $E_2$ is a stable star forest.

**Lemma 7 (Simulation).** If $H[t] \parallel E \xrightarrow{t} \rho(H)[t'] \parallel E'$ for some $\rho: \mathcal{V}ar \to \mathcal{V}$ and $H[t] \parallel E \sim_H^H \hat{t} \parallel \hat{E}$ and $\hat{t} \parallel \hat{E} \xrightarrow{\mu(l)} \hat{t}' \parallel \hat{E}'$ then $\rho(H)[t'] \parallel E' \sim_{\mu'}^{\rho(H)} \hat{t}' \parallel \hat{E}'$ for some $\mu'$ extending $\mu$.

*Proof.* Since $t$ and $t'$ are equal up to $\mu'$, the only difficult case is $t_1 \parallel E \xrightarrow{x \neq y} t_2 \parallel E'$. In this case, we check that for every possible constraint split introduced by the "preservation of star forests" optimisation, the resulting constraints still have the same number of stars, and have the same star centers up to $\mu'$.
**Lemma 8.** Every node in the FET matches some node in the ET: if $H[t] \parallel E \to^* T_f \parallel E_f$ and $H[t] \parallel E \sim_H^H \hat{t} \parallel \hat{E}$, then there exist $(\hat{t}_f \parallel \hat{E}_f) \in \text{FET}(f(\bar{x}))$, a context $H_f$ and a bijective renaming $\mu_f$ such that $T_f \parallel E_f \sim_{\mu_f}^H \hat{t}_f \parallel \hat{E}_f$.

*Proof.* Consequence of Lemma 7.

**Lemma 9 (The FET over-approximates the ET).** If for all nodes $\hat{t} \parallel \hat{E}$ in $\text{FET}(f(\bar{x}))$, $\|\hat{E}\| \le k$, then for all reachable nodes $T \parallel E$ in $\text{ET}(f(\bar{x}))$, $\|E\| \le k$.

*Proof.* Since $T \parallel E$ is reachable, there exist $\sigma_0$, $\sigma$ such that $(f(\bar{x}) \parallel \emptyset)\sigma_0 \rightsquigarrow^* (T \parallel E)\sigma$. Then by definition of $\rightsquigarrow$, $f(\bar{x}) \parallel \emptyset \to^* T \parallel E$. By Lemma 8, since $f(\bar{x}) \parallel \emptyset \sim f(\bar{x}) \parallel \emptyset$, there exist $H, \mu$ and a node $\hat{t} \parallel \hat{E}$ in $\text{FET}(f(\bar{x}))$ such that $T \parallel E \sim_H^H \hat{t} \parallel \hat{E}$. Therefore, by definition of matching, $\|E\| = \|\hat{E}\| \le k$.

**Theorem 4 (The algorithm is correct with ADT-context matching).**
Given a terminating function $f$, if the algorithm (with ADT-context matching and star forest preservation) successfully returns $k > 0$, then for all instantiations $\sigma$ of $f(\bar{x})$ on some type $\mathbb{C}$, there exists an abstraction function $\alpha : \mathbb{C} \to \mathbb{A}_k$ such that $\sigma(f(\bar{x}))$ and $\alpha$ strongly commute.

*Proof.* Let $\sigma$ instantiating $f(\bar{x})$ on some type $\mathbb{C}$. Since $f$ terminates and $f(\bar{x})$ is well-typed, then by safety of the semantics there exists $v \in \mathcal{V}$ such that $f(\bar{x})\sigma \to^* v$. Therefore, by Lemma 5, there exists a node $v_f \parallel E_f \in \text{ET}(f(\bar{x}))$ such that $(f(\bar{x}) \parallel \emptyset)\sigma \rightsquigarrow^* (v_f \parallel E_f)\sigma_f$, for some $\sigma_f$ such that $v = v_f\sigma_f$. The algorithm ensures that for all nodes $\hat{t} \parallel \hat{E}$ in $\text{FET}(f(\bar{x}))$, $\|\hat{E}\| \le k-1$. Therefore, by Lemma 9, $k$ satisfies all reachable nodes in $\text{ET}(f(\bar{x}))$. In particular $k \models E_f$. Therefore, by Proposition 9, there exists $\alpha : \mathbb{C} \to \mathbb{A}_k$ such that

$$ (\sigma(f(\bar{x})), (\alpha^* \circ \sigma)(f(\bar{x}))) \rightsquigarrow^* (\sigma_f(v_f), (\alpha^* \circ \sigma_f)(v_f)) $$

In other words $\sigma(f(\bar{x}))$ and $\alpha$ strongly commute.

## C.2 With ite-contexts and star preservation

Lemma 12 complements Lemma 7 by describing another kind of simulation, between the ET the function calls within an ite-folded node of the FET. Together, these properties entail Lemma 13, which, similarly to Lemma 9, ensures that the FET with ite-folding also over-approximates the ET. Finally, this proves (Theorem 5) that our algorithm is correct when matching with ite-contexts is used.

**Lemma 10.** Let $H_0$ be a reduced ite-context. For all well-typed fills $\delta_0$ of $H_0$, for all instantiations $\sigma_0$ and for all constraints $E_0$, then

$$ \begin{align*} \sigma(H_0 \delta \parallel E) &\rightsquigarrow^* \sigma_1(H_0 \llbracket b_1 \rrbracket \delta_1 \parallel E_1) \\ &\vdots \\ &\rightsquigarrow^* \sigma_n(H_0 \llbracket b_1 \rrbracket \dots \llbracket b_n \rrbracket \delta_n \parallel E_n) \end{align*} $$
for some $\delta_i$, $\sigma_i$ and $E_i$, such that $H_n \in \text{Bool}$, and for all $i \in [0, n-1]$, $H_i$ is reduced, $\delta_{i+1}$ extends $\delta_i$ and $\sigma_i(H_{i|_{CP(H_i)}}\delta_i) \to^* b_{i+1}$.

This lemma describes how an instantiation follows a path in the IteCT of a filled ite-context.

**Lemma 11 (Tree Safety).** Suppose the node $\hat{t}_0 \parallel \hat{E}_0$ in some FET is safe on $b \in \text{Bool}$. Then for all instantiations $\sigma_0$, if $\sigma_0(\hat{t}_0 \parallel \hat{E}_0) \rightsquigarrow^* \sigma_f(b \parallel \hat{E}_f)$ for some $b \in \text{Bool}$, $\sigma_f$ and $\hat{E}_f$, then $\hat{E}_0 \sqsubseteq \hat{E}_f$.

*Proof.* By induction on the length of $\sigma_0(\hat{t}_0 \parallel \hat{E}_0) \rightsquigarrow^* \sigma_f(b \parallel \hat{E}_f)$, then by induction on the structure of the IteCT of an ite-context of a folded node $H\delta \parallel E$ that we may encounter. The safety condition ensures that the evaluation of the function calls appearing in $H\delta$ never introduces any new star in the star forest (it may at most add leaves to some already existing stars).

**Lemma 12 (IteCT Simulation).** Let $H$ be an ite-context, let $\delta$ be a well-typed fill for $H$ and let $\sigma$ be an instantiation of $H\delta$. If $H\delta \parallel E \approx \hat{t} \parallel \hat{E}$, $\sigma(H|_{CP(H)}\delta) \to^* b \in \text{Bool}$ and $H[b] \notin \text{Bool}$, then there exists a constraint $E'$ and an instantiation $\sigma'$ extending $\sigma$ such that $\sigma(H\delta \parallel E) \rightsquigarrow^* \sigma'(H[b]\delta \parallel E')$ and $H[b]\delta \parallel E' \approx \hat{t} \parallel \hat{E}$.

*Proof.* Since $H$ is uniform, $\hat{t} \parallel \hat{E}$ is safe on $b$. As a consequence, by Lemma 11, the evaluation of the function call $H|_{CP(H)}\delta$ preserves the constraint $E$. Moreover, all function calls in $H[b]\delta$ already appeared in $H\delta$. As a consequence, $H[b]\delta \parallel E' \approx \hat{t} \parallel \hat{E}$.

**Lemma 13 (ET Overapproximation).** If for all nodes $\hat{t} \parallel \hat{E}$ in FET($f(\bar{x})$), $\parallel \hat{E}\parallel \le k$, then for all reachable nodes $T \parallel E$ in ET($f(\bar{x})$), $\parallel E\parallel \le k$.

*Proof.* This is a consequence of Lemma 12.

**Theorem 5 (The algorithm is correct with ite-context matching).** The algorithm is correct: given a terminating function $f$, if the algorithm (with ite-context matching and star forest preservation) successfully returns $k > 0$, then for all instantiations $\sigma$ of $f(\bar{x})$ on some type $C$, there exists an abstraction function $\alpha: C \to A_k$ such that $\sigma(f(\bar{x}))$ and $\alpha$ strongly commute.

*Proof.* The proof is similar to Theorem 3, with Lemma 13 instead of Lemma 9.