# Optimal matching for sharing and linearity analysis

AMATO GIANLUCA  0000-0002-6214-5198<EMAIL_ADDRESS>SCOZZARI FRANCESCA
0000-0002-2105-4855<EMAIL_ADDRESS>
###### Abstract

Static analysis of logic programs by abstract interpretation requires
designing abstract operators which mimic the concrete ones, such as
unification, renaming and projection. In the case of goal-driven analysis,
where goal-dependent semantics are used, we also need a backward-unification
operator, typically implemented through matching. In this paper we study the
problem of deriving optimal abstract matching operators for sharing and
linearity properties. We provide an optimal operator for matching in the
domain ${\mathtt{ShLin}^{\omega}}$, which can be easily instantiated to derive
optimal operators for the domains ${\mathtt{ShLin}^{2}}$ by Andy King and the
reduced product $\mathtt{Sharing}\times\mathtt{Lin}$.

###### keywords:

static analysis, sharing, linearity, matching.

##  1 Introduction

In the field of static analysis of logic programs, sharing information is one
of the most interesting and widely used property. The goal of sharing analysis
is to detect sets of variables which share a common variable. For instance, in
the substitution $\\{x/f(z,a),y/g(z)\\}$ the variables $x$ and $y$ share the
common variable $z$. Sharing may also track and infer groundness in the same
way as the Def domain (de la Banda and Hermenegildo, 1993; Armstrong et al.,
1998). Typical applications of sharing analysis are in the fields of
optimization of unification (Søndergaard, 1986) and parallelization of logic
programs (Hermenegildo and Rossi, 1995).

It is widely recognized that the pioneering abstract domain $\mathtt{Sharing}$
(Langen, 1990; Jacobs and Langen, 1992) is not very precise, so that it is
often combined with other domains for tracking freeness, linearity, groundness
or structural information (see Bagnara et al., (2005); Codish et al., (1995)
for comparative evaluations).

Any domain for static analysis of logic programs must be equipped with four
standard operators: renaming, projection, union and unification. The theory of
abstract interpretation (Cousot and Cousot, 1979; Cousot and Cousot, 1992a )
ensures the existence of the optimal (best correct) abstract operator for each
concrete operator. Nevertheless, while finding optimal operators for renaming,
projection and union is trivial most of the time, devising an optimal abstract
unification is much harder.

Amato and Scozzari, (2010; 2014) have proposed a new (infinite) domain
${\mathtt{ShLin}^{\omega}}$ which precisely represents the interaction between
sharing and linearity properties, while discharging other structural,
irrelevant information. All the abstract operators for
${\mathtt{ShLin}^{\omega}}$ are shown to be optimal. From
${\mathtt{ShLin}^{\omega}}$ the authors derive, for the first time, optimal
abstract unification for well-known domains combining sharing and linearity,
such as ${\mathtt{ShLin}^{2}}$ (King, 1994) and
$\mathtt{Sharing}\times\mathtt{Lin}$ (Muthukumar and Hermenegildo, 1992).

In this paper we extend the ${\mathtt{ShLin}^{\omega}}$ framework to the case
of goal-dependent analysis. In this setting, the unification operator is used
twice (see Figure 1):

forward unification:

performs parameter passing by unifying the goal and the _call substitution_
with the head of the chosen clause. The result is called _entry substitution_.

backward unification:

propagates back to the goal the _exit substitution_ (that is, the result of
the sub-computation), obtaining the _answer substitution_ 111We follow Cortesi
et al., (1996) for the terminology of _forward_ and _backward unification_.
Bruynooghe, (1991) and Hans and Winkler, (1992) use _procedure entry_ and
_procedure exit_. Muthukumar and Hermenegildo, (1991) use _call_to_entry_ and
_exit_to_success_..

call substitutionentry substitutionexit substitutionanswer substitutionforward
unificationcomputationbackward unification Figure 1: The role of forward and
backward unification in goal-dependent analysis.

Despite its name, backward unification may be implemented through _matching_ ,
exploiting the property that the exit substitution is always more instantiated
than the call substitution. Analyses with matching are strictly more precise
than analyses which do not use matching (see Bruynooghe, (1991) and Amato and
Scozzari, (2009) for a thorough discussion of the problem). This idea has been
implemented in real abstract interpreters such as GAIA (Le Charlier and Van
Hentenryck, 1994) and PLAI (Muthukumar and Hermenegildo, 1992).

However, except for Amato and Scozzari, (2009), none of the papers which are
based on matching (Bruynooghe, 1991; Le Charlier and Van Hentenryck, 1994;
Hans and Winkler, 1992; Muthukumar and Hermenegildo, 1992; King and Longley,
1995) has ever proved optimality of the proposed abstract operators. In
particular, there is no known optimal matching operator for any domain
combining sharing and linearity.

The lack of optimal operators brings two kinds of disadvantages: first, the
analysis obviously loses precision when using suboptimal abstract operators;
second, computing approximated abstract objects can lead to a speed-down of
the analysis. The latter is typical of sharing analysis, where abstract
domains are usually defined in such a way that, the less information we have,
the more abstract objects are complex. This is not the case for other kind of
analyses, such as groundness analysis, where the complexity of abstract
objects may grow accordingly to the amount of groundness information they
encode. Moreover, knowing the optimal abstract operator, even if we do not
plan to implement it, is useful to understand the potentiality and limits of
the abstract domain in use, and to guide the search for a more precise (or
more efficient) domain.

For this reason, in this paper we define a matching operator for
${\mathtt{ShLin}^{\omega}}$ and prove its optimality. Moreover, from this
operator, we derive, for the first time, optimal matching operators for
domains combining sharing and linearity information, such as
${\mathtt{ShLin}^{2}}$ and $\mathtt{Sharing}\times\mathtt{Lin}$.

##  2 Notations

We fix a first order signature that includes a constant symbol and a function
symbol of arity at least two, otherwise every term has at most one variable,
and the structure of terms is trivial (we need this assumption in the proofs
of optimality). The signature also includes a denumerable set of variables
$\mathcal{V}$. Given a term or other syntactic object $o$, we denote by
$\mathrm{vars}(o)$ the set of variables occurring in $o$. Given a set $A$, we
denote by $\mathscr{P}(A)$ the powerset of $A$ and by $\mathscr{P}_{f}(A)$ the
set of finite subsets of $A$.

###  2.1 Multisets

A _multiset_ is a set where repetitions are allowed. We denote by
$\\{\\!\\!\\{x_{1},\ldots,x_{m}\\}\\!\\!\\}$ a multiset, where
$x_{1},\ldots,x_{m}$ is a sequence with (possible) repetitions, and by
$\\{\\!\\!\\{\\}\\!\\!\\}$ the empty multiset. We will often use the
polynomial notation $v_{1}^{i_{1}}\ldots v_{n}^{i_{n}}$, where
$v_{1},\ldots,v_{n}$ is a sequence without repetitions, to denote a multiset
$A$ whose element $v_{j}$ appears $i_{j}$ times. The set $\\{v_{j}\mid
i_{j}>0\\}$ is called the _support_ of $A$ and is denoted by $\llfloor
A\rrfloor$. We also use the functional notation
$A:\\{v_{1},\ldots,v_{n}\\}\rightarrow\mathbb{N}$, where $A(v_{j})=i_{j}$.

In this paper, we only consider multisets whose support is _finite_. We denote
with $\mathscr{P}_{m}(X)$ the set of all the multisets whose support is _any
finite subset_ of $X$. For example, $a^{3}c^{5}$ and $a^{3}b^{2}c^{1}$ are
elements of $\mathscr{P}_{m}(\\{a,b,c\\})$. The fundamental operation for
multisets is the _sum_ , defined as

$A\uplus B=\lambda v\in\llfloor A\rrfloor\cup\llfloor
B\rrfloor.A(v)+B(v)\enspace.$

Note that we also use $\uplus$ to denote disjoint union for standard sets. The
context will allow us to discern the proper meaning of $\uplus$. Given a
multiset $A$ and $X\subseteq\llfloor A\rrfloor$, the _restriction_ of $A$ over
$X$, denoted by $A_{|X}$, is the only multiset $B$ such that $\llfloor
B\rrfloor=X$ and $B(v)=A(v)$ for each $v\in X$.

###  2.2 The domain of existential substitutions

We work in the framework of existential substitutions (Amato and Scozzari,
2009), which allows us to simplify those semantic definitions which are
heavily based on renaming apart objects and to avoid variable clashes. In this
framework all the details concerning renamings are moved to the inner level of
the semantic domain, where they are more easily manageable. We briefly recall
the basic definitions of the domain.

The set of substitutions, idempotent substitutions, and renamings are denoted
by $\mathit{Subst}$, $\mathit{ISubst}$, and $\mathit{Ren}$ respectively. Given
$\theta_{1},\theta_{2}\in\mathit{Subst}$ and
$U\in\mathscr{P}_{f}(\mathcal{V})$, the preorder $\preceq_{U}$ is defined as
follows:

$\theta_{1}\preceq_{U}\theta_{2}\iff\exists\delta\in\mathit{Subst}.\forall
x\in U.\ \theta_{1}(x)=\delta(\theta_{2}(x))\enspace.$

The notation $\theta_{1}\preceq_{U}\theta_{2}$ states that $\theta_{1}$ is an
instance of $\theta_{2}$ w.r.t. the variables in $U$. The equivalence relation
induced by the preorder $\preceq_{U}$ is given by:

$\theta_{1}\sim_{U}\theta_{2}\iff\exists\rho\in\mathit{Ren}.\forall x\in U.\
\theta_{1}(x)=\rho(\theta_{2}(x))\enspace.$

Let $\mathit{ISubst}_{\sim_{U}}$ be the quotient set of $\mathit{ISubst}$
w.r.t. $\sim_{U}$. The domain $\mathit{ISubst}_{\sim}$ of _existential
substitutions_ is defined as the disjoint union of all the
$\mathit{ISubst}_{\sim_{U}}$ for $U\in\mathscr{P}_{f}(\mathcal{V})$, namely:

$\mathit{ISubst}_{\sim}=\biguplus_{U\in\mathscr{P}_{f}(\mathcal{V})}\mathit{ISubst}_{\sim_{U}}\enspace.$

In the following we write $[\theta]_{U}$ for the equivalence class of $\theta$
w.r.t. $\sim_{U}$. The partial order $\preceq$ over $\mathit{ISubst}_{\sim}$
is given by:

$[\theta]_{U}\preceq[\theta^{\prime}]_{V}\iff U\supseteq
V\wedge\theta\preceq_{V}\theta^{\prime}\enspace.$

Intuitively, $[\theta]_{U}\preceq[\theta^{\prime}]_{V}$ means that $\theta$ is
an instance of $\theta^{\prime}$ w.r.t. the variables in $V$, provided that
they are all variables of interest of $\theta$.

To ease notation, we often omit braces from the sets of variables of interest
when they are given extensionally. So we write $[\theta]_{x,y}$ or
$[\theta]_{xy}$ instead of $[\theta]_{\\{x,y\\}}$ and $\sim_{x,y,z}$ instead
of $\sim_{\\{x,y,z\\}}$. When the set of variables of interest is clear from
the context or when it is not relevant, it will be omitted. Finally, we omit
the braces which enclose the bindings of a substitution when the latter occurs
inside an equivalence class, i.e., we write $[x/y]_{U}$ instead of
$[\\{x/y\\}]_{U}$.

####  2.2.1 Unification

Given $U,V\in\mathscr{P}_{f}(\mathcal{V})$,
$[\theta_{1}]_{U},[\theta_{2}]_{V}\in\mathit{ISubst}_{\sim}$, the most general
unifier between these two classes is defined as the mgu of suitably chosen
representatives, where variables not of interest are renamed apart. In
formulas:

$\mathsf{mgu}([\theta_{1}]_{U},[\theta_{2}]_{V})=[\mathsf{mgu}(\theta^{\prime}_{1},\theta^{\prime}_{2})]_{U\cup
V}\enspace,$ (1)

where $\theta_{1}\sim_{U}\theta^{\prime}_{1}\in\mathit{ISubst}$,
$\theta_{2}\sim_{V}\theta^{\prime}_{2}\in\mathit{ISubst}$ and
$(U\cup\mathrm{vars}(\theta^{\prime}_{1}))\cap(V\cup\mathrm{vars}(\theta^{\prime}_{2}))\subseteq
U\cap V$. The last condition is needed to avoid variable clashes between the
chosen representatives $\theta^{\prime}_{1}$ and $\theta^{\prime}_{2}$. It
turns out that $\mathsf{mgu}$ is the greatest lower bound of
$\mathit{ISubst}_{\sim}$ ordered by $\preceq$.

A different version of unification is obtained when one of the two arguments
is an existential substitution and the other one is a standard substitution.
In this case, the latter argument may be viewed as an existential substitution
where all the variables are of interest:

$\mathsf{mgu}([\theta]_{U},\delta)=\mathsf{mgu}([\theta]_{U},[\delta]_{\mathrm{vars}(\delta)})\enspace.$
(2)

Note that deriving the general unification in (1) from the special case in (2)
is not possible. This is because there are elements in
$\mathit{ISubst}_{\sim}$ which cannot be obtained as
$[\delta]_{\mathrm{vars}(\delta)}$ for any $\delta\in\mathit{ISubst}$.

This is the form of unification which is better suited for analysis of logic
programs, where existential substitutions are the denotations of programs
while standard substitutions are the result of unification between goals and
heads of clauses. Devising optimal abstract operators for (2) in different
abstract domains is the topic of Amato and Scozzari, (2010).

####  2.2.2 Matching

Given $U_{1},U_{2}\in\mathscr{P}_{f}(\mathcal{V})$,
$[\theta_{1}]_{U_{1}}\in\mathit{ISubst}_{\sim}$ and
$[\theta_{2}]_{U_{2}}\in\mathit{ISubst}$, the matching of
$[\theta_{1}]_{U_{1}}$ with $[\theta_{2}]_{U_{2}}$ (Amato and Scozzari, 2009)
is defined in the same way as unification, as soon as none of the variables in
$U_{1}$ get instantiated in the result. If this is not the case, the matching
is undefined.

######  Definition 2.1 (Matching)

Given $[\theta_{1}]_{U_{1}},[\theta_{2}]_{U_{2}}\in\mathit{ISubst}_{\sim}$ we
have that

$\mathsf{match}([\theta_{1}]_{U_{1}},[\theta_{2}]_{U_{2}})=\begin{cases}\mathsf{mgu}([\theta_{1}]_{U_{1}},[\theta_{2}]_{U_{2}})&\text{if
}\theta_{1}\preceq_{U_{1}\cap U_{2}}\theta_{2},\\\
\text{undefined}&\text{otherwise.}\end{cases}$ (3)

Note that the condition $\theta_{1}\preceq_{U_{1}\cap U_{2}}\theta_{2}$ is
equivalent to
$[\theta_{1}]_{U_{1}}=\mathsf{mgu}([\theta_{1}]_{U_{1}},[\theta_{2}]_{U_{2}})_{|U_{1}}$
(Amato and Scozzari, 2009).

###### Example 2.2

If we unify $[\theta_{1}]_{x,y}=[x/a,y/b]_{x,y}$ with
$[\theta_{2}]_{y,z}=[z/r(y)]_{y,z}$, we obtain
$[\theta_{3}]_{x,y,z}=[x/a,y/b,z/r(b)]_{x,y,z}$. Note that the variables $y$
and $z$ in $\theta_{3}$ are instantiated w.r.t. $\theta_{2}$, therefore
$\mathsf{match}([\theta_{2}]_{y,z},[\theta_{1}]_{x,y})$ is undefined. However,
$x$ and $y$ in $\theta_{3}$ are not instantiated w.r.t. $\theta_{1}$,
therefore
$\mathsf{match}([\theta_{1}]_{x,y},[\theta_{2}]_{y,z})=[\theta_{3}]_{x,y,z}$.

Most of the time, when matching is applied in goal-dependent analysis of logic
programs, we have that $U_{1}\subseteq U_{2}$. This is because $U_{1}$ is the
set of variables in a clause, while $U_{2}$ contains both the variables in the
clause and in the call substitution. Nonetheless, we study here the general
case, so that it can be applied in any framework.

####  2.2.3 Other operations

Given $V\in\mathscr{P}_{f}(\mathcal{V})$ and
$[\theta]_{U}\in\mathit{ISubst}_{\sim}$, we denote by $([\theta]_{U})_{|V}$
the _projection_ of $[\theta]_{U}$ on the set of variables $V$, defined as:

$([\theta]_{U})_{|V}=[\theta]_{U\cap V}\enspace.$ (4)

###  2.3 Abstract interpretation

Given two sets $C$ and $A$ of concrete and abstract objects respectively, an
_abstract interpretation_ (Cousot and Cousot, 1992b ) is given by an
approximation relation $\rightslice\subseteq A\times C$. When $a\rightslice c$
holds, this means that $a$ is a correct abstraction of $c$. We are interested
in the case when $(A,\leq_{A})$ is a poset and $a\leq_{A}a^{\prime}$ means
that $a$ is more precise than $a^{\prime}$. In this case we require that, if
$a\rightslice c$ and $a\leq_{A}a^{\prime}$, then $a^{\prime}\rightslice c$,
too. In more detail, we require what Cousot and Cousot, 1992b  call the
_existence of the best abstract approximation assumption_ , i.e., the
existence of a map $\alpha:C\rightarrow A$ such that for all $a\in A,c\in C$,
it holds that $a\rightslice c\iff\alpha(c)\leq_{A}a$. The map $\alpha$ is
called the _abstraction function_ and maps each $c$ to its best approximation
in $A$.

Given a (possibly partial) function $f:C\rightarrow C$, we say that
$\tilde{f}:A\rightarrow A$ is a correct abstraction of $f$, and write
$\tilde{f}\rightslice f$, whenever

$a\rightslice c\Rightarrow\tilde{f}(a)\rightslice f(c)\enspace,$

assuming that $\tilde{f}(a)\rightslice f(c)$ is true whenever $f(c)$ is not
defined. We say that $\tilde{f}:A\rightarrow A$ is the _optimal_ abstraction
of $f$ when it is the best correct approximation of $f$, i.e., when
$\tilde{f}\rightslice f$ and

$\forall f^{\prime}:A\rightarrow A.\ f^{\prime}\rightslice
f\Rightarrow\tilde{f}\leq_{A\rightarrow A}f^{\prime}\enspace.$

In some cases, we prefer to deal with a stronger framework, in which the
domain $C$ is also endowed with a partial order $\leq_{C}$ and
$\alpha:C\rightarrow A$ is a left adjoint to $\gamma:A\rightarrow C$, i.e.,

$\forall c\in C.\forall a\in A.\alpha(c)\leq_{A}a\iff
c\leq_{C}\gamma(a)\enspace.$

The pair $\langle\alpha,\gamma\rangle$ is called a _Galois connection_. In
particular, we will only consider the case of _Galois insertions_ , which are
Galois connections such that $\alpha\circ\gamma$ is the identity map. If
$\langle\alpha,\gamma\rangle$ is a Galois insertion and $f:C\rightarrow C$ is
a monotone map, the optimal abstraction $\tilde{f}$ always exists, and it is
definable as $\tilde{f}=\alpha\circ f\circ\gamma$.

##  3 Abstract matching over ${\mathtt{ShLin}^{\omega}}$

The domain ${\mathtt{ShLin}^{\omega}}$ (Amato and Scozzari, 2010) generalizes
$\mathtt{Sharing}$ by recording multiplicity of variables in sharing groups.
For example, the substitution $\theta=\\{x/s(u,v),y/g(u,u,u),z/v\\}$ is
abstracted on $\mathtt{Sharing}$ into $\\{uxy,vxz\\}$, where the sharing group
$uxy$ means that $\theta(u)$, $\theta(x)$, and $\theta(y)$ share a common
variable, namely $u$. In ${\mathtt{ShLin}^{\omega}}$ the same substitution
would be abstracted as $\\{uxy^{3},vxz\\}$, with the additional information
that the variable $u$ occurs three times in $\theta(y)$. For the sake of
completeness, in the following section we recall the basic definitions.

###  3.1 The domain ${\mathtt{ShLin}^{\omega}}$

We call _$\omega$ -sharing group_ a multiset of variables, i.e., an element of
$\mathscr{P}_{m}(\mathcal{V})$. Given a substitution $\theta$ and a variable
$v\in\mathcal{V}$, we denote by $\theta^{-1}(v)$ the $\omega$-sharing group
$\lambda w\in\mathcal{V}.\mathit{occ}(v,\theta(w))$, which maps each variable
$w$ to the number of occurrences of $v$ in $\theta(w)$.

Given a set of variables $U$ and a set of $\omega$-sharing groups
$S\subseteq\mathscr{P}_{m}(U)$, we say that $[S]_{U}$ _correctly approximates_
a substitution $[\theta]_{W}$ if $U=W$ and, for each $v\in\mathcal{V}$,
$\theta^{-1}(v)_{|U}\in S$. We write $[S]_{U}\rightslice[\theta]_{W}$ to mean
that $[S]_{U}$ correctly approximates $[\theta]_{W}$. Therefore,
$[S]_{U}\rightslice[\theta]_{U}$ when $S$ contains all the $\omega$-sharing
groups in $\theta$, restricted to the variables in $U$.

######  Definition 3.1 (${\mathtt{ShLin}^{\omega}}$)

The domain ${\mathtt{ShLin}^{\omega}}$ is defined as

${\mathtt{ShLin}^{\omega}}=\\{[S]_{U}\mid
U\in\mathscr{P}_{f}(\mathcal{V}),S\subseteq\mathscr{P}_{m}(U),S\neq\emptyset\Rightarrow\\{\\!\\!\\{\\}\\!\\!\\}\in
S\\}\enspace,$ (5)

and ordered by $[S_{1}]_{U_{1}}\leq_{\omega}[S_{2}]_{U_{2}}$ iff $U_{1}=U_{2}$
and $S_{1}\subseteq S_{2}$.

The existence of the empty multiset, when $S$ is not empty, is required in
order to have a surjective abstraction function.

In order to ease the notation, we write
$[\\{\\{\\!\\!\\{\\}\\!\\!\\},B_{1},\ldots,B_{n}\\}]_{U}$ as
$[B_{1},\ldots,B_{n}]_{U}$ by omitting the braces and the empty multiset, and
variables in each $\omega$-sharing group are sorted lexicographically.
Moreover, if $X\in{\mathtt{ShLin}^{\omega}}$, we write $B\in X$ in place of
$X=[S]_{U}\wedge B\in S$. Analogously, if
$S^{\prime}\in{\mathtt{ShLin}^{\omega}}$, we write $S^{\prime}\subseteq X$ in
place of $X=[S]_{U}\wedge S^{\prime}\subseteq S$. The best correct abstraction
of a substitution $[\theta]_{U}$ is

$\alpha_{\omega}([\theta]_{U})=[\\{\theta^{-1}(v)_{|U}\mid
v\in\mathcal{V}\\}]_{U}\enspace.$ (6)

###### Example 3.2

Given $\theta=\\{x/s(y,u,y),z/s(u,u),v/u\\}$ and $U=\\{w,x,y,z\\}$, we have
$\theta^{-1}(u)=uvxz^{2}$, $\theta^{-1}(y)=x^{2}y$,
$\theta^{-1}(z)=\theta^{-1}(v)=\theta^{-1}(x)=\\{\\!\\!\\{\\}\\!\\!\\}$ and
$\theta^{-1}(o)=o$ for all the other variables ($w$ included). Projecting over
$U$ we obtain $\alpha_{\omega}([\theta]_{U})=[x^{2}y,xz^{2},w]_{U}$.

###  3.2 Matching operator

In the matching operation, when $[\theta_{1}]_{U_{1}}$ is matched with
$[\theta_{2}]_{U_{2}}$, sharing groups in $\theta_{1}$ and $\theta_{2}$ are
joined together in the resulting substitution. However, not all combinations
are allowed. Assume
$\alpha_{\mathrm{\omega}}([\theta_{i}]_{U_{i}})=[S_{i}]_{U_{i}}$ for
$i\in\\{1,2\\}$. If
$\mathsf{match}([\theta_{1}]_{U_{1}},[\theta_{2}]_{U_{2}})$ is defined,
$\theta_{1}$ will not be further instantiated and thus
$\alpha_{\mathrm{\omega}}(\mathsf{match}([\theta_{1}]_{U_{1}},[\theta_{2}]_{U_{2}})_{|U_{1}})\subseteq
S_{1}$. Moreover, the sharing groups in $S_{2}$ which do not contain any
variable in $U_{1}$ are not affected by the unification, since the
corresponding existential variable does not appear in $\theta_{2}(v)$ for any
$v\in U_{1}$.

###### Example 3.3

Let $\theta_{1}=\\{x/r(w_{1},w_{2},w_{2},w_{3},w_{3}),y/a,z/r(w_{1})\\}$ with
$U_{1}=\\{x,y,z\\}$ and
$\theta_{2}=\\{x/r(w_{4},w_{5},w_{6},w_{8},w_{8}),u/r(w_{4},w_{7}),v/r(w_{7},w_{8})\\}$
with $U_{2}=\\{u,v,x\\}$. We have that

$[\theta]_{U}=\mathsf{match}([\theta_{1}]_{U_{1}},[\theta_{2}]_{U_{2}})=[u/r(w_{1},w_{7}),v/r(w_{7},w_{3}),\\\
x/r(w_{1},w_{2},w_{2},w_{3},w_{3}),y/a,z/r(w_{1})]_{U}\enspace,$

with $U=\\{u,v,x,y,z\\}$. At the abstract level, we have
$[S_{1}]_{U_{1}}=\alpha_{\mathrm{\omega}}([\theta_{1}]_{U_{1}})=[x^{2},xz]_{U_{1}}$,
$[S_{2}]_{U_{2}}=\alpha_{\mathrm{\omega}}([\theta_{2}]_{U_{2}})=[uv,ux,vx^{2},x]_{U_{2}}$
and
$[S]_{U}=\alpha_{\mathrm{\omega}}([\theta]_{U})=[uv,uxz,vx^{2},x^{2}]_{U}$.

Note that the new sharing group $uxz$ has the property that its restriction to
$U_{1}$ is in $S_{1}$. More generally, if we abstract $\theta_{1}$ w.r.t. the
variables in $U_{1}$ we get
$\alpha_{\mathrm{\omega}}([\theta]_{U_{1}})=[x^{2},xz]_{U_{1}}$. This is equal
to $[S_{1}]_{U_{1}}$, showing that no new sharing group has been introduced by
the matching operation relatively to the variables in $U_{1}$. Moreover, the
sharing group $uv$, which does not contain variables in $U_{1}$, is brought
unchanged from $S_{2}$ to $S$.

Following the idea presented above, we may design an abstract matching
operation for the domain ${\mathtt{ShLin}^{\omega}}$.

######  Definition 3.4 (Matching over ${\mathtt{ShLin}^{\omega}}$)

Given $[S_{1}]_{U_{1}},[S_{2}]_{U_{2}}\in{\mathtt{ShLin}^{\omega}}$ we define

$\mathsf{match}_{\mathrm{\omega}}([S_{1}]_{U_{1}},[S_{2}]_{U_{2}})=\big{[}S^{\prime}_{2}\cup\big{\\{}X\in\mathscr{P}_{m}(U_{1}\cup
U_{2})\mid\\\ X_{|U_{1}}\in S_{1}\wedge
X_{|U_{2}}\in(S^{\prime\prime}_{2})^{*}\big{\\}}\big{]}_{U_{1}\cup U_{2}}$

where

$S^{\prime}_{2}=\\{B\in S_{2}\mid B_{|U_{1}}=\emptyset\\}\qquad
S^{\prime\prime}_{2}=S_{2}\setminus S^{\prime}_{2}\enspace\qquad
S^{*}=\left\\{\uplus\mathcal{S}\mid\mathcal{S}\in\mathscr{P}_{m}(S)\right\\}\enspace.$

We now show an example of computing the matching over
${\mathtt{ShLin}^{\omega}}$.

###### Example 3.5

Consider $[S_{1}]_{U_{1}}=[x^{2},xz]_{xyz}$ and
$[S_{2}]_{U_{2}}=[uv,ux,vx^{2},x]_{uvx}$ as in Example 3.3. We show that, from
the definition of $\mathsf{match}_{\mathrm{\omega}}$, it holds:

$\mathsf{match}_{\mathrm{\omega}}([S_{1}]_{U_{1}},[S_{2}]_{U_{2}})=[uv,uxz,xz,u^{2}x^{2},ux^{2},vx^{2},x^{2}]_{uvxyz}\enspace.$

First, we have that $S^{\prime}_{2}=\\{uv\\}$ and
$S^{\prime\prime}_{2}=\\{ux,vx^{2},x\\}$. Apart from $uv$, which directly
comes from $S^{\prime}_{2}$, all the other $\omega$-sharing groups in the
result may be obtained by choosing a multiset $\mathcal{M}$ of sharing groups
in $S^{\prime\prime}_{2}$ and summing them together, obtaining
$\uplus\mathcal{M}$. Then, we consider if it is possible to add to
$\uplus\mathcal{M}$ some occurrences of the variables $y$ and $z$, for
instance $n$ occurrences of $y$ and $m$ of $z$, in such a way that
$(\uplus\mathcal{M})\uplus\\{\\!\\!\\{y^{n}z^{m}\\}\\!\\!\\}$ restricted to
$U_{1}$ is a sharing group in $S_{1}$.

We start by considering $\mathcal{M}$ with a single $\omega$-sharing group.

  * •

If $\mathcal{M}=\\{\\!\\!\\{ux\\}\\!\\!\\}$, then $\uplus\mathcal{M}=ux$ but
$(\uplus\mathcal{X})|_{U_{1}}=x\notin S_{1}$. However, we can add the variable
$z$ to get $uxz\in S_{1}$, hence $uxz$ is an $\omega$-sharing group in the
result of $\mathsf{match}_{\mathrm{\omega}}$.

  * •

If $\mathcal{M}=\\{\\!\\!\\{vx^{2}\\}\\!\\!\\}$, then
$\uplus\mathcal{M}=vx^{2}$ and $(\uplus\mathcal{M})|_{U_{1}}=x^{2}$ which is
already an element of $S_{1}$. Therefore, $vx^{2}$ is in the result of
$\mathsf{match}_{\mathrm{\omega}}$.

  * •

If $\mathcal{M}=\\{\\!\\!\\{x\\}\\!\\!\\}$, then $\uplus\mathcal{M}=x$, but
$(\uplus\mathcal{M})|_{U_{1}}=x\notin S_{1}$. However, we can add the variable
$z$ to get $xz\in S_{1}$, hence $xz$ is in the result of
$\mathsf{match}_{\mathrm{\omega}}$.

We now consider the cases when $\mathcal{M}$ has two (possibly equal)
elements. Note that if $\mathcal{M}$ contains $vx^{2}$, it cannot contain
anything else, otherwise $\uplus\mathcal{M}$ would contain at least three
occurrences of $x$, and no sharing group in $S_{1}$ could be matched.
Therefore, the only choices are:

  * •

if $\mathcal{M}=\\{\\!\\!\\{ux,ux\\}\\!\\!\\}$, then
$\uplus\mathcal{M}=u^{2}x^{2}$ and $(\uplus\mathcal{M})|_{U_{1}}=x^{2}$ which
is already in $S_{1}$, hence $u^{2}x^{2}$ is in the result of
$\mathsf{match}_{\mathrm{\omega}}$;

  * •

if $\mathcal{M}=\\{\\!\\!\\{x,x\\}\\!\\!\\}$, then $\uplus\mathcal{M}=x^{2}$
and $(\uplus\mathcal{M})|_{U_{1}}=x^{2}$ which is already in $S_{1}$, hence
$x^{2}$ is in the result of $\mathsf{match}_{\mathrm{\omega}}$;

  * •

if $\mathcal{M}=\\{\\!\\!\\{ux,x\\}\\!\\!\\}$, then $\uplus\mathcal{M}=ux^{2}$
and $(\uplus\mathcal{M})|_{U_{1}}=x^{2}$ which is already in $S_{1}$, hence
$ux^{2}$ is in the result of $\mathsf{match}_{\mathrm{\omega}}$.

In theory, we should also consider the case when $\mathcal{M}$ has more than
two elements, but in the example this would not lead to new results, for the
same reason why $vx^{2}$ may only be used alone.

We will prove that $\mathsf{match}_{\mathrm{\omega}}$ is correct, therefore
comes at no surprise that

$\alpha_{\mathrm{\omega}}(\mathsf{match}([\theta_{1}]_{U_{1}},[\theta_{2}]_{U_{2}}])))=[uv,uxz,vx^{2},x^{2}]_{U}\leq[uv,uxz,xz,u^{2}x^{2},ux^{2},vx^{2},x^{2}]_{U}\enspace.$

The lack of equality means that $\mathsf{match}_{\mathrm{\omega}}$ is not
($\alpha$-)complete (Giacobazzi et al., 2000; Amato and Scozzari, 2011). We
will show later that it is optimal.

We try to give the intuition behind the definition of $\mathsf{match}$,
especially in the context of the backward unification. First note that the
operator is additive on the first argument, namely:

$\mathsf{match}_{\mathrm{\omega}}([S_{1}]_{U_{1}},[S_{2}]_{U_{2}})=\left[\bigcup_{B\in
S_{1}}\mathsf{match}_{\mathrm{\omega}}([\\{B\\}]_{U_{1}},[S_{2}]_{U_{2}})\right]_{U_{1}\cup
U_{2}}$

This immediately implies that we can reason on matching considering one
sharing group at a time. Given a sharing group $B\in S_{1}$, which represents
the exit substitution from a sub-computation, we try to guess which of the
sharing groups in $S_{2}$ are part of the entry substitution which has
generated the sub-computation ended with $B$. In the simple case when
$U_{1}\supseteq U_{2}$, we simply check that $B$ can be generated by the
sharing groups in $S_{2}$, that is, there exists
$\mathcal{S}\in\mathscr{P}_{m}(S_{2})$ such that
$B_{|U_{2}}=\uplus\mathcal{S}$.

The difficult case is when $U_{2}$ contains some variables which are not in
$U_{1}$. These variables come from the call substitution, they are removed
from the abstraction before entering the sub-computation, and now should be
re-introduced as precisely as possible. In this case, we build a new sharing
group $X$ such that $X_{|U_{1}}$ coincides with $B$, and $X_{|U_{2}}$ is
generated by $S_{2}$, namely there exists
$\mathcal{S}\in\mathscr{P}_{m}(S_{2})$ such that
$X_{|U_{2}}=\uplus\mathcal{S}$. This condition ensures that we pair each exit
substitution $\theta_{1}$ (in the concretization of $B$) with some entry
substitution $\theta_{2}$ (in the concretization of $\mathcal{S}$) which is
less instantiated than $\theta_{1}$.

Note that, although the abstract unification operator
$\mathsf{mgu}_{\mathrm{\omega}}$ defined in Amato and Scozzari, (2010) takes
an abstract object and a substitution as inputs, the operator
$\mathsf{match}_{\mathrm{\omega}}$ is designed in such a way that both the
arguments are abstract objects. The reason for this choice is that these are
the variants needed for static analysis of logic programs. However, it would
be possible to devise a variant of $\mathsf{mgu}_{\mathrm{\omega}}$ with two
abstract arguments and variants of $\mathsf{match}_{\mathrm{\omega}}$ with one
abstract argument and a concrete one.

In order to prove correctness of $\mathsf{match}_{\mathrm{\omega}}$, we first
extend the definition of $\theta^{-1}$ to the case when it is applied to a
sharing group $B$, elementwise as

$\theta^{-1}(v_{1}^{i_{1}}\cdots
v_{n}^{i_{n}})=\biguplus\\{\\!\\!\\{(\theta^{-1}(v_{1}))^{i_{1}},\dots,(\theta^{-1}(v_{n}))^{i_{n}}\\}\\!\\!\\}\enspace.$
(7)

It turns out that

$(\eta\circ\theta)^{-1}(B)=\theta^{-1}(\eta^{-1}(B))\enspace,$ (8)

a result which has been proved in Amato and Scozzari, (2010).

###### Example 3.6

Given $\eta=\\{x/s(y,u,y),z/s(u,u),v/u\\}$ and $\theta=\\{v/a,w/s(x,x)\\}$, we
have $\eta\circ\theta=\\{v/a,w/s(s(y,u,y),s(y,u,y)),x/s(y,u,y),z/s(u,u))\\}$
and $(\eta\circ\theta)^{-1}(u)=uw^{2}xz^{2}$. The same result may be obtained
as $\theta^{-1}(\eta^{-1}(u))$, since $\eta^{-1}(u)=uvxz^{2}$ and

$\theta^{-1}(uvxz^{2})=\uplus\\{\\!\\!\\{\theta^{-1}(u),\theta^{-1}(v),\theta^{-1}(x),(\theta^{-1}(z))^{2}\\}\\!\\!\\}=\\\
=\uplus\\{\\!\\!\\{u,\\{\\!\\!\\{\\}\\!\\!\\},xw^{2},(z)^{2}\\}\\!\\!\\}=uw^{2}xz^{2}\enspace.$

######  Theorem 3.7 (Correctness of $\mathsf{match}_{\mathrm{\omega}}$)

$\mathsf{match}_{\mathrm{\omega}}$ is correct w.r.t. $\mathsf{match}$.

######  Proof 3.8.

Given $[S_{1}]_{U_{1}}\rightslice[\theta_{1}]_{U_{1}}$ and
$[S_{2}]_{U_{2}}\rightslice[\theta_{2}]_{U_{2}}$ such that
$\mathsf{match}([\theta_{1}]_{U_{1}},[\theta_{2}]_{U_{2}})$ is defined, we
need to prove that

$\mathsf{match}_{\mathrm{\omega}}([S_{1}]_{U_{1}},[S_{2}]_{U_{2}})\rightslice\mathsf{match}([\theta_{1}]_{U_{1}},[\theta_{2}]_{U_{2}})\enspace.$

Assume without loss of generality that $\mathrm{dom}(\theta_{1})=U_{1}$,
$\mathrm{dom}(\theta_{2})=U_{2}$ and
$\mathrm{vars}(\theta_{1})\cap\mathrm{vars}(\theta_{2})\subseteq U_{1}\cap
U_{2}$. In particular, this implies
$\mathrm{rng}(\theta_{1})\cap\mathrm{rng}(\theta_{2})=\emptyset$. By
hypothesis $\theta_{1}\preceq_{U_{1}\cap U_{2}}\theta_{2}$, i.e., there exists
$\delta\in\mathit{ISubst}$ such that $\theta_{1}(x)=\delta(\theta_{2}(x))$ for
each $x\in U_{1}\cap U_{2}$,
$\mathrm{dom}(\delta)=\mathrm{vars}(\theta_{2}(U_{1}\cap U_{2}))$ and
$\mathrm{rng}(\delta)=\mathrm{vars}(\theta_{1}(U_{1}\cap U_{2}))$. We have

$\displaystyle\mathsf{mgu}(\theta_{1},\theta_{2})$ $\displaystyle=$
$\displaystyle\mathsf{mgu}(\\{\theta_{2}(x)=\theta_{2}(\theta_{1}(x))\mid x\in
U_{1}\\})\circ\theta_{2}$ [by assumptions on the $\theta_{i}$’s]
$\displaystyle=$ $\displaystyle\mathsf{mgu}(\\{\theta_{2}(x)=\theta_{1}(x)\mid
x\in U_{1}\\})\circ\theta_{2}$ $\displaystyle=$
$\displaystyle\mathsf{mgu}(\\{\theta_{2}(x)=\theta_{1}(x)\mid x\in U_{1}\cap
U_{2}\\})\circ(\theta_{1})_{|U_{1}\setminus U_{2}}\circ\theta_{2}$ [since
$\mathrm{vars}(\theta_{2})\cap\mathrm{vars}((\theta_{1})_{U_{1}\setminus
U_{2}})=\emptyset]$ $\displaystyle=$
$\displaystyle\mathsf{mgu}(\\{\theta_{2}(x)=\delta(\theta_{2}(x))\mid x\in
U_{1}\cap U_{2}\\})\circ((\theta_{1})_{|U_{1}\setminus
U_{2}}\uplus\theta_{2})$ $\displaystyle=$
$\displaystyle\delta\circ((\theta_{1})_{|U_{1}\setminus
U_{2}}\uplus\theta_{2})$ [since
$\mathrm{dom}(\delta)\cap\mathrm{vars}((\theta_{1})_{U_{1}\setminus
U_{2}})=\emptyset]$ $\displaystyle=$
$\displaystyle(\theta_{1})_{|U_{1}\setminus
U_{2}}\uplus(\delta\circ\theta_{2})\enspace.$

With an analogous derivation, we obtain

$\mathsf{mgu}(\theta_{1},\theta_{2})=\theta_{1}\uplus(\delta\circ(\theta_{2})_{|U_{2}\setminus
U_{1}})\enspace.$

Now, if $\eta=\mathsf{mgu}(\theta_{1},\theta_{2})$, we need to prove that, for
each $v\in\mathcal{V}$, $\eta^{-1}(v)_{|U_{1}\cup
U_{2}}\in\mathsf{match}_{\mathrm{\omega}}([S_{1}]_{U_{1}},[S_{2}]_{U_{2}})$.
We distinguish several cases.

  * •

$v\notin\mathrm{rng}(\theta_{1})$ and $v\notin\mathrm{rng}(\theta_{2})$. In
this case $v\notin\mathrm{vars}(\delta)$ and $\eta^{-1}(v)_{|U_{1}\cup
U_{2}}=\\{\\!\\!\\{\\}\\!\\!\\}\in\mathsf{match}_{\mathrm{\omega}}([S_{1}]_{U_{1}},[S_{2}]_{U_{2}})$.

  * •

$v\in\mathrm{rng}(\theta_{1})$ and $v\notin\mathrm{vars}(\theta_{1}(U_{2}))$.
In this case $v\notin\mathrm{rng}(\theta_{2})$ and
$v\notin\mathrm{vars}(\delta)$. We have $\eta^{-1}(v)_{|U_{1}\cup
U_{2}}=\theta_{1}^{-1}(v)_{|U_{1}}\in
S_{1}\subseteq\mathsf{match}_{\mathrm{\omega}}([S_{1}]_{U_{1}},[S_{2}]_{U_{2}})$.

  * •

$v\in\mathrm{rng}(\theta_{2})$ and $v\notin\mathrm{vars}(\theta_{2}(U_{1}))$.
In this case $v\notin\mathrm{rng}(\theta_{1})$ and
$v\notin\mathrm{vars}(\delta)$. We have $\eta^{-1}(v)_{|U_{1}\cup
U_{2}}=\theta_{2}^{-1}(v)_{|U_{2}}\in S_{2}$. Since
$v\notin\mathrm{vars}(\theta_{2}(U_{1}))$, then
$\theta_{2}^{-1}(v)_{|U_{2}}\in
S^{\prime}_{2}\subseteq\mathsf{match}_{\mathrm{\omega}}([S_{1}]_{U_{1}},[S_{2}]_{U_{2}})$.

  * •

$v\in\mathrm{vars}(\theta_{2}(U_{1}\cap U_{2}))$. In this case
$v\notin\mathrm{rng}(\theta_{1})$ and $v\in\mathrm{dom}(\delta)$, therefore
$\eta^{-1}(v)_{|U_{1}\cup U_{2}}=\\{\\!\\!\\{\\}\\!\\!\\}$.

  * •

$v\in\mathrm{vars}(\theta_{1}(U_{1}\cap U_{2}))$. Now,
$v\in\mathrm{rng}(\delta)$ and
$\eta^{-1}(v)_{|U_{2}}=\theta_{2}^{-1}(\delta^{-1}(v))_{|U_{2}}=\biguplus X$,
where $X\in\mathscr{P}_{m}(S_{2})$ and each sharing group $B\in X$ is of the
form $\theta_{2}^{-1}(w)_{|U_{2}}$ for some
$w\in\llfloor\delta^{-1}(v)\rrfloor$. Note that every such $w$ is an element
of $\mathrm{vars}(\theta_{2}(U_{1}\cap U_{2}))$, therefore
$\theta_{2}^{-1}(w)_{|U_{2}}\in S^{\prime\prime}_{2}$,
$X\in\mathscr{P}_{m}(S^{\prime\prime}_{2})$ and $\biguplus
X\in(S_{2}^{\prime\prime})^{*}$. On the other side, since
$\eta=\theta_{1}\uplus(\delta\circ(\theta_{2})_{|U_{2}\setminus U_{1}})$, we
have $\eta^{-1}(v)_{|U_{1}}=\theta_{1}^{-1}(v)_{|U_{1}}\in S_{1}$. Hence,
$\eta^{-1}(v)_{|U_{1}\cup
U_{2}}\in\mathsf{match}_{\mathrm{\omega}}([S_{1}]_{U_{1}},[S_{2}]_{U_{2}})$.

This concludes the proof.

Now, we may prove the optimality of $\mathsf{match}_{\mathrm{\omega}}$.
Actually, we prove a stronger property, a sort of weak completeness of
$\mathsf{match}_{\mathrm{\omega}}$, which will be used later to derive
optimality.

######  Example 3.9.

Consider again the substitutions and sharing groups in Examples 3.3 and 3.5.
Recall that $U_{1}=\\{x,y,z\\}$ and $U_{2}=\\{u,v,x\\}$. We have seen that,
although the sharing groups $xz$, $u^{2}x^{2}$, and $ux^{2}$ are in
$\mathsf{match}_{\mathrm{\omega}}([S_{1}]_{U_{1}},[S_{2}]_{U_{2}})$, they are
not in
$\alpha_{\mathrm{\omega}}(\mathsf{match}([\theta_{1}]_{U_{1}},[\theta_{2}]_{U_{2}}))$.
If $\mathsf{match}_{\mathrm{\omega}}$ were optimal, we should be able to find,
for each $B\in\\{xz,u^{2}x^{2},ux^{2}\\}$, a pair of substitutions
$\theta_{3}$ and $\theta_{4}$ such that
$[S_{1}]_{U_{1}}\rightslice[\theta_{3}]_{U_{1}}$,
$[S_{2}]_{U_{2}}\rightslice[\theta_{4}]_{U_{2}}$ and
$B\in\alpha_{\mathrm{\omega}}(\mathsf{match}([\theta_{3}]_{U_{1}},[\theta_{4}]_{U_{2}})$.
Actually, we can do better, keep $\theta_{4}=\theta_{2}$ fixed, and only
change $\theta_{3}$ for different sharing groups.

Consider $B=xz$. Note that $B_{|U_{1}}=xz$ and
$B_{|U_{2}}=x=\biguplus\mathcal{X}$, with
$\mathcal{X}=\\{\\!\\!\\{x\\}\\!\\!\\}$. The sharing group $x$ in $\theta_{2}$
is generated by the variables $w_{5}$ and $w_{6}$. Consider the substitution
$\theta_{3}=\\{x/r(a,w,a,a,a),y/a,z/w\\}$ where

  * •

the binding $x/r(a,w,a,a,a)$ is obtained by the corresponding binding in
$\theta_{2}$ replacing $w_{5}$ with a fresh variable $w$ and all the other
variables in the range with the constant symbol $a$;

  * •

the bindings $\\{y/a,z/w\\}$ are chosen according to $B_{|U_{1}\setminus
U_{2}}=z$.

It is immediate to show that
$xz\in\alpha_{\mathrm{\omega}}(\mathsf{mgu}([\theta_{3}]_{U_{1}},[\theta_{2}]_{U_{2}}))$
and $[S_{1}]_{U_{1}}\rightslice[\theta_{3}]_{U_{1}}$.

As an another example, let us consider $B=u^{2}x^{2}$. In this case
$B_{|U_{1}}=x^{2}\in S_{1}$ and
$B_{|U_{2}}=u^{2}x^{2}=\biguplus\\{\\!\\!\\{ux,ux\\}\\!\\!\\}$. The variable
which generates the sharing group $ux$ is $w_{4}$. We proceed as before, and
obtain $\theta_{3}=\\{x/r(r(w,w),a,a,a,a),y/a,z/a\\}$. Note that $w_{4}$ has
been replaced with $r(w,w)$ since two copies of $ux$ are needed to obtain
$u^{2}x^{2}$. Again $[S_{1}]_{U_{1}}\rightslice[\theta_{3}]_{U_{1}}$ and
$u^{2}x^{2}\in\alpha_{\mathrm{\omega}}(\mathsf{mgu}([\theta_{3}]_{U_{1}},[\theta_{2}]_{U_{2}}))$.

We distill the idea presented above in the following result.

######  Lemma 3.10 (Completeness on the second argument).

Given $[S_{1}]_{U_{1}}\in{\mathtt{ShLin}^{\omega}}$ and
$[\theta_{2}]_{U_{2}}\in\mathit{ISubst}_{\sim}$, there exist
$\delta_{1},\dots,\delta_{n}\in\mathit{ISubst}_{\sim}$ such that for all
$i\in\\{1,\dots,n\\}$, $[S_{1}]_{U_{1}}\rightslice[\delta_{i}]_{U_{1}}$ and

$\mathsf{match}_{\mathrm{\omega}}([S_{1}]_{U_{1}},\alpha_{\mathrm{\omega}}([\theta_{2}]_{U_{2}}))=\left[\bigcup_{i\in\\{1,\ldots,n\\}}\alpha_{\omega}(\mathsf{match}([\delta_{i}]_{U_{1}},[\theta_{2}]_{U_{2}}))\right]_{U_{1}\cup
U_{2}}$

######  Proof 3.11.

Since we already know that $\mathsf{match}_{\mathrm{\omega}}$ is a correct
abstraction of $\mathsf{match}$, we only need to prove that, given
$[S_{1}]_{U_{1}}\in{\mathtt{ShLin}^{\omega}}$ and
$[\theta_{2}]_{U_{2}}\in\mathit{ISubst}_{\sim}$, for any sharing group
$B\in\mathsf{match}_{\mathrm{\omega}}([S_{1}]_{U_{1}},\alpha_{\mathrm{\omega}}([\theta_{2}]_{U_{2}}))$,
there exists $[\theta_{1}]_{U_{1}}\in\mathit{ISubst}_{\sim}$ such that
$[S_{1}]_{U_{1}}\rightslice[\theta_{1}]_{U_{1}}$ and
$B\in\alpha_{\mathrm{\omega}}(\mathsf{match}([\theta_{1}]_{U_{1}},[\theta_{2}]_{U_{2}}))$.

In order to ease notation, let $U=U_{1}\cup U_{2}$,
$[S_{2}]_{U_{2}}=\alpha_{\mathrm{\omega}}([\theta_{2}]_{U_{2}})$ and
$[S]_{U}=\mathsf{match}_{\mathrm{\omega}}([S_{1}]_{U_{1}},[S_{2}]_{U_{2}})$.
We may choose $\theta_{2}$ such that $\mathrm{dom}(\theta_{2})=U_{2}$ without
loss of generality. Moreover, $S^{\prime}_{2}$ and $S^{\prime\prime}_{2}$ are
given as in the definition of abstract matching. We distinguish two cases.

first case)

If $B\in S^{\prime}_{2}$, there exists $v\in\mathcal{V}$ such that
$\theta_{2}^{-1}(v)_{|U_{2}}=B$. Let $X=\mathrm{vars}(\theta_{2}(U_{1}\cap
U_{2}))$ and take $\delta=\\{x/a\mid x\in X\\}$. Then
$\theta_{1}=(\delta\circ\theta_{2})_{|U_{1}}\uplus\\{x/a\mid x\in
U_{1}\setminus U_{2}\\}$ is such that
$\theta_{1}^{-1}(v)_{|U_{1}}=\\{\\!\\!\\{\\}\\!\\!\\}$ for each
$v\in\mathcal{V}$, therefore $[S_{1}]_{U_{1}}\rightslice[\theta_{1}]_{U_{1}}$.
Moreover, since $\theta_{1}\preceq_{U_{1}\cap U_{2}}\theta_{2}$, we have that
$\mathsf{match}_{\mathrm{\omega}}([\theta_{1}]_{U_{1}},[\theta_{2}]_{U_{2}})$
is defined equal to $\mathsf{mgu}([\theta_{1}]_{U_{1}},[\theta_{2}]_{U_{2}})$
and
$\mathsf{mgu}([\theta_{1}]_{U_{1}},[\theta_{2}]_{U_{2}})=[\mathsf{mgu}(\theta_{1},\theta_{2})]_{U}$
since $\mathrm{vars}(\theta_{1})\cap\mathrm{vars}(\theta_{2})\subseteq
U_{1}\cap U_{2}$. By the proof of Theorem 3.7, we have that
$\mathsf{mgu}(\theta_{1},\theta_{2})=(\theta_{1})_{|U_{1}\setminus
U_{2}}\uplus(\delta\circ\theta_{2})$. Since
$B_{|U_{1}}=\\{\\!\\!\\{\\}\\!\\!\\}$, then $v\notin X=\mathrm{vars}(\delta)$,
and therefore
$\mathsf{mgu}(\theta_{1},\theta_{2})^{-1}(v)_{|U}=\theta_{2}^{-1}(v)_{|U}=B$.
Hence, $B$ is an $\omega$-sharing group in
$\alpha_{\mathrm{\omega}}(\mathsf{match}([\theta_{1}]_{U_{1}},[\theta_{2}]_{U_{2}}))$
which is what we wanted to prove.

second case)

We now assume $B_{|U_{1}}\in S_{1}$ and $B_{|U_{2}}=\biguplus X$ with
$\mathcal{X}\in\mathscr{P}_{m}(S^{\prime\prime}_{2})$. Then, for each
$H\in\llfloor\mathcal{X}\rrfloor$, there exists $v_{H}\in\mathcal{V}$ such
that $\theta_{2}^{-1}(v_{H})_{|U_{2}}=H$. Since $H\cap
U_{1}\neq\\{\\!\\!\\{\\}\\!\\!\\}$ for each $H\in\llfloor\mathcal{X}\rrfloor$,
then $v_{H}\in Y=\mathrm{vars}(\theta_{2}(U_{1}\cap U_{2}))$. Consider the
substitutions

$\displaystyle\delta$
$\displaystyle=\\{v_{H}/t(\underbrace{v,\ldots,v}_{\text{$\mathcal{X}(H)$
times}})\mid H\in\llfloor\mathcal{X}\rrfloor\\}\uplus\\{y/a\mid y\in Y\text{
and }\forall H\in\llfloor\mathcal{X}\rrfloor.y\neq v_{H}\\}\enspace,$
$\displaystyle\eta$
$\displaystyle=\\{w/t(\underbrace{v,\ldots,v}_{\text{$B(w)$ times}})\mid w\in
U_{1}\setminus U_{2}\\}\enspace,$

for a fresh variable $v$. Let us define
$\theta_{1}=\eta\uplus(\delta\circ\theta_{2})_{|U_{1}}$. We want to prove that
$[S_{1}]_{U_{1}}\rightslice[\theta_{1}]_{U_{1}}$. Note that
$\mathrm{vars}(\theta_{1}(U_{1}))=\\{v\\}$, hence we only need to check that
$\theta^{-1}_{1}(v)_{|U_{1}}\in S_{1}$. We have that
$\theta^{-1}(v)_{|U_{1}}=\eta^{-1}(v)_{|U_{1}}\uplus(\theta_{2}^{-1}\delta^{-1}(v))_{|U_{1}}=\eta^{-1}(v)_{|U_{1}}\uplus\theta_{2}^{-1}(\\{\\!\\!\\{v_{H}^{X(H)}\mid
H\in\llfloor\mathcal{X}\rrfloor\\}\\!\\!\\})_{|U_{1}}=B_{|U_{1}\setminus
U_{2}}\uplus(\biguplus\mathcal{X})_{|U_{1}\cap U_{2}}=B_{|U_{1}}\uplus
B_{|U_{1}\cap U_{2}}=B_{|U_{1}}$ which, we know, is an element of $S_{1}$.
Moreover, since $\theta_{1}\preceq_{U_{1}\cap U_{2}}\theta_{2}$ and
$\mathrm{vars}(\theta_{1})\cap\mathrm{vars}(\theta_{2})\subseteq U_{1}\cap
U_{2}$, we have that
$\mathsf{match}_{\mathrm{\omega}}([\theta_{1}]_{U_{1}},[\theta_{2}]_{U_{2}})=[\mathsf{mgu}(\theta_{1},\theta_{2})]_{U}$.
If we define $\theta=\mathsf{mgu}(\theta_{1},\theta_{2})$, by looking at the
proof of Theorem 3.7 we have that
$\theta=\theta_{1}\uplus(\delta\circ(\theta_{2})_{|U_{2}\setminus U_{1}})$ and
$\theta=(\theta_{1})_{|U_{1}\setminus U_{2}}\uplus(\delta\circ\theta_{2})$. By
the first equality, it is immediate to check that
$\theta^{-1}(v)_{|U_{1}}=\theta_{1}^{-1}(v)_{|U_{1}}=B_{|U_{1}}$. By the
second equality,
$\theta^{-1}(v)_{|U_{2}}=\theta_{2}^{-1}(\\{\\!\\!\\{v_{H}^{\mathcal{X}(H)}\mid
H\in\llfloor\mathcal{X}\rrfloor\\}\\!\\!\\})_{|U_{2}}=\biguplus\mathcal{X}=B_{|U_{2}}$.
Therefore, $\theta^{-1}(v)_{|U}=B$.

It is worth noting that, although this proof uses a function symbol of
arbitrary arity, it may be easily rewritten using only one constant symbol and
one function symbol of arity at least two, as required at the beginning of
Section 2.

######  Theorem 3.12 (Optimality of $\mathsf{match}_{\mathrm{\omega}}$).

The operation $\mathsf{match}_{\mathrm{\omega}}$ is optimal w.r.t.
$\mathsf{match}$.

######  Proof 3.13.

It is enough to prove that for each
$[S_{1}]_{U_{1}},[S_{2}]_{U_{2}}\in{\mathtt{ShLin}^{\omega}}$ and
$B\in\mathsf{match}_{\mathrm{\omega}}([S_{1}]_{U_{1}},[S_{2}]_{U_{2}})$, there
are substitutions $\theta_{1}$, $\theta_{2}$ such that
$[S_{1}]_{U_{1}}\rightslice[\theta_{1}]_{U_{1}}$,
$[S_{2}]_{U_{2}1}\rightslice[\theta_{2}]_{U_{2}}$ and
$B\in\alpha_{\mathrm{\omega}}(\mathsf{match}([\theta_{1}]_{U_{1}},[\theta_{2}]_{U_{2}})$.
Assume $B_{|U_{2}}=\biguplus\mathcal{X}$ where
$\mathcal{X}\in\mathscr{P}_{m}(S^{\prime\prime}_{2})$. Consider a substitution
$[\theta_{2}]_{U_{2}}$ such that
$[\llfloor\mathcal{X}\rrfloor]_{U_{2}}\leq\alpha_{\mathrm{\omega}}([\theta_{2}]_{U_{2}})\leq[S_{2}]_{U_{2}}$.
It means that, for each $H\in\llfloor\mathcal{X}\rrfloor$, there is
$v_{H}\in\mathcal{V}$ such that $\theta_{2}^{-1}(v_{H})_{|U_{2}}=H$. If
$\llfloor\mathcal{X}\rrfloor=\\{H_{1},\ldots,H_{n}\\}$, we may define
$\theta_{2}$ as the substitution with $\mathrm{dom}(\theta_{2})=U_{2}$ and,
for each $u\in U_{2}$,

$\theta_{2}(u)=t(\underbrace{v_{H_{1}},\ldots,v_{H_{1}}}_{H_{1}(u)\text{
times}},\underbrace{v_{H_{2}},\ldots,v_{H_{2}}}_{H_{2}(u)\text{
times}},\ldots,\underbrace{v_{H_{n}},\ldots,v_{H_{n}}}_{H_{n}(u)\text{
times}})\enspace.$

By Lemma 3.10, there exists $[\theta_{1}]_{U_{1}}$ such that
$[S_{1}]_{U_{1}}\rightslice[\theta_{1}]_{U_{1}}$ and
$B\in\alpha_{\mathrm{\omega}}(\mathsf{match}([\theta_{1}]_{U_{1}},[\theta_{2}]_{U_{2}}))$.
Therefore, $\mathsf{match}_{\mathrm{\omega}}$ is the optimal approximation of
$\mathsf{match}$.

##  4 Abstract matching over ${\mathtt{ShLin}^{2}}$

The domain ${\mathtt{ShLin}^{\omega}}$ has been inspired by the domain
${\mathtt{ShLin}^{2}}$, appeared for the first time in King, (1994). The
novelty of ${\mathtt{ShLin}^{2}}$ was to embed linearity information inside
the sharing groups, instead of keeping them separate like it was in
$\mathtt{Sharing}\times\mathtt{Lin}$.

###  4.1 The domain ${\mathtt{ShLin}^{2}}$

Here we recall the main definitions for the domain ${\mathtt{ShLin}^{2}}$,
viewed as an abstraction of ${\mathtt{ShLin}^{\omega}}$, following the
presentation given in Amato and Scozzari, (2010).

The idea is to simplify the domain ${\mathtt{ShLin}^{\omega}}$ by only
recording whether a variable in a sharing group is linear or not, but
forgetting its actual multiplicity. Intuitively, we abstract an
$\omega$-sharing group by replacing any exponent equal to or greater than $2$
with a new symbol $\infty$.

A _2-sharing group_ is a map $o:\mathcal{V}\rightarrow\\{0,1,\infty\\}$ such
that its support $\llfloor o\rrfloor=\\{v\in\mathcal{V}\mid o(v)\neq 0\\}$ is
finite. We use a polynomial notation for 2-sharing groups as for
$\omega$-sharing groups. For instance, $o=xy^{\infty}z$ denotes the 2-sharing
group whose support is $\llfloor o\rrfloor=\\{x,y,z\\}$, such that
$o(x)=o(z)=1$ and $o(y)=\infty$. We denote with $\emptyset$ the 2-sharing
group with empty support and by ${\mathit{Sg}^{2}}(V)$ the set of 2-sharing
groups whose support is a subset of $V$. Note that in King, (1994) the number
$2$ is used as an exponent instead of $\infty$, but we prefer our notation to
be coherent with $\omega$-sharing groups.

An $\omega$-sharing group $B$ may be abstracted into the 2-sharing group
$\alpha_{\mathrm{2}}(B)$ given by

$\alpha_{\mathrm{2}}(B)=\lambda v\in\mathcal{V}.\begin{cases}B(v)&\text{if
$B(v)\leq 1$,}\\\ \infty&\text{otherwise.}\end{cases}$ (9)

For instance, the $\omega$-sharing groups
$xy^{2}z,xy^{3}z,xy^{4}z,xy^{5}z,\ldots$ are all abstracted into
$xy^{\infty}z$.

There are operations on 2-sharing groups which correspond to variable
projection and multiset union. For projection

$o_{|V}=\lambda v\in\mathcal{V}.\begin{cases}o(V)&\text{if $v\in V$,}\\\
0&\text{otherwise,}\end{cases}$ (10)

while for multiset union

$o\uplus o^{\prime}=\lambda v\in\mathcal{V}.o(v)\oplus o^{\prime}(v)\enspace,$
(11)

where $0\oplus x=x\oplus 0=x$ and $\infty\oplus x=x\oplus\infty=1\oplus
1=\infty$. We will use $\biguplus\\{\\!\\!\\{o_{1},\ldots,o_{n}\\}\\!\\!\\}$
for $o_{1}\uplus\cdots\uplus o_{n}$. Given a sharing group $o$, we also define
the _delinearization_ operator:

$o^{2}=o\uplus o\enspace.$ (12)

This operator is extended pointwise to sets and multisets. The next
proposition shows some properties of these operators.

######  Proposition 4.1.

Given an $\mathrm{\omega}$-sharing group $B$, a set of variables $V$ and
multiset of $\omega$-sharing groups $\mathcal{X}$, the following properties
hold:

  1. 1.

$\llfloor B\rrfloor=\llfloor\alpha_{\mathrm{2}}(B)\rrfloor$

  2. 2.

$\alpha_{\mathrm{2}}(B_{|V})=\alpha_{\mathrm{2}}(B)_{|V}$

  3. 3.

$\alpha_{\mathrm{2}}(\biguplus\mathcal{X})=\biguplus\alpha_{\mathrm{2}}(\mathcal{X})$

  4. 4.

$\alpha_{\mathrm{2}}(B\uplus B)=\alpha_{\mathrm{2}}(B)^{2}$

where $\alpha_{\mathrm{2}}(\mathcal{X})$ is just the elementwise extension of
$\alpha_{\mathrm{2}}$ to a multiset of $\omega$-sharing groups.

######  Proof 4.2.

Given the $\omega$-sharing group $B$, we have
$\llfloor\alpha_{\mathrm{2}}(B)\rrfloor=\\{x\in\mathcal{V}\mid\alpha_{\mathrm{2}}(B)\neq
0\\}=\\{x\in\mathcal{V}\mid B(x)\neq 0\\}=\llfloor B\rrfloor$, which proves
Property 1. For the Property 2, given $V\subseteq\mathcal{V}$, we want to
prove that $\alpha_{\mathrm{2}}(B_{|V})(v)=(\alpha_{\mathrm{2}}(B)_{|V})(v)$
for each $v\in\mathcal{V}$. The property is easily proved considering the
three cases $v\notin V$, $v\in V\setminus\llfloor B\rrfloor$ and $v\in
V\cap\llfloor B\rrfloor$. Property 3 has been proved in Amato and Scozzari,
(2010). Property 4 is a trivial consequence of Property 3.

Since we do not want to represent definite non-linearity, we introduce an
order relation over sharing groups as follows:

$o\leq o^{\prime}\iff\llfloor o\rrfloor=\llfloor
o^{\prime}\rrfloor\wedge\forall x\in\llfloor o\rrfloor.\ o(x)\leq
o^{\prime}(x)\enspace,$

and we restrict our attention to downward closed sets of sharing groups. The
domain we are interested in is the following:

${\mathtt{ShLin}^{2}}=\bigl{\\{}[T]_{U}\mid
T\in\mathscr{P}_{{\mathop{\downarrow}}}({\mathit{Sg}^{2}}(U)),U\in\mathscr{P}_{f}(\mathcal{V}),T\neq\emptyset\Rightarrow\emptyset\in
T\bigr{\\}}\enspace,$

where $\mathscr{P}_{{\mathop{\downarrow}}}({\mathit{Sg}^{2}}(U))$ is the
powerset of downward closed subsets of ${\mathit{Sg}^{2}}(U)$ according to
$\leq$ and $[T_{1}]_{U_{1}}\leq_{\mathrm{2}}[T_{2}]_{U_{2}}$ iff $U_{1}=U_{2}$
and $T_{1}\subseteq T_{2}$. For instance, the set $\\{xy^{\infty}z\\}$ is not
downward closed, while $\\{xyz,xy^{\infty}z\\}$ is downward closed. There is a
Galois insertion of ${\mathtt{ShLin}^{2}}$ into ${\mathtt{ShLin}^{\omega}}$
given by the pair of adjoint maps
$\gamma_{\mathrm{2}}:{\mathtt{ShLin}^{2}}\rightarrow{\mathtt{ShLin}^{\omega}}$
and
$\alpha_{\mathrm{2}}:{\mathtt{ShLin}^{\omega}}\rightarrow{\mathtt{ShLin}^{2}}$:

$\displaystyle\gamma_{\mathrm{2}}([T]_{U})=\left[\alpha_{\mathrm{2}}^{-1}(T)\right]_{U}\qquad\alpha_{\mathrm{2}}([S]_{U})=\left[{\mathop{\downarrow}}\alpha_{\mathrm{2}}(S)\right]_{U}\enspace,$

where ${\mathop{\downarrow}}T=\\{o\mid o^{\prime}\in T,o\leq o^{\prime}\\}$ is
the downward closure of $T$. With an abuse of notation, we also apply
$\gamma_{\mathrm{2}}$ and $\alpha_{\mathrm{2}}$ to subsets of $\omega$-sharing
groups and 2-sharing groups respectively, by ignoring the set of variables of
interest. For instance,
$\gamma_{\mathrm{2}}([\emptyset,xyz,xy^{\infty}z]_{x,y,z})=[\\{\\!\\!\\{\\}\\!\\!\\},xyz,xy^{2}z,xy^{3}z,xy^{4}z,xy^{5}z,\ldots]_{x,y,z}$.
Moreover, we write ${\mathop{\downarrow}}[S]_{U}$ as an alternative form for
$[{\mathop{\downarrow}}S]_{U}$.

######  Example 4.3.

Consider the substitution
$[\theta]_{U}=[\\{x/s(y,u,y),z/s(u,u),v/u\\}]_{w,x,y,z}$ in the Example 3.2.
Its abstraction in ${\mathtt{ShLin}^{2}}$ is given by

$\alpha_{\mathrm{2}}(\alpha_{\mathrm{\omega}}([\theta]_{U}))=[\\{xy,x^{\infty}y,xz,xz^{\infty},w\\}]_{U}=[{\mathop{\downarrow}}\\{x^{\infty}y,xz^{\infty},w\\}]_{U}\enspace.$

Analogously, substitutions
$[\theta_{1}]_{U_{1}}=[\\{x/r(w_{1},w_{2},w_{2},w_{3},w_{3}),y/a,z/r(w_{1})\\}]_{x,y,z}$
and
$[\theta_{2}]_{U_{2}}=[\\{x/r(w_{4},w_{5},w_{6},w_{8},w_{8}),u/r(w_{4},w_{7}),v/r(w_{7},w_{8})\\}]_{u,v,x}$
from Example 3.3 are abstracted into
$[T_{1}]_{U_{1}}={\mathop{\downarrow}}[x^{\infty},xz]_{U_{1}}$ and
$[T_{2}]_{U_{2}}={\mathop{\downarrow}}[uv,ux,vx^{\infty},x]_{U_{2}}$
respectively.

###  4.2 Matching operator

By composition, $\alpha_{\mathrm{2}}\circ\alpha_{\mathrm{\omega}}$ is an
abstraction from $\mathit{ISubst}_{\sim}$ to ${\mathtt{ShLin}^{2}}$.
Properties of the Galois connection
$\langle\alpha_{\mathrm{2}},\gamma_{\mathrm{2}}\rangle$ may be lifted to
properties of $\alpha_{\mathrm{2}}\circ\alpha_{\mathrm{\omega}}$. In our case,
we need to define an abstract matching $\mathsf{match}_{\mathrm{2}}$ over
${\mathtt{ShLin}^{2}}$ which is optimal w.r.t. $\mathsf{match}$. However,
optimality of $\mathsf{match}_{\mathrm{2}}$ w.r.t. $\mathsf{match}$ is
immediately derived by optimality w.r.t. $\mathsf{match}_{\mathrm{\omega}}$.
Since the correspondence between ${\mathtt{ShLin}^{\omega}}$ and
${\mathtt{ShLin}^{2}}$ is straightforward, the same happens for
$\mathsf{match}_{\mathrm{\omega}}$ and $\mathsf{match}_{\mathrm{2}}$.

######  Definition 4.4 (Matching over ${\mathtt{ShLin}^{2}}$).

Given $[T_{1}]_{U_{1}},[T_{2}]_{U_{2}}\in{\mathtt{ShLin}^{2}}$, we define

$\mathsf{match}_{\mathrm{2}}([T_{1}]_{U_{1}},[T_{2}]_{U_{2}})=\bigl{[}T^{\prime}_{2}\cup{\mathop{\downarrow}}\bigl{\\{}o\in{\mathit{Sg}^{2}}(\mathcal{V})\mid
o_{|U_{1}}\in T_{1}\wedge
o_{|U_{2}}\in(T^{\prime\prime}_{2})^{*}\bigr{\\}}\bigr{]}_{U_{1}\cup U_{2}}$

where $T^{\prime}_{2}=\\{B\in T_{2}\mid B_{|U_{1}}=\emptyset\\}$,
$T^{\prime\prime}_{2}=T_{2}\setminus T^{\prime}_{2}$ and $T^{*}=\\{\biguplus
X\mid X\subseteq T\cup T^{2}\\}$.

######  Example 4.5.

Under the hypothesis of Examples 3.5 and 4.3, and according to the definition
of $\mathsf{match}_{\mathrm{2}}$, we have that $T^{\prime}_{2}=\\{uv\\}$,
$T^{\prime\prime}_{2}=\\{ux,vx,vx^{\infty},x\\}$ and

$\mathsf{match}_{\mathrm{2}}([T_{1}]_{U_{1}},[T_{2}]_{U_{2}})={\mathop{\downarrow}}[uv,u^{\infty}v^{\infty}x^{\infty},uxz,u^{\infty}x^{\infty},v^{\infty}x^{\infty},vxz,x^{\infty},xz]_{u,v,x,y,z}\enspace.$

Note that

$\alpha_{\mathrm{2}}(\mathsf{match}_{\mathrm{\omega}}([S_{1}]_{U_{1}},[S_{2}]_{U_{2}}))={\mathop{\downarrow}}[uv,u^{\infty}x^{\infty},uxz,vx^{\infty},x^{\infty},xz]_{u,v,x,y,z}\\\
\leq\mathsf{match}_{\mathrm{2}}([T_{1}]_{U_{1}},[T_{2}]_{U_{2}})\enspace.$

This is consistent with the fact that $\mathsf{match}_{\mathrm{2}}$ is correct
w.r.t. $\mathsf{match}_{\mathrm{\omega}}$. The 2-sharing groups
$u^{\infty}v^{\infty}x^{\infty}$, $v^{\infty}x^{\infty}$ and $vxz$ do not
appear in
$\alpha_{\mathrm{2}}(\mathsf{match}_{\mathrm{\omega}}([S_{1}]_{U_{1}},[S_{2}]_{U_{2}}))$
since $\mathsf{match}_{\mathrm{2}}$ is not complete w.r.t.
$\mathsf{match}_{\mathrm{\omega}}$

As anticipated before, we prove optimality of $\mathsf{match}_{\mathrm{2}}$
w.r.t. $\mathsf{match}_{\mathrm{\omega}}$, which automatically entails
optimality w.r.t. $\mathsf{match}$.

######  Theorem 4.6 (Correctness and optimality of
$\mathsf{match}_{\mathrm{2}}$).

The operator $\mathsf{match}_{\mathrm{2}}$ is correct and optimal w.r.t.
$\mathsf{match}_{\mathrm{\omega}}$.

######  Proof 4.7.

We need to prove that, for each
$[T_{1}]_{U_{1}},[T_{2}]_{U_{2}}\in{\mathtt{ShLin}^{2}}$,

$\mathsf{match}_{\mathrm{2}}([T_{1}]_{U_{1}},[T_{2}]_{U_{2}})=\alpha_{\mathrm{2}}(\mathsf{match}_{\mathrm{\omega}}(\gamma_{\mathrm{2}}([T_{1}]_{U_{1}}),\gamma_{\mathrm{2}}([T_{2}]_{U_{2}})))\enspace.$
(13)

To ease notation, we denote $\gamma_{\mathrm{2}}([T_{1}]_{U_{1}})$ and
$\gamma_{\mathrm{2}}([T_{2}]_{U_{2}})$ by $[S_{1}]_{U_{1}}$ and
$[S_{2}]_{U_{2}}$ respectively. Moreover, we denote with $S^{\prime}_{2}$,
$S^{\prime\prime}_{2}$, $T^{\prime}_{2}$ and $T^{\prime\prime}_{2}$ the
subsets of $S_{2}$ and $T_{2}$ given accordingly to Definitions 3.4 and 4.4.
Since $\llfloor B\rrfloor=\llfloor\alpha_{\mathrm{2}}(B)\rrfloor$, given $B\in
S_{2}$ we have that $B\in S_{2}^{\prime}$ iff $\alpha_{\mathrm{2}}(B)\in
T_{2}^{\prime}$.

Let $o\in\mathsf{match}_{\mathrm{2}}([T_{1}]_{U_{1}},[T_{2}]_{U_{2}})$. If
$o\in T^{\prime}_{2}$, consider any $B\in\alpha^{-1}_{\mathrm{2}}(o)\subseteq
S_{2}$. Then, $B\in
S^{\prime}_{2}\subseteq\mathsf{match}_{\mathrm{\omega}}([S_{1}]_{U_{1}},[S_{2}]_{U_{2}})$.
Therefore, $o=\alpha_{\mathrm{2}}(B)$ is in the right-hand side of (13). If
$o\notin T^{\prime}_{2}$ then $o\leq o^{\prime}$ where $o^{\prime}_{|U_{1}}\in
T_{1}$ and $o^{\prime}_{|U_{2}}\in(T^{\prime\prime}_{2})^{*}$, i.e., there is
$X\subseteq T^{\prime\prime}_{2}\cup(T^{\prime\prime}_{2})^{2}$ such that
$o^{\prime}_{|U_{2}}=\biguplus X$. For each $o^{\prime\prime}\in X\cap T_{2}$,
let $B_{o^{\prime\prime}}\in\alpha^{-1}_{\mathrm{2}}(o^{\prime\prime})$. For
each $o^{\prime\prime}\in X\setminus T_{2}$, we have
$o^{\prime\prime}=(o^{\prime\prime\prime})^{2}$ for some
$o^{\prime\prime\prime}\in T_{2}$, and let
$B_{o^{\prime\prime}}\in\alpha^{-1}_{\mathrm{2}}(o^{\prime\prime\prime})$. Let
$\mathcal{X}$ be a multiset containing a single copy of each
$B^{\prime\prime}_{o}$ for $o\in X\cap T_{2}$ and two copies of
$B^{\prime\prime}_{o}$ for each $o\in X\setminus T_{2}$, e.g.,
$\mathcal{X}=\\{\\!\\!\\{B_{o^{\prime\prime}}\mid o^{\prime\prime}\in X\cap
T_{2}\\}\\!\\!\\}\uplus\biguplus\\{\\!\\!\\{\\{\\!\\!\\{B_{o^{\prime\prime}},B_{o^{\prime\prime}}\\}\\!\\!\\}\mid
o^{\prime\prime}\in X\setminus T_{2}\\}\\!\\!\\})$. Note that
$\alpha_{\mathrm{2}}(\biguplus\mathcal{X})=\biguplus\alpha_{2}(X)=o^{\prime}_{|U_{2}}$
by (3) of Proposition 4.1. Then, consider the $\omega$-sharing group $C$ such
that

$C(v)=\begin{cases}(\biguplus\mathcal{X})(v)&\text{for $v\in U_{2}$,}\\\
o^{\prime}(v)&\text{if $v\in U_{1}\setminus U_{2}$ and $o(v)\leq 1$,}\\\
2&\text{otherwise}.\end{cases}$

It is clear that $\alpha_{\mathrm{2}}(C_{|U_{1}})=o^{\prime}_{|U_{1}}$, hence
$C_{|U_{1}}\in S_{1}$. Moreover, $C_{|U_{2}}=\biguplus X$ with
$\mathcal{X}\in\mathscr{P}_{m}(S_{2}^{\prime\prime})$. Therefore, we have
$C\in\mathsf{match}_{\mathrm{\omega}}([T_{1}]_{U_{1}},[T_{2}]_{U_{2}})$ and
$\alpha_{\mathrm{2}}(C)=o^{\prime}$ is in the right-hand side of (13). The
same holds for $o$ by downward closure of $\alpha_{\mathrm{2}}$.

Conversely, let
$o\in\alpha_{\mathrm{2}}(\mathsf{match}_{\mathrm{\omega}}([S_{1}]_{U_{1}},[S_{2}]_{U_{2}}))$.
As a consequence, there exists
$B\in\mathsf{match}_{\mathrm{\omega}}([S_{1}]_{U_{1}},[S_{2}]_{U_{2}})$ such
that $o\leq o^{\prime}$ and $o^{\prime}=\alpha_{\mathrm{2}}(B)$. It is enough
to prove that
$o^{\prime}\in\mathsf{match}_{\mathrm{2}}([T_{1}]_{U_{1}},[T_{2}]_{U_{2}})$.
If $B\in S^{\prime}_{2}$ then $o^{\prime}\in T^{\prime}_{2}$, hence
$o^{\prime}\in\mathsf{match}_{\mathrm{2}}([T_{1}]_{U_{1}},[T_{2}]_{U_{2}})$.
If $B\notin S^{\prime}_{2}$, then $B_{|U_{1}}\in S_{1}$ and
$B_{|U_{2}}=\biguplus\mathcal{X}$ where
$\mathcal{X}\in\mathscr{P}_{m}(S^{\prime\prime}_{2})$. By $B_{|U_{1}}\in
S_{1}$ we have $o^{\prime}_{|U_{1}}=\alpha_{\mathrm{2}}(B_{|U_{1}})\in T_{1}$.
For each $C\in\mathcal{X}$ with $\mathcal{X}(C)=1$, we define
$o_{C}=\alpha_{\mathrm{2}}(C)\in T^{\prime\prime}_{2}$, while for each $C$
with $\mathcal{X}(C)>1$, we define
$o_{C}=\alpha_{\mathrm{2}}(C)^{2}\in(T^{\prime\prime}_{2})^{2}$. We have that
$o^{\prime\prime}_{|U_{2}}=\alpha_{\mathrm{2}}(B)_{|U_{2}}=\alpha_{\mathrm{2}}(B_{|U_{2}})=\alpha_{\mathrm{2}}(\biguplus\mathcal{X})=\biguplus
X$ where $X=\\{o_{C}\mid C\in\mathcal{X}\\}$ is an element of
$\mathscr{P}(T^{\prime\prime}_{2}\cup(T^{\prime\prime}_{2})^{2})$. This means
that
$o^{\prime}\in\mathsf{match}_{\mathrm{2}}([T_{1}]_{U_{1}},[T_{2}]_{U_{2}})$.

Although $\mathsf{match}_{\mathrm{2}}$ is not complete w.r.t. either
$\mathsf{match}_{\mathrm{\omega}}$ or $\mathsf{match}$, we claim it enjoys a
property analogous to the one in Lemma 3.10.

###  4.3 Optimization

In a real implementation, we would like to encode an element of
${\mathtt{ShLin}^{2}}$ with the set of its maximal elements. This works well
only if we may compute $\mathsf{match}_{\mathrm{2}}$ starting from its maximal
elements, without implicitly computing the downward closure. We would also
like $\mathsf{match}_{\mathrm{2}}$ to compute as few non-maximal elements as
possible. We provide a new algorithm for $\mathsf{match}_{\mathrm{2}}$
following this approach.

######  Definition 4.8.

Given $T_{1},T_{2}$ sets of $2$-sharing groups and
$U_{1},U_{2}\subseteq\mathcal{V}$, we define

$\mathsf{match}^{\prime}_{\mathrm{2}}(T_{1},U_{1},T_{2},U_{2})=T^{\prime}_{2}\cup\bigcup_{o\in
T_{1}}\mathsf{match}^{\prime}_{\mathrm{2}}(o)\enspace,$

where

$\mathsf{match}^{\prime}_{\mathrm{2}}(o)=\left\\{\left(o\wedge\biguplus
X\right)\uplus\biguplus(X\cap\mkern
1.5mu\overline{\mkern-1.5muT\mkern-1.5mu}\mkern 1.5mu)\Bigm{|}X\subseteq
T^{\prime\prime}_{2},\left(\biguplus\llfloor X\rrfloor\right)_{|U_{1}}\leq
o_{|U_{2}}\right\\}\enspace,$

with $T^{\prime}_{2}$ and $T^{\prime\prime}_{2}$ as in Definition 4.4, $\mkern
1.5mu\overline{\mkern-1.5muT\mkern-1.5mu}\mkern 1.5mu=\\{o^{\prime}\in
T^{\prime\prime}_{2}\mid\forall v\in o^{\prime}\cap U_{1},o(v)=\infty\\}$ and

$o\wedge o^{\prime}=\lambda v.\begin{cases}o(v)&\text{if $v\in U_{1}\setminus
U_{2}$},\\\ min(o(v),o^{\prime}(v))&\text{if $v\in U_{1}\cap U_{2}$,}\\\
o^{\prime}(v)&\text{otherwise.}\end{cases}$

The operator $\mathsf{match}^{\prime}_{\mathrm{2}}$ aims at computing the set
of maximal $2$-sharing groups in
$\mathsf{match}_{\mathrm{2}}([{\mathop{\downarrow}}T_{1}]_{U_{1}},[{\mathop{\downarrow}}T_{2}]_{U_{2}})$.
It works by considering one sharing group $o\in T_{1}$ at a time, and calling
an auxiliary operator which computes the maximal $2$-sharing groups compatible
with $o$. A $2$-sharing group $o^{\prime}$ is compatible with $o$ if $\llfloor
o^{\prime}\rrfloor\cap U_{1}=\llfloor o\rrfloor\cap U_{1}$.

When computing the auxiliary operator
$\mathsf{match}^{\prime}_{\mathrm{2}}(o)$ we choose a subset $X$ of
$T^{\prime\prime}_{2}$. Given $o^{\prime}\in X$, note that $\llfloor
o^{\prime}\rrfloor$ may be viewed as a $2$-sharing group which is the
linearized version of $o^{\prime}$: it has the same support as $o^{\prime}$,
but all variables are linear. If $o^{\prime}\in T^{\prime\prime}_{2}$, its
linearization is in ${\mathop{\downarrow}}T_{2}$. The choice of $X$ is valid
if the multiset sum of all its linearizations is smaller than $o$ for all the
variables in $U_{1}\cap U_{2}$. Once established that $X$ is a valid choice,
we do not take directly $\biguplus\llfloor X\rrfloor$ as the resulting
$2$-sharing group, but we try to find an $o^{\prime\prime}\geq\biguplus X$.

To this purpose, we observe that, given $o^{\prime}\in X$, if $o(v)=\infty$
for each $v\in\llfloor o^{\prime}\rrfloor\cap U_{1}$, then we may take
$o^{\prime}$ twice. We denote with $\mkern
1.5mu\overline{\mkern-1.5muT\mkern-1.5mu}\mkern 1.5mu$ the set of all the
sharing groups in $T^{\prime\prime}_{2}$ which such a property, and we
unconditionally add to the result the sharing groups in $X\cap\mkern
1.5mu\overline{\mkern-1.5muT\mkern-1.5mu}\mkern 1.5mu$, so that all these
sharing groups are taken twice. Therefore, the biggest element compatible with
$o$ is $(o\wedge\biguplus X)\uplus\biguplus(X\cap\mkern
1.5mu\overline{\mkern-1.5muT\mkern-1.5mu}\mkern 1.5mu)$.

######  Example 4.9.

Under the hypothesis of Examples 3.5 and 4.3, let us define
$T_{1}=\\{x^{\infty},xz\\}$ and $T_{2}=\\{uv,ux,vx^{\infty},x\\}$. We have
$T^{\prime}_{2}=\\{uv\\}$ and $T^{\prime\prime}_{2}=\\{ux,vx^{\infty},x\\}$.

Let us compute $\mathsf{match}^{\prime}_{\mathrm{2}}(x^{\infty})$. We have
$\mkern 1.5mu\overline{\mkern-1.5muT\mkern-1.5mu}\mkern
1.5mu=T^{\prime\prime}_{2}$. If we take $X=\\{ux,xv^{\infty}\\}$, we have
$\left(\biguplus\llfloor X\rrfloor\right)_{|U_{1}}=x^{\infty}$, hence the
choice is valid. The corresponding result is $(x^{\infty}\wedge\biguplus
X)\uplus\biguplus X=uv^{\infty}x^{\infty}\uplus
uv^{\infty}x^{\infty}=u^{\infty}v^{\infty}x^{\infty}$. Overall, we have
$\mathsf{match}^{\prime}_{\mathrm{2}}(x^{\infty})=\\{u^{\infty}x^{\infty},v^{\infty}x^{\infty},x^{\infty},u^{\infty}x^{\infty}v^{\infty}\\}$.
Note that some results are computed by different choices of $X$. For example,
both $\\{ux,x\\}$ and $\\{ux\\}$ generates $u^{\infty}x^{\infty}$.

Let us compute $\mathsf{match}^{\prime}_{\mathrm{2}}(xz)$ and take
$X=\\{vx^{\infty}\\}$. We have that $\left(\biguplus\llfloor
X\rrfloor\right)_{|U_{1}}=x=xz_{|U_{2}}$. In this case, $\mkern
1.5mu\overline{\mkern-1.5muT^{\prime\prime}_{2}\mkern-1.5mu}\mkern
1.5mu=\emptyset$. Therefore, the result is $x\wedge vx^{\infty}=vx$. Note that
if we take $X=\\{xz,x\\}$ then $\left(\biguplus\llfloor
X\rrfloor\right)_{|U_{1}}=x\uplus x=x^{\infty}$, and the choice is not valid.
This shows that, due to the downward closure, choosing in $X$ a sharing group
with a non-linear variable is very different from choosing the same variable
twice. At the end, we have
$\mathsf{match}^{\prime}_{\mathrm{2}}(xz)=\\{uxz,vxz,xz\\}$. Finally,

$\mathsf{match}_{\mathrm{2}}(T_{1},U_{1},T_{2},U_{2})=\\{uv,u^{\infty}x^{\infty},v^{\infty}x^{\infty},x^{\infty},u^{\infty}x^{\infty}v^{\infty},uxz,vxz,xz\\}\enspace.$

This is exactly the set of maximal elements in
$\mathsf{match}_{\mathrm{2}}([{\mathop{\downarrow}}T_{1}]_{U_{1}},[{\mathop{\downarrow}}T_{2}]_{U_{2}})$.

We can show that the correspondence between $\mathsf{match}_{\mathrm{2}}$ and
$\mathsf{match}^{\prime}_{\mathrm{2}}$ in the previous example was not by
chance, proving the following:

######  Theorem 4.10.

Given $T_{1},T_{2}$ sets of $2$-sharing groups such that
${\mathop{\downarrow}}[T_{1}]_{U_{1}},{\mathop{\downarrow}}[T_{2}]_{U_{2}}\in{\mathtt{ShLin}^{2}}$,
we have

$\mathsf{match}_{\mathrm{2}}({\mathop{\downarrow}}[T_{1}]_{U_{1}},{\mathop{\downarrow}}[T_{2}]_{U_{2}})={\mathop{\downarrow}}[\mathsf{match}^{\prime}_{\mathrm{2}}(T_{1},U_{1},T_{2},U_{2})]_{U_{1}\cup
U_{2}}\enspace.$

######  Proof 4.11.

We start by proving that if $o$ is an element in
$\mathsf{match}_{\mathrm{2}}({\mathop{\downarrow}}[T_{1}]_{U_{1}},{\mathop{\downarrow}}[T_{2}]_{U_{2}})$,
then
$o\in{\mathop{\downarrow}}\mathsf{match}^{\prime}_{\mathrm{2}}(T_{1},U_{1},T_{2},U_{2})$.
If $o\in{\mathop{\downarrow}}T^{\prime}_{2}$ this is trivial since
$T^{\prime}_{2}\subseteq\mathsf{match}^{\prime}_{\mathrm{2}}(T_{1},U_{1},T_{2},U_{2})$.
Otherwise, $o_{|U_{1}}\in{\mathop{\downarrow}}T_{1}$ and
$o_{|U_{2}}\in({\mathop{\downarrow}}T^{\prime\prime}_{2})^{*}$, according to
Definition 4.4. Let $o_{1}\in T_{1}$ such that $o_{1}\geq o_{|U_{1}}$, we want
to prove that there exists
$\bar{o}\in\mathsf{match}^{\prime}_{\mathrm{2}}(o_{1})$ such that
$o\leq\bar{o}$.

Since $o_{|U_{2}}\in({\mathop{\downarrow}}T^{\prime\prime}_{2})^{*}$, there
are $X_{a}\subseteq{\mathop{\downarrow}}T^{\prime\prime}_{2}$ and
$X_{b}\subseteq({\mathop{\downarrow}}T^{\prime\prime}_{2})^{2}$ such that
$o_{|U_{2}}=\biguplus X_{a}\uplus\biguplus X_{b}$. For each $o_{a}\in X_{a}$,
consider $o^{\prime}_{a}\in T^{\prime\prime}_{2}$ such that
$o^{\prime}_{a}\geq o_{a}\in T^{\prime\prime}_{2}$. Let $Y_{a}$ be the set of
all those $o^{\prime}_{a}$. For each $o_{b}\in X_{b}$, consider an
$o^{\prime}_{b}\in T^{\prime\prime}_{2}$ such that
$(o^{\prime}_{b})^{2}=o_{b}$. Let $Y_{b}$ be the set of all those
$o^{\prime}_{b}$. By construction $\biguplus Y_{a}\geq\biguplus
X_{a}\geq\biguplus\llfloor Y_{a}\rrfloor$ and $\biguplus Y_{b}\uplus\biguplus
Y_{b}=\biguplus\llfloor Y_{b}\rrfloor\uplus\biguplus\llfloor
Y_{b}\rrfloor=\biguplus X_{b}$.

Let $Y=Y_{a}\cup Y_{b}$. Obviously $Y\subseteq T^{\prime\prime}_{2}$ and
$(\biguplus\llfloor Y\rrfloor)_{|U_{1}}=\biguplus\llfloor
Y_{a}\rrfloor\uplus\biguplus\llfloor Y_{b}\rrfloor\leq(\biguplus
X_{a}\uplus\biguplus
X_{b})_{|U_{1}}=(o_{|U_{2}})_{|U_{1}}=(o_{|U_{1}})_{|U_{2}}\leq(o_{1})_{|U_{2}}$.
Therefore, $\bar{o}=(o_{1}\wedge\biguplus Y)\uplus\biguplus(Y\cap\mkern
1.5mu\overline{\mkern-1.5muT\mkern-1.5mu}\mkern
1.5mu)\in\mathsf{match}_{\mathrm{2}}^{\prime}(o_{1})$. We now prove that
$o\leq\bar{o}$.

Given any $o_{b}\in X_{b}$, we have that $o_{1}(v)=o_{b}(v)=\infty$ for each
$v\in o_{b}\cap U_{1}$. This implies that $Y_{b}\subseteq\mkern
1.5mu\overline{\mkern-1.5muT\mkern-1.5mu}\mkern 1.5mu$. Therefore,
$\bar{o}\geq(o_{1}\wedge\biguplus Y_{a}\uplus\biguplus Y_{b})\uplus\biguplus
Y_{b}=(o_{1}\wedge\biguplus Y_{a})\uplus\biguplus Y_{b}\uplus\biguplus
Y_{b}\geq(o_{1}\wedge\biguplus X_{a})\uplus\biguplus
X_{b}=o_{1}\wedge(\biguplus X_{a}\uplus\biguplus X_{b})=o_{1}\wedge
o_{|U_{2}}$. Now, if $v\in U_{1}\setminus U_{2}$, we have
$\bar{o}(v)=o_{1}(v)\geq o(v)$. If $v\in U_{2}\setminus U_{1}$ we have
$\bar{o}(v)\geq o_{|U_{2}}(v)=o(v)$. Finally, if $v\in U_{1}\cap U_{2}$, then
$o_{1}(v)\geq o_{|U_{1}}(v)=o_{|U_{2}}(v)=o(v)$, hence $\bar{o}(v)\geq o(v)$.
This concludes one side of the proof.

For the other side of the equality, assume
$o\in\mathsf{match}^{\prime}_{2}(T_{1},U_{1},T_{2},U_{2})$ and prove
$o\in\mathsf{match}_{\mathrm{2}}({\mathop{\downarrow}}[T_{1}]_{U_{1}},{\mathop{\downarrow}}[T_{2}]_{U_{2}})$.
If $o\in T^{\prime}_{2}$ this is trivial, since
$\mathsf{match}_{\mathrm{2}}({\mathop{\downarrow}}[T_{1}]_{U_{1}},{\mathop{\downarrow}}[T_{2}]_{U_{2}})\supseteq{\mathop{\downarrow}}T^{\prime}_{2}$.
Otherwise, $o=(o_{1}\wedge\biguplus X)\uplus\biguplus(X\cap\mkern
1.5mu\overline{\mkern-1.5muT\mkern-1.5mu}\mkern 1.5mu)$ for some $o_{1}\in
T_{1}$ and $X\subseteq T^{\prime\prime}_{2}$ satisfying the properties of
Definition 4.8. Consider $Y=(X\setminus\mkern
1.5mu\overline{\mkern-1.5muT\mkern-1.5mu}\mkern 1.5mu)\cup(X\cap\mkern
1.5mu\overline{\mkern-1.5muT\mkern-1.5mu}\mkern 1.5mu)^{2}$ which is an
element of $T^{\prime\prime}_{2}\cup(T^{\prime\prime}_{2})^{2}$ such that
$\biguplus Y=\biguplus X\uplus\biguplus(X\cap\mkern
1.5mu\overline{\mkern-1.5muT\mkern-1.5mu}\mkern
1.5mu)\in(T^{\prime\prime}_{2})^{*}$. It is enough to prove that
$o_{|U_{1}}=o_{1}$ and $o_{|U_{2}}=\biguplus Y$. If $v\in U_{1}\setminus
U_{2}$ we have $o(v)=o_{1}(v)$. Note that if $\bar{o}\in X\cap\mkern
1.5mu\overline{\mkern-1.5muT\mkern-1.5mu}\mkern 1.5mu$ and $v\in\bar{o}\cap
U_{1}$, then $o_{1}(v)=\infty$. Therefore, for each $v\in U_{1}\cap U_{2}$, we
have $o(v)=o_{1}(v)$. Finally, if $v\in U_{2}$, we have $o(v)=\biguplus
X\uplus\biguplus(X\cap\mkern 1.5mu\overline{\mkern-1.5muT\mkern-1.5mu}\mkern
1.5mu)=\biguplus Y$.

##  5 Abstract matching over $\mathtt{Sharing}\times\mathtt{Lin}$

The reduced product $\mathtt{ShLin}=\mathtt{Sharing}\times\mathtt{Lin}$ has
been used for a long time in the analysis of aliasing properties, since it was
recognized quite early that the precision of these analyses could be greatly
improved by keeping track of the linear variables. In the following, we
briefly recall the definition of the abstract domain following the
presentation in Amato and Scozzari, (2010).

###  5.1 The domain $\mathtt{ShLin}$

The domain $\mathtt{ShLin}$ couples an object of $\mathtt{Sharing}$ with the
set of variables known to be linear. Each element of $\mathtt{ShLin}$ is
therefore a triple: the first component is an object of $\mathtt{Sharing}$,
the second component is an object of $\mathtt{Lin}$, that is, the set of
variables which are linear in all the sharing groups of the first component,
and the third component is the set of variables of interest. It is immediate
that $\mathtt{ShLin}$ is an abstraction of ${\mathtt{ShLin}^{2}}$ (and thus of
${\mathtt{ShLin}^{\omega}}$).

$\mathtt{ShLin}=\\{[S,L,U]\mid
S\subseteq\mathscr{P}(U),(S\neq\emptyset\Rightarrow\emptyset\in S),L\supseteq
U\setminus\mathrm{vars}(S),U\in\mathscr{P}_{f}(\mathcal{V})\\}\enspace,$

with the approximation relation $\leq_{\mathit{sl}}$ defined as
$[S,L,U]\leq_{\mathit{sl}}[S^{\prime},L^{\prime},U^{\prime}]$ iff
$U=U^{\prime}$, $S\subseteq S^{\prime}$, $L\supseteq L^{\prime}$. There is a
Galois insertion of $\mathtt{ShLin}$ into ${\mathtt{ShLin}^{2}}$ given by the
pair of maps:

$\displaystyle\alpha_{\mathit{sl}}([T]_{U})$ $\displaystyle=[\\{\llfloor
o\rrfloor\mid o\in T\\},\\{x\in U\mid\forall o\in T.\ o(x)\leq
1\\},U]\enspace,$ $\displaystyle\gamma_{\mathit{sl}}([S,L,U])$
$\displaystyle=[{\mathop{\downarrow}}\\{B_{L}\mid B\in S\\}]_{U}\enspace,$
where $B_{L}$ is the 2-sharing group which has the same support of $B$, with
linear variables dictated by the set $L$: $\displaystyle B_{L}$
$\displaystyle=\lambda v\in\mathcal{V}.\begin{cases}\infty&\text{if $v\in
B\setminus L$,}\\\ 1&\text{if $v\in B\cap L$,}\\\
0&\text{otherwise.}\end{cases}$

The functional composition of $\alpha_{\mathrm{\omega}}$,
$\alpha_{\mathrm{2}}$ and $\alpha_{\mathit{sl}}$ gives the standard
abstraction map from substitutions to $\mathtt{ShLin}$. We still use the
polynomial notation to represent sharing groups, but now all the exponents are
fixed to one. Note that the last component $U$ in $[S,L,U]$ is redundant since
it can be retrieved as $L\cup\mathrm{vars}(S)$. This is because the set $L$
contains all the ground variables.

######  Example 5.1.

Consider the substitution
$[\theta]_{U}=[\\{x/s(y,u,y),z/s(u,u),v/u\\}]_{w,x,y,z}$ in the Example 3.2.
Its abstraction in $\mathtt{ShLin}$ is given by

$\alpha_{\mathit{sl}}(\alpha_{\mathrm{2}}(\alpha_{\mathrm{\omega}}([\theta]_{U})))=[\\{xy,xz,w\\},\\{y,w\\},U]\enspace.$

Analogously, substitutions
$[\theta_{1}]_{U_{1}}=[\\{x/r(w_{1},w_{2},w_{2},w_{3},w_{3}),y/a,z/r(w_{1})\\}]_{x,y,z}$
and
$[\theta_{2}]_{U_{2}}=[\\{x/r(w_{4},w_{5},w_{6},w_{8},w_{8}),u/r(w_{4},w_{7}),v/r(w_{7},w_{8})\\}]_{u,v,x}$
from Example 3.3 are abstracted into
$[S_{1},L_{1},U_{1}]=[\\{x,xz\\},\\{y,z\\},U_{1}]$ and
$[S_{2},L_{2},U_{2}]=[\\{uv,ux,vx,x\\},\\{u,v\\},U_{2}]$ respectively.

###  5.2 Matching operator

We want to provide an optimal abstract matching operator for $\mathtt{ShLin}$.
We may effectively compute $\mathsf{match}_{\mathit{sl}}$ by composing
$\gamma_{\mathit{sl}}$, $\mathsf{match}_{\mathrm{2}}$ and
$\alpha_{\mathit{sl}}$. However, we provide a more direct characterization of
$\mathsf{match}_{\mathit{sl}}$, which may potentially improve performance.

First, we define the auxiliary function
$nl:\mathscr{P}(\mathscr{P}(\mathcal{V}))\rightarrow\mathscr{P}(\mathcal{V})$
which takes a set $X$ of sharing groups and returns the set of variables which
appear in $X$ more than once. In formulas:

$nl(X)=\\{v\in\mathcal{V}\mid\exists B_{1},B_{2}\in X,B_{1}\neq B_{2},v\in
B_{1}\cap B_{2}\\}$ (14)

The name $nl$ stands for non-linear, since it is used to recover those
variables which, after joining sharing groups in $X$, are definitively not
linear.

######  Definition 5.2 (Matching over $\mathtt{ShLin}$ ).

Given $[S_{1},L_{1},U_{1}]$ and $[S_{2},L_{2},U_{2}]\in\mathtt{ShLin}$, we
define

$\mathsf{match}_{\mathit{sl}}([S_{1},L_{1},U_{1}],[S_{2},L_{2},U_{2}])=\left[s(S^{\prime}_{0}\cup
S^{\prime\prime}_{0}),l(S^{\prime}_{0}\cup S^{\prime\prime}_{0}),U\right],$

where $U=U_{1}\cup U_{2}$, $S^{\prime}_{2}=\\{B\in S_{2}\mid B\cap
U_{1}=\emptyset\\}$, $S^{\prime\prime}_{2}=S_{2}\setminus S^{\prime}_{2}$,
$\mkern 1.5mu\overline{\mkern-1.5muS\mkern-1.5mu}\mkern 1.5mu=\\{B\in
S^{\prime\prime}_{2}\mid B\cap L_{1}=\emptyset\\}$ and

$\displaystyle S^{\prime}_{0}$ $\displaystyle=\bigl{\\{}\langle
B,L_{2}\rangle\mid B\in S^{\prime}_{2}\bigr{\\}},$ $\displaystyle
S^{\prime\prime}_{0}$ $\displaystyle=\Big{\\{}\left\langle B\cup\bigcup
X,L_{2}\setminus nl(X)\setminus\bigcup(X\cap\mkern
1.5mu\overline{\mkern-1.5muS\mkern-1.5mu}\mkern
1.5mu)\right\rangle\Bigm{|}B\in S_{1},$ $\displaystyle\qquad X\subseteq
S^{\prime\prime}_{2},B\cap U_{2}=\left(\bigcup X\right)\cap U_{1},L_{1}\cap
nl(X)=\emptyset\Big{\\}},$ $\displaystyle s(H)$
$\displaystyle=\left\\{B\mid\langle B,L\rangle\in H\right\\},$ $\displaystyle
l(H)$ $\displaystyle=\bigcap\left\\{L_{1}\cup L\cup(U\setminus B)\mid\langle
B,L\rangle\in H\right\\}.$

This operator is more complex than previous ones, because linearity
information is not connected to sharing groups and needs to be handled
separately. In view of this and a similar situation which happens for
unification (Amato and Scozzari, 2010), it seems that the idea of embedding
linearity within sharing groups from King, (1994) was particularly insightful.

We give an intuitive explanation of $\mathsf{match}_{\mathit{sl}}$. It
essentially works by simulating the optimized version of
$\mathsf{match}_{\mathrm{2}}$ starting from
$[T_{1}]_{U_{1}}=\gamma_{\mathrm{2}}([S_{1},L_{1},U_{1}])$ and
$[T_{2}]_{U_{2}}=\gamma_{\mathrm{2}}([S_{2},L_{2},U_{2}])$. The sets
$S^{\prime}_{2}$ and $S^{\prime\prime}_{2}$ are defined as for the other
matching operators. Each element of $H$, $S^{\prime}_{0}$ or
$S^{\prime\prime}_{0}$ is a pair $\langle B,L\rangle$ which corresponds to the
$2$-sharing group $B_{L\cup L_{1}}$ in
$\mathsf{match}_{\mathrm{2}}([T_{1}]_{U_{1}},[T_{2}]_{U_{2}})$. The component
$B$ is the support of the $2$-sharing group, while $L$ is the set of linear
variables. We only record a subset of the linear variables, since those in
$L_{1}$ are always linear.

The set $S^{\prime}_{0}$ encodes all the maximal $2$-sharing groups derived
from $S^{\prime}_{2}$. The set $S^{\prime\prime}_{0}$ encodes $2$-sharing
groups which may be generated by gluing the sharing groups in
$S^{\prime\prime}_{2}$ in a way which is compatible with $S_{1}$. A given
choice of $X\subseteq T^{\prime\prime}_{2}$ is compatible with a sharing group
$B\in S_{1}$ only if $\bigcup X$ and $B$ have the same support on the common
variables $U_{1}\cap U_{2}$ and if $X$ does not conflict with the linearity of
variables given by $L_{1}$. This means that we cannot use a variable in
$L_{1}$ more than once, therefore $L_{1}\cap nl(X)=\emptyset$. Note that we
may use a variable $v\in L_{1}\setminus L_{2}$, since $v\notin L_{2}$ means
that $v$ is possibly, but not definitively, non-linear. On the contrary, if
$v\in nl(X)$, then $v$ is definitively non-linear in the resultant sharing
group. Once established that $X$ is compatible with $B$, the set $\mkern
1.5mu\overline{\mkern-1.5muS\mkern-1.5mu}\mkern 1.5mu$ plays the same role of
$\mkern 1.5mu\overline{\mkern-1.5muT\mkern-1.5mu}\mkern 1.5mu$ in Definition
4.8: we may join another copy of the sharing groups in $X\cap\mkern
1.5mu\overline{\mkern-1.5muS\mkern-1.5mu}\mkern 1.5mu$, making all their
variables non-linear.

Finally, the maps $s$ and $l$ extract from $S^{\prime}_{0}$ and
$S^{\prime\prime}_{0}$ the set of all the sharing groups, and the set of
variables which are linear in all the sharing groups.

######  Example 5.3.

Consider the substitutions in Example 5.1. According to the definition of
$\mathsf{match}_{\mathit{sl}}$, we have: $S^{\prime}_{2}=\\{uv\\}$,
$S^{\prime\prime}_{2}=\mkern 1.5mu\overline{\mkern-1.5muS\mkern-1.5mu}\mkern
1.5mu=\\{ux,vx,x\\}$, $S^{\prime}_{0}=\\{\langle uv,\\{u,v\\}\rangle\\}$ and
$S^{\prime\prime}_{0}=\\{\langle ux,\emptyset\rangle,\langle
vx,\emptyset\rangle,\langle x,\emptyset\rangle,\langle
uvx,\emptyset\rangle,\langle uxz,\emptyset\rangle,\langle
vxz,\emptyset\rangle,\langle xz,\emptyset\rangle,\langle
uvxz,\emptyset\rangle\\}$. The final result is

$\mathsf{match}_{\mathit{sl}}([S_{1},L_{1},U_{1}],[S_{2},L_{2},U_{2}])=[\\{uv,uvx,ux,vx,x,\\\
uvxz,uxz,xz,vxz\\},\\{y,z\\},U_{1}\cup U_{2}]\enspace.$ (15)

Considering the results for $\mathsf{match}_{\mathrm{2}}$ in the Example 4.5,
we have:

$\alpha_{\mathit{sl}}(\mathsf{match}_{\mathrm{2}}([T_{1}]_{U_{1}},[T_{2}]_{U_{2}}))\\\
=\alpha_{\mathit{sl}}({\mathop{\downarrow}}[uv,u^{\infty}v^{\infty}x^{\infty},uxz,u^{\infty}x^{\infty},v^{\infty}x^{\infty},vxz,x^{\infty},xz]_{u,v,x,y,z})\\\
=[\\{uv,uvx,uxz,ux,vx,vxz,x,xz\\},\\{y,z\\},\\{u,v,x,y,z\\}]$

and
$\mathsf{match}_{\mathit{sl}}([S_{1},L_{1},U_{1}],[S_{2},L_{2},U_{2}])>\alpha_{\mathit{sl}}(\mathsf{match}_{\mathrm{2}}([T_{1}]_{U_{1}},[T_{2}]_{U_{2}}))$.
In particular, the sharing group $uvxz$ does not appear in
$\alpha_{\mathit{sl}}(\mathsf{match}_{\mathrm{2}}([T_{1}]_{U_{1}},[T_{2}]_{U_{2}}))$
which proves that $\mathsf{match}_{\mathit{sl}}$ is not a complete abstraction
of $\mathsf{match}_{\mathrm{2}}$. However, the next theorem shows that
$\mathsf{match}_{\mathit{sl}}$ is optimal w.r.t.
$\mathsf{match}_{\mathrm{2}}$, and by composition also w.r.t.
$\mathsf{match}_{\mathrm{\omega}}$ and $\mathsf{match}$.

######  Theorem 5.4 (Optimality of $\mathsf{match}_{\mathit{sl}}$).

The operator $\mathsf{match}_{\mathit{sl}}$ is correct and optimal w.r.t.
$\mathsf{match}_{\mathrm{2}}$.

######  Proof 5.5.

We prove that, given $[S_{1},L_{1},U_{1}]$ and
$[S_{2},L_{2},U_{2}]\in\mathtt{ShLin}$, we have

$\mathsf{match}_{\mathit{sl}}([S_{1},L_{1},U_{1}],[S_{2},L_{2},U_{2}])=\alpha_{\mathit{sl}}({\mathop{\downarrow}}[\mathsf{match}^{\prime}_{\mathrm{2}}(T_{1},U_{1},T_{2},U_{2})]_{U})$

where $T_{i}=\\{B_{L_{i}}\mid B\in S_{i}\\}$ is the set of maximal elements of
$\gamma_{\mathit{sl}}([S_{i},L_{i},U_{i}])$ and $U=U_{1}\cup U_{2}$.

Let us define the function $\gamma_{0}$ which maps a pair $\langle B,L\rangle$
with $B,L\in\mathscr{P}(\mathcal{V})$ to the $2$-sharing group $B_{L\cup
L_{1}}$. We show that, given
$H\subseteq\mathscr{P}(\mathcal{V})\times\mathscr{P}(\mathcal{V})$, we have
$\alpha_{\mathit{sl}}([{\mathop{\downarrow}}\gamma_{0}(H)]_{U})=[s(H),l(H),U]$.
Assume
$\alpha_{\mathit{sl}}([{\mathop{\downarrow}}\gamma_{0}(S)]_{U}])=[R,V,U]$. We
have $R=\\{\llfloor o\rrfloor\mid
o\in{\mathop{\downarrow}}\gamma_{0}(S)\\}=\\{\llfloor o\rrfloor\mid
o\in\gamma_{0}(S)\\}=\\{\llfloor\gamma_{o}(\langle
B,L\rangle)\rrfloor\mid\langle B,L\rangle\in S\\}=\\{B\mid\langle
B,L\rangle\in S\\}=s(S)$ and $V=\\{x\in U\mid\forall
o\in{\mathop{\downarrow}}\gamma_{0}(S),o(x)\leq 1\\}=\\{x\in U\mid\forall
o\in\gamma_{0}(S),o(x)\leq 1\\}=\\{x\in U\mid\forall\langle B,L\rangle\in
S,B_{L\cup L_{1}}(x)\leq 1\\}\\}=\\{x\in U\mid\forall\langle B,L\rangle\in
S,x\in L_{1}\cup L\cup(U\setminus B)\\}=\bigcap\\{L_{1}\cup L\cup(U\setminus
B)\mid\langle B,L\rangle\in S\\}=l(S)$.

Therefore, if we prove that $\gamma_{0}(S^{\prime}_{0}\cup
S^{\prime\prime}_{0})=\mathsf{match}^{\prime}_{\mathrm{2}}(T_{1},U_{1},T_{2},U_{2})$,
then we have
$\mathsf{match}_{\mathit{sl}}([S_{1},T_{1},U_{1}],[S_{2},T_{2},U_{2}])=[s(S^{\prime}_{0}\cup
S^{\prime\prime}_{0}),l(S^{\prime}_{0}\cup
S^{\prime\prime}_{0}),U]=\alpha_{\mathit{sl}}([{\mathop{\downarrow}}\gamma_{0}(S^{\prime}_{0}\cup
S^{\prime\prime}_{0})]_{U}])=\alpha_{\mathit{sl}}({\mathop{\downarrow}}[\mathsf{match}^{\prime}_{\mathrm{2}}(T_{1},U_{1},T_{2},U_{2})]_{U}))$.

Let us take $o\in\gamma_{0}(S^{\prime}_{0}\cup S^{\prime\prime}_{0})$ and
prove $o\in\mathsf{match}^{\prime}_{\mathrm{2}}(T_{1},U_{1},T_{2},U_{2})$. If
$o=B_{L\cup L_{1}}$ for some $\langle B,L\rangle\in S^{\prime}_{0}$, then
$B\in S^{\prime}_{2}$ and $L=L_{2}$. Therefore, $B_{L\cup L_{1}}=B_{L_{2}\cup
L_{1}}=B_{L_{2}}\in T_{2}$ since $B\cap U_{1}=\emptyset$. In particular,
$B_{L_{2}}\in T^{\prime}_{2}$, hence
$B_{L_{2}}\in\mathsf{match}^{\prime}_{\mathrm{2}}(T_{1},U_{1},T_{2},U_{2})$.
Otherwise, $o=\gamma_{0}(\langle C,L\rangle)$ for $\langle C,L\rangle\in
S^{\prime\prime}_{0}$ where $C=B\cup\bigcup X$ and $L=L_{2}\setminus
nl(X)\setminus\bigcup(X\cap\mkern
1.5mu\overline{\mkern-1.5muS\mkern-1.5mu}\mkern 1.5mu)$ according to
Definition 5.2. For each sharing group $B^{\prime}\in X$, consider the
$2$-sharing group $B^{\prime}_{L_{2}}\in T^{\prime\prime}_{2}$ and let $Y$ be
the set of all those $2$-sharing groups. We want to prove that $o$ is
generated by $B_{L_{1}}\in T_{1}$ and $Y\subseteq T^{\prime\prime}_{2}$,
according to Definition 4.8. First, note that $\llfloor(\biguplus\llfloor
Y\rrfloor)_{|U_{1}}\rrfloor=\llfloor(\biguplus X)_{|U_{1}}\rrfloor=(\bigcup
X)\cap U_{1}=B\cap U_{2}=\llfloor(B_{L_{1}})_{|U_{2}}\rrfloor$. Now, assume
$v\in\llfloor(B_{L_{1}})_{|U_{2}}\rrfloor$. If $v$ is linear in
$(B_{L_{1}})_{|U_{2}}$, then $v\in L_{1}$, hence $v\notin nl(X)$ and $v$ is
linear in $(\biguplus X)_{|U_{1}}=(\biguplus\llfloor Y\rrfloor)_{|U_{1}}$.
Therefore, $Y$ is a valid choice for $\mathsf{match}_{\mathrm{2}}^{\prime}$
and $\mathsf{match}^{\prime}_{\mathrm{2}}(B)$ generates
$o^{\prime}=(B_{L_{1}}\wedge\biguplus Y)\uplus\biguplus(Y\cap\mkern
1.5mu\overline{\mkern-1.5muT\mkern-1.5mu}\mkern 1.5mu)$. We prove
$o^{\prime}=o$.

First, we prove that $B^{\prime}\in\mkern
1.5mu\overline{\mkern-1.5muS\mkern-1.5mu}\mkern 1.5mu$ iff
$B^{\prime}_{L_{2}}\in\mkern 1.5mu\overline{\mkern-1.5muT\mkern-1.5mu}\mkern
1.5mu$. We have $B^{\prime}_{L_{2}}\in\mkern
1.5mu\overline{\mkern-1.5muT\mkern-1.5mu}\mkern 1.5mu$ iff
$B^{\prime}_{L_{2}}\in T^{\prime\prime}_{2}$ and $\forall v\in\llfloor
B^{\prime}_{L_{2}}\rrfloor\cap U_{1},B^{\prime}_{L_{1}}(v)=\infty$, iff
$B^{\prime}\in S^{\prime\prime}_{2}$ and $\forall v\in B^{\prime}\cap U_{1}$,
$v\notin L_{1}$ iff $B^{\prime}\cap L_{1}=\emptyset$ iff $B^{\prime}\in
S^{\prime\prime}_{2}$ and $B^{\prime}\cap L_{1}=\emptyset$ iff $B\in S$.

Now, it is immediate to check that, $\llfloor o\rrfloor=B\cup\bigcup
X=\llfloor o^{\prime}\rrfloor$. Then, consider $v\in\llfloor
o^{\prime}\rrfloor$. We have that:

$\displaystyle o^{\prime}(v)=1\Leftrightarrow$
$\displaystyle(B_{L_{1}}(v)=1\vee\left(\biguplus
Y\right)(v)=1)\wedge\left(\biguplus(Y\cap\mkern
1.5mu\overline{\mkern-1.5muT\mkern-1.5mu}\mkern
1.5mu)\right)=0\Leftrightarrow$ $\displaystyle(v\in L_{1}\vee(v\in
L_{2}\setminus nl(X)))\wedge v\notin\bigcup(X\cap\mkern
1.5mu\overline{\mkern-1.5muS\mkern-1.5mu}\mkern 1.5mu)\Leftrightarrow$
$\displaystyle v\in L_{1}\vee(v\in L_{2}\setminus
nl(X)\setminus\bigcup(X\cap\mkern
1.5mu\overline{\mkern-1.5muS\mkern-1.5mu}\mkern 1.5mu)\Leftrightarrow$
$\displaystyle v\in L_{1}\vee v\in L\Leftrightarrow$ $\displaystyle B_{L\cup
L_{1}}(v)=o(v)=1$

It remains to prove that given
$o\in\mathsf{match}^{\prime}_{\mathrm{2}}(T_{1},U_{1},T_{2},U_{2})$, we have
$o\in\gamma_{0}(S^{\prime}_{0}\cup S^{\prime\prime}_{0})$. If $o\in
T^{\prime}_{2}$, then $o=B_{L_{2}}$ with $B\in S^{\prime}_{2}$. Therefore,
$\langle B,L_{2}\rangle\in S^{\prime}_{0}$ and $o=\gamma_{0}(\langle
B,L_{2}\rangle)$. Otherwise, $o=(o^{\prime}\wedge\biguplus
Y)\uplus\biguplus(Y\cap\mkern 1.5mu\overline{\mkern-1.5muT\mkern-1.5mu}\mkern
1.5mu)$. We know $o^{\prime}=B^{\prime}_{L_{1}}$ with $B^{\prime}\in S_{1}$
and let $X=\\{\llfloor o^{\prime\prime}\rrfloor\mid o^{\prime\prime}\in Y\\}$.
By Definition 4.8, $\bigcup X\cap U_{1}=\llfloor\uplus Y\rrfloor\cap
U_{1}=\llfloor o^{\prime}\rrfloor\cap U_{2}=B^{\prime}\cap U_{2}$. Moreover,
if $v\in L_{1}$ then $o^{\prime}(v)\leq 1$ and therefore $v$ cannot appear
twice in $Y$, which means $v\notin nl(X)$, hence $L_{1}\cap nl(X)=\emptyset$.
Therefore, $B^{\prime}$ and $X$ makes a valid choice for
$\mathsf{match}_{\mathit{sl}}$ and generate the pair

$\langle B,L\rangle=\left\langle B^{\prime}\cup\bigcup X,L_{2}\setminus
nl(X)\setminus\bigcup(X\cap\mkern
1.5mu\overline{\mkern-1.5muS\mkern-1.5mu}\mkern 1.5mu)\right\rangle.$

Using the first half of the proof, it is easy to check that $B_{L\cup
L^{\prime}}=o$, which terminates the proof.

##  6 Evaluation of matching in goal-dependent analysis

We now show two examples, in the context of goal-dependent analysis, where the
newly introduced matching operators improve the precision w.r.t. what is
attainable using only the mgu operators in Amato and Scozzari, (2010).

###  6.1 Matching and backward unification

First, we show with a simple example how the matching operator strictly
improves the result of a standard goal-dependent analysis using forward and
backward unification. Consider the goal $p(x,f(x,z),z)$ with the (abstract)
call substitution $[x,z]_{xz}$ and the trivial program with just one clause:

$p(u,v,w).$

In order to analyze the goal, we first need to perform the forward unification
between the call substitution $[x,z]_{xz}$, the goal $p(x,f(x,z),z)$ and the
head of the clause $p(u,v,w)$, and then project the result on the variables of
the clause. In order to keep the notation simple, we do not perform renaming,
unless necessary. This amounts to computing:

$\mathsf{mgu}_{\mathrm{\omega}}([x,z]_{xz},\\{u/x,v/f(x,z),w/z\\})=[uvx,vwz]_{uvwxz}\enspace.$

By projecting the result on the variables of the clause we obtain the entry
substitution $[uv,vw]_{uvw}$. Since the clause has no body, it is immediate to
see that the exit substitution coincides with the entry substitution.

We now need to compute the backward unification of the exit substitution
$[uv,vw]_{uvw}$, the call substitution $[x,z]_{xz}$ and
$\theta=\\{u/x,v/f(x,z),w/z\\}$. If we implement this operator with the aid of
matching, we may first unify $[x,z]_{xz}$ with $\theta$, obtaining
$[uvx,vwz]_{uvwxz}$ as above, and then apply the matching with the exit
substitution $[uv,vw]_{uvw}$ obtaining:

$\mathsf{match}_{\mathrm{\omega}}([uv,vw]_{uvw},[uvx,vwz]_{uvwxz})=[uvx,vwz]_{uvwxz}\enspace.$

By projecting the result on the variables of the goal we obtain the result
$[x,z]_{xz}$ which proves that $x$ and $z$ do not share.

On the contrary, if we avoid matching, the backward unification operator must
unify $[x,z]_{xz}$ with $[uv,vw]_{uvw}$ and $\theta$ in any order it deems
fit. However, this means that the operator must correctly approximate the mgu
of any substitution $\theta_{1}$ in the concretization of the call
substitution $[x,z]_{xz}$, with any substitution $\theta_{2}$ in the
concretization of the exit substitution $[uv,vw]_{uvw}$ and
$\theta=\\{u/x,v/f(x,z),w/z\\}$. If we choose $\theta_{1}=\epsilon$ and
$\theta_{2}=\\{v/f(w,u)\\}$, we obtain that the unification of $\theta_{1}$,
$\theta_{2}$ and $\theta$ is

$\\{u/x,v/f(x,x),w/x,z/x\\}$

which is not in the concretization of $[uvx,vwz]_{uvwxz}$, since $u$, $v$ and
$w$ share a common variable. Moreover, in this substitution $x$ and $z$ share.
This means that, after the projection on the variables of the goals $x$ and
$z$, the result will always include the $\omega$-sharing group $xz$. Note that
this consideration holds for any correct abstract unification operator which
avoids matching.

It is worth noting that the above example, with minimal changes, also works
for ${\mathtt{ShLin}^{2}}$ and $\mathtt{ShLin}$: also in these cases, matching
improves the precision of the analysis.

###  6.2 Example on a non-trivial program

Consider a program implementing the $\mathit{member}$ predicate. Using the
Prolog notation for lists, we have:

$\mathit{member}(u,[u|v]).$
$\mathit{member}(u,[v|w])\leftarrow\mathit{member}(u,w).$

We want to analyze the goal $\mathit{member}(x,[y])$ in the domain
${\mathtt{ShLin}^{2}}$ using the _call substitution_ $[xy,xz]_{xyz}$.

We start by considering the first clause of $\mathit{member}$. The concrete
unification of the goal $\mathit{member}(x,[y])$ and the head of the clause
$\mathit{member}(u,[u|v])$ yields the most general unifier
$\theta=\\{x/u,y/u,v/[]\\}$. Forward unification computes the entry
substitution as the abstract mgu between the call substitution $[xy,xz]_{xyz}$
and $\theta$. Proceeding one binding at a time, we have

  * •

$\mathsf{mgu}_{\mathrm{2}}([xy,xz]_{xyz},\\{x/u\\})=[uxy,uxz]_{uxyz}$;

  * •

$\mathsf{mgu}_{\mathrm{2}}([uxy,uxz]_{uxyz},\\{y/u\\})={\mathop{\downarrow}}[u^{\infty}x^{\infty}y^{\infty}]_{uxyz}$;

  * •

$\mathsf{mgu}_{\mathrm{2}}({\mathop{\downarrow}}[u^{\infty}x^{\infty}y^{\infty}]_{uxyz},\\{v/[]\\})={\mathop{\downarrow}}[u^{\infty}x^{\infty}y^{\infty}]_{uvxyz}$.

Projecting over the variables of the clause, we get the entry substitution
${\mathop{\downarrow}}[u^{\infty}]_{uv}$. Since this clause has no body, the
entry substitution is equal to the exit substitution, and we may proceed to
compute the answer substitution trough backward unification.

First, we consider the case when the backward unification is performed using
the standard $\mathsf{mgu}_{\mathrm{2}}$ operator. We need to unify the call
substitution $[xy,xz]_{xyz}$, the exit substitution
${\mathop{\downarrow}}[u^{\infty}]_{uv}$ and the concrete substitution
$\theta$ (the same as before). Unifying call and exit substitution is
immediate since they are relative to disjoint variables of interest: the
result is ${\mathop{\downarrow}}[u^{\infty},xy,xz]_{uvxyz}$, obtained by
collecting all sharing groups together. This should be unified with $\theta$.
Proceeding one binding at a time, and omitting the set of variables of
interest since it does not change, we have:

  * •

$\mathsf{mgu}_{\mathrm{2}}({\mathop{\downarrow}}[u^{\infty},xy,xz],\\{x/u\\})={\mathop{\downarrow}}[u^{\infty}x^{\infty}y^{\infty},u^{\infty}x^{\infty}y^{\infty}z^{\infty},u^{\infty}x^{\infty}z^{\infty}]$;

  * •

$\mathsf{mgu}_{\mathrm{2}}({\mathop{\downarrow}}[u^{\infty}x^{\infty}y^{\infty},u^{\infty}x^{\infty}y^{\infty}z^{\infty},u^{\infty}x^{\infty}z^{\infty}],\\{y/u\\})={\mathop{\downarrow}}[u^{\infty}x^{\infty}y^{\infty},u^{\infty}x^{\infty}y^{\infty}z^{\infty}]$;

  * •

$\mathsf{mgu}_{\mathrm{2}}({\mathop{\downarrow}}[u^{\infty}x^{\infty}y^{\infty},u^{\infty}x^{\infty}y^{\infty}z^{\infty}],\\{v/[]\\})={\mathop{\downarrow}}[u^{\infty}x^{\infty}y^{\infty},u^{\infty}x^{\infty}y^{\infty}z^{\infty}]$.

Projecting over the set of variables in the goal we get
${\mathop{\downarrow}}[x^{\infty}y^{\infty},x^{\infty}y^{\infty}z^{\infty}]_{xyz}$.

On the contrary, if we perform backward unification using the matching
operation, we need to compute the matching of the exit substitution
$[u^{\infty}]_{uv}$ with the entry substitution before variable projection
$[u^{\infty}x^{\infty}y^{\infty}]_{uvxyz}$, namely:

$\mathsf{match}_{\mathrm{2}}({\mathop{\downarrow}}[u^{\infty}]_{uv},{\mathop{\downarrow}}[u^{\infty}x^{\infty}y^{\infty}]_{uvxyz})={\mathop{\downarrow}}[u^{\infty}x^{\infty}y^{\infty}]_{uvxyz}\enspace.$

Projecting over the variables of the goal, we get
${\mathop{\downarrow}}[x^{\infty}y^{\infty}]_{xyz}$: using matching we can
prove that $z$ is ground in the answer substitution.

However, we still need to check what happens when we analyze the second clause
of the $\mathit{member}$ predicate. In this case, the concrete unification
between $\mathit{member}(x,[y])$ and $\mathit{member}(u,[v|w])$ gives the
substitution $\theta=\\{x/u,y/v,w/[]\\}$. Then, forward unification between
the call substitution and $\theta$ gives

  * •

$\mathsf{mgu}_{\mathrm{2}}([xy,xz]_{xyz},\\{x/u\\})=[uxy,uxz]_{uxyz}$;

  * •

$\mathsf{mgu}_{\mathrm{2}}([uxy,uxz]_{uxyz},\\{y/v\\})=[uvxy,uxz]_{uvxyz}$;

  * •

$\mathsf{mgu}_{\mathrm{2}}([uvxy,uxz]_{uvxyz},\\{w/[]\\})=[uvxy,uxz]_{uvwxyz}$.

Projecting over the variables of the clause we get the entry substitution
$[uv,v]_{uvw}$.

Now we should compute the answer substitution of the body
$\mathit{member}(u,w)$ under the call substitution $[uv,u]_{uvw}$. We could
proceed showing all the details, but we try to be more concise. In the
abstract substitution $[uv,w]_{uvw}$ the variable $w$ is known to be ground.
When $\mathit{member}$ is called with its second argument ground, the first
argument becomes ground too. This property is easily captured by
$\mathtt{Sharing}$ and more precise domains, independently of the fact that we
use matching or not for the backward unification. Therefore, we can conclude
that the answer substitution for the goal $\mathit{member}(u,w)$ under the
entry substitution $[uv,u]_{uvw}$ is $[\emptyset]_{uvw}$. Although we do not
generally write the empty $\mathrm{2}$-sharing group $\emptyset$ in an element
of ${\mathtt{ShLin}^{2}}$, in this case it is important to write it in order
to distinguish $[\emptyset]_{uvw}$, denoting those substitutions in which
$u,v,w$ are ground, from $[]_{uvw}$, denoting a non-succeeding derivation.

Performing the backward unification of $[\emptyset]_{uvw}$, we get the answer
substitution $[\emptyset]_{xyz}$, independently of the use of matching.

Putting together the results we got for analyzing the goal
$\mathit{member}(x,[y])$ according to the two clauses of the program, we have
shown that using matching we get $[x^{\infty}y^{\infty}]_{xyz}$ while using
standard unification we get
$[x^{\infty}y^{\infty},x^{\infty}y^{\infty}z^{\infty}]_{xyz}$, and we are not
able to prove that $z$ is ground after the goal returns.

##  7 Conclusion

In this paper we have extended the domain ${\mathtt{ShLin}^{\omega}}$ (Amato
and Scozzari, 2010) to goal-dependent analysis, by introducing a matching
operator, and proved its optimality. From this operator we have derived the
optimal matching operators for the well known ${\mathtt{ShLin}^{2}}$ (King,
1994) and $\mathtt{Sharing}\times\mathtt{Lin}$ (Muthukumar and Hermenegildo,
1992) abstract domains.

As far as we know, this is the first paper which shows matching optimality
results for domains combining sharing and linearity information. In
particular, the matching operators presented in (Hans and Winkler, 1992; King,
2000) for the domain SFL, which combines set-sharing, linearity and freeness
information, are not optimal, as shown by Amato and Scozzari, (2009).

Recently logic programming has been used as an intermediate representation for
the analysis of imperative or object-oriented programs and services (see,
e.g., Peralta et al., (1998); Henriksen and Gallagher, (2006); Benton and
Fischer, (2007); Méndez-Lojo et al., (2008); Spoto et al., (2010); Albert et
al., (2012); Ivanović et al., (2013); Gange et al., (2015); De Angelis et al.,
(2021)). Since many of these approaches use existing logic program analysis on
the transformed program, we believe that they can benefit from more precise
logic program analysis.

Competing interests: The authors declare none.

## References

  * Albert et al., (2012) Albert, E., Arenas, P., Genaim, S., Puebla, G., and Zanardini, D. 2012\.  Cost analysis of object-oriented bytecode programs.  Theoretical Computer Science, 413, 1, pp. 142–159.  Special Issue on Quantitative Aspects of Programming Languages (QAPL 2010).
  * Amato and Scozzari, (2009) Amato, G. and Scozzari, F. 2009\.  Optimality in goal-dependent analysis of sharing.  Theory and Practice of Logic Programming, 9, 5, pp. 617–689.
  * Amato and Scozzari, (2010) Amato, G. and Scozzari, F. 2010\.  On the interaction between sharing and linearity.  Theory and Practice of Logic Programming, 10, 1, pp. 49–112.
  * Amato and Scozzari, (2011) Amato, G. and Scozzari, F. 2011\.  Observational completeness on abstract interpretation.  Fundamenta Informaticae, 106, 2–4, pp. 149–173.
  * Amato and Scozzari, (2014) Amato, G. and Scozzari, F. 2014\.  Optimal multibinding unification for sharing and linearity analysis.  Theory and Practice of Logic Programming, 14, pp. 379–400.
  * Armstrong et al., (1998) Armstrong, T., Marriott, K., Schachte, P., and Søndergaard, H. 1998\.  Two classes of Boolean functions for dependency analysis.  Science of Computer Programming, 31, 1, pp. 3–45.
  * Bagnara et al., (2005) Bagnara, R., Zaffanella, E., and Hill, P. M. 2005\.  Enhanced sharing analysis techniques: A comprehensive evaluation.  Theory and Practice of Logic Programming, 5, 1–2, pp. 1–43.
  * Benton and Fischer, (2007) Benton, W. C. and Fischer, C. N. Interactive, scalable, declarative program analysis: From prototype to implementation.  In Leuschel, M. and Podelski, A., editors, PPDP ’07: Proceedings of the 9th ACM SIGPLAN international conference on Principles and practice of declarative programming 2007, pp. 13–24, New York, NY, USA. ACM.
  * Bruynooghe, (1991) Bruynooghe, M. 1991\.  A practical framework for the abstract interpretation of logic programs.  The Journal of Logic Programming, 10, 1/2/3 & 4, pp. 91–124.
  * Codish et al., (1995) Codish, M., Mulkers, A., Bruynooghe, M., de la Banda, M. G., and Hermenegildo, M. 1995\.  Improving abstract interpretations by combining domains.  ACM Transactions on Programming Languages and Systems, 17, 1, pp. 28–44.
  * Cortesi et al., (1996) Cortesi, A., Filé, G., and Winsborough, W. W. 1996\.  Optimal groundness analysis using propositional logic.  The Journal of Logic Programming, 27, 2, pp. 137–167.
  * Cousot and Cousot, (1979) Cousot, P. and Cousot, R. Systematic design of program analysis frameworks.  In Aho, A. V. and Zilles, S. N., editors, POPL ’79: Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages 1979, pp. 269–282, New York, NY, USA. ACM.
  * (13) Cousot, P. and Cousot, R. 1992a.  Abstract interpretation and applications to logic programs.  The Journal of Logic Programming, 13a, 2–3, pp. 103–179.
  * (14) Cousot, P. and Cousot, R. 1992b.  Abstract interpretation frameworks.  Journal of Logic and Computation, 2b, 4, pp. 511–549.
  * De Angelis et al., (2021) De Angelis, E., Fioravanti, F., Gallagher, J. P., Hermenegildo, M. V., Pettorossi, A., and Proietti, M. 2021\.  Analysis and transformation of constrained horn clauses for program verification.  Theory and Practice of Logic Programming, 22, 6, pp. 974–1042.
  * de la Banda and Hermenegildo, (1993) de la Banda, M. G. and Hermenegildo, M. A practical approach to the global analysis of CLP programs.  In Proceedings of the 1993 International Symposium on Logic Programming 1993, pp. 437–455, Cambridge, MA, USA. The MIT Press.
  * Gange et al., (2015) Gange, G., Navas, J. A., Schachte, P., Søndergaard, H., and Stuckey, P. J. 2015\.  Horn clauses as an intermediate representation for program analysis and transformation.  Theory and Practice of Logic Programming, 15, 4–5, pp. 526–542.
  * Giacobazzi et al., (2000) Giacobazzi, R., Ranzato, F., and Scozzari, F. 2000\.  Making abstract interpretations complete.  Journal of the ACM, 47, 2, pp. 361–416.
  * Hans and Winkler, (1992) Hans, W. and Winkler, S. 1992\.  Aliasing and groundness analysis of logic programs through abstract interpretation and its safety.  Technical Report 92-27, Technical University of Aachen (RWTH Aachen).  Available from http://sunsite.informatik.rwth-aachen.de/Publications/AIB. Last accessed Jan 10, 2024.
  * Henriksen and Gallagher, (2006) Henriksen, K. S. and Gallagher, J. P. Abstract interpretation of PIC programs through logic programming.  In 2006 Sixth IEEE International Workshop on Source Code Analysis and Manipulation 2006, pp. 184–196, Los Alamitos, CA, USA. IEEE Computer Society Press.
  * Hermenegildo and Rossi, (1995) Hermenegildo, M. V. and Rossi, F. 1995\.  Strict and nonstrict independent and-parallelism in logic programs: Correctness, efficiency, and compile-time conditions.  The Journal of Logic Programming, 22, 1, pp. 1–45.
  * Ivanović et al., (2013) Ivanović, D., Carro, M., and Hermenegildo, M. V. 2013\.  A sharing-based approach to supporting adaptation in service compositions.  Computing, 95, 6, pp. 453–492.
  * Jacobs and Langen, (1992) Jacobs, D. and Langen, A. 1992\.  Static analysis of logic programs for independent AND parallelism.  The Journal of Logic Programming, 13, 2–3, pp. 291–314.
  * King, (1994) King, A. A synergistic analysis for sharing and groundness which traces linearity.  In Sannella, D., editor, Programming Languages and Systems – ESOP ’94, 5th European Symposium on Programming, Edinburg, U.K., April 11–13, 1994. Proceedings 1994, volume 788 of Lecture Notes in Computer Science, pp. 363–378, Berlin Heidelberg. Springer.
  * King, (2000) King, A. 2000\.  Pair-sharing over rational trees.  The Journal of Logic Programming, 46, 1–2, pp. 139–155.
  * King and Longley, (1995) King, A. and Longley, M. 1995\.  Abstract matching can improve on abstract unification.  Technical Report 4-95*, University of Kent, Computing Laboratory, Canterbury, UK.  Available from http://www.cs.ukc.ac.uk/pubs/1995/64. Last accessed Oct 10, 2022.
  * Langen, (1990) Langen, A. 1990\.  Static Analysis for Independent And-parallelism in Logic Programs.  PhD thesis, University of Southern California, Los Angeles, California.
  * Le Charlier and Van Hentenryck, (1994) Le Charlier, B. and Van Hentenryck, P. 1994\.  Experimental evaluation of a generic abstract interpretation algorithm for PROLOG.  ACM Transactions on Programming Languages and Systems, 16, 1, pp. 35–101.
  * Muthukumar and Hermenegildo, (1991) Muthukumar, K. and Hermenegildo, M. V. Combined determination of sharing and freeness of program variables through abstract interpretation.  In Furukawa, K., editor, Logic Programming, Proceedings of the Eighth International Conference 1991, Logic Programming, pp. 49–63, Cambridge, MA, USA. The MIT Press.
  * Muthukumar and Hermenegildo, (1992) Muthukumar, K. and Hermenegildo, M. V. 1992\.  Compile-time derivation of variable dependency using abstract interpretation.  The Journal of Logic Programming, 13, 2–3, pp. 315–347.
  * Méndez-Lojo et al., (2008) Méndez-Lojo, M., Navas, J., and Hermenegildo, M. V. A flexible, (C)LP-based approach to the analysis of object-oriented programs.  In King, A., editor, Logic Based Program Synthesis and Transformation 17th International Workshop, LOPSTR 2007, Kongens Lyngby, Denmark, August, 23–24, 2007. Revised Selected Papers 2008, volume 4915 of Lecture Notes in Computer Science, pp. 154–168, Berlin Heidelberg. Springer.
  * Peralta et al., (1998) Peralta, J. C., Gallagher, J. P., and Sağlam, H. Analysis of imperative programs through analysis of constraint logic programs.  In Levi, G., editor, Static Analysis. 5th International Symposium, SAS ’98, Pisa, Italy, September 14–16, 1998, Proceedings 1998, volume 1503 of Lecture Notes in Computer Science, pp. 246–261, Berlin Heidelberg. Springer.
  * Søndergaard, (1986) Søndergaard, H. An application of abstract interpretation of logic programs: Occur check reduction.  In Robinet, B. and Wilhelm, R., editors, ESOP 86, European Symposium on Programming, Saarbrücken, Federal Republic of Germany, March 17-19, 1986. Proceedings 1986, volume 213 of Lecture Notes in Computer Science, pp. 327–338, Berlin Heidelberg. Springer.
  * Spoto et al., (2010) Spoto, F., Mesnard, F., and Payet, E. 2010\.  A termination analyzer for Java bytecode based on path-length.  ACM Transactions on Programming Languages and Systems, 32, 3, pp. 8:1–8:70.