11institutetext: Univ. Grenoble Alpes, CNRS, LIG, F-38000 Grenoble France

# Two Results on Separation Logic With Theory Reasoning

Mnacho Echenim 11 Nicolas Peltier 11

##  1 Introduction

In Separation Logic (see, e.g., [11, 18]), recursive data structures are
usually specified using inductively defined predicates. The recursive rules
defining the semantics of these predicates may be provided by the user. This
specification mechanism is similar to the definition of a recursive data type
in an imperative programming language. For instance, a nonempty list segment
may be specified by using the inductive rules below, where the atom
$x\mapsto(y)$ states that the memory location corresponding to $x$ is
allocated and refers to $y$. The symbol $*$ is a special logical connective
denoting the disjoint composition of heaps.

$\mathtt{ls}(x,y)\Leftarrow x\mapsto(y)\qquad\mathtt{ls}(x,y)\Leftarrow\exists
x^{\prime}~{}.~{}(x\mapsto(x^{\prime})*\mathtt{ls}(x^{\prime},y))$

Sorted lists with elements inside the interval $[u,v]$ may be specified as
follows.

$\mathtt{ils}(x,y,u,v)\Leftarrow(x\mapsto(y)\wedge x\leq v\wedge x\geq u)$
$\mathtt{ils}(x,y,u,v)\Leftarrow\exists
x^{\prime}~{}.~{}(x\mapsto(x^{\prime})*\mathtt{ils}(x^{\prime},y,x,v)\wedge
x\leq v\wedge x\geq u)$

Many verification tasks can be reduced to an entailment problem in this logic.
For example, to verify that some formula $\phi$ is a loop invariant, we have
to prove that the weakest pre-condition of $\phi$ w.r.t. a finite sequence of
transformations is a logical consequence of $\phi$. Since techniques exist for
computing automatically such pre-conditions, the problem may be reduced to an
entailment problem between two SL formulas. Entailment problems can also be
used to express typing properties. For instance one may have to check that the
entailment $\mathtt{ils}(x,y,u,v)\models\mathtt{ls}(x,y)$ holds, i.e., that a
sorted list is a list, that $v\leq
v^{\prime}\wedge\mathtt{ils}(x,y,u,v)\models\mathtt{ils}(x,y,u,v^{\prime})$
holds (if $v$ is an upper bound then any number greater than $v$ is also an
upper bound) or that
$\mathtt{ils}(x,y,u,v)*\mathtt{ils}(y,z,v,v^{\prime})\models\mathtt{ils}(x,y,u,v^{\prime})$
(the composition of two sorted lists is a sorted list). In general, the
entailment problem is undecidable [10], and a lot of effort has been devoted
to identifying decidable fragments and devising proof procedures, see e.g.,
[1, 2, 3, 8, 7, 4]. In particular, a very general class of decidable
entailment problems is described in [9]. This fragment does not allow for any
theory predicate other than equality and is defined by restricting the form of
the inductive rules, which must fulfill $3$ conditions, formally defined
below: the progress condition (every rule allocates a single memory location),
the connectivity condition (the set of allocated locations has a tree-shaped
structure) and the establishment condition (every existentially quantified
variable is eventually allocated). More recently, a $2$-$\mathsf{EXPTIME}$
algorithm was proposed for such entailments [14], and we showed in [5] that
this bound is tight. To tackle entailments such as those given above, one must
be able to combine spatial reasoning with theory reasoning, and the
combination of SL with data constraints has been considered by several authors
(see, e.g., [16, 17, 15, 19, 12]). It is therefore natural to ask whether the
above decidability result extends to the case where theory reasoning is
considered. In the present paper, we show that this is not the case, even for
very simple theories. More precisely, we establish two new results. First, we
show that the entailment problem is undecidable for rules satisfying the above
conditions if theory reasoning is allowed (Theorem 3.1). The result holds for
a very wide class of theories, even for theories with a very low expressive
power. For instance, it holds for the natural numbers with only the successor
function, or with only the predicate $\leq$ (interpreted as usual). Second, we
show that every entailment can be reduced to an entailment not containing
equality (Theorem 4.1). The intuition is that all the equality and disequality
constraints can be encoded in the formulas describing the shape of the data
structures. The transformation increases the number of rules exponentially but
it increases the size of the rules only polynomially (hence it preserves the
complexity results in [6]). This result shows that the addition of the
equality predicate does not increase the expressive power. It may be useful to
facilitate the definition of proof procedures for the considered fragment.

##  2 Preliminaries

In this section, we define the syntax and semantics of the fragment of
separation logic that is considered in the paper (see for instance [13, 18, 9]
for more details).

#### Syntax.

Let ${\cal V}$ be a countably infinite set of variables. We consider a set
${\cal P}_{\cal T}$ of ${\cal T}$-predicates (or theory predicates, denoting
relations in an underlying theory of locations) and a set ${\cal P}_{S}$ of
spatial predicates, disjoint from ${\cal P}_{\cal T}$. Each symbol $p\in{\cal
P}_{\cal T}\cup{\cal P}_{S}$ is associated with a unique arity $\\#(p)$. We
assume that ${\cal P}_{\cal T}$ contains in particular two binary symbols
$\approx$ and $\not\approx$ and a nullary symbol $\mathtt{false}$.

###### Definition 1

Let $\kappa$ be some fixed natural number. The set of $SL$-formulas (or simply
formulas) $\phi$ is inductively defined as follows:

$\phi:=\mathtt{emp}\;\|\;x\mapsto(y_{1},\dots,y_{\kappa})\;\|\;\phi_{1}\vee\phi_{2}\;\|\;\phi_{1}*\phi_{2}\|\;p(x_{1},\dots,x_{\\#(p)})\;\|\;\exists
x.~{}\phi_{1}$

where $\phi_{1},\phi_{2}$ are $SL$-formulas, $p\in{\cal P}_{\cal T}\cup{\cal
P}_{S}$ and $x,x_{1},\dots,x_{\\#(p)},y_{1},\dots,y_{\kappa}$ are variables.

A formula of the form $x\mapsto(y_{1},\dots,y_{\kappa})$ is called a points-to
atom, and a formula $p(x_{1},\dots,x_{\\#(p)})$ with $p\in{\cal P}_{S}$ is
called a predicate atom. A spatial atom is either a points-to atom or a
predicate atom. A ${\cal T}$-atom is a formula of the form
$p(x_{1},\dots,x_{\\#(p)})$ with $p\in{\cal P}_{\cal T}$. An atom is either a
spatial atom or a ${\cal T}$-atom. A ${\cal T}$-formula is either
$\mathtt{emp}$ or a separating conjunction of ${\cal T}$-atoms. A formula of
the form $\exists x_{1}.\dots.\exists x_{n}.~{}\phi$ (with $n\geq 0$) is
denoted by $\exists\mathbf{x}.~{}\phi$, where
$\mathbf{x}=(x_{1},\dots,x_{n})$. A formula is predicate-free (resp.
disjunction-free, resp. quantifier-free) if it contains no predicate symbol in
${\cal P}_{S}$ (resp. no occurrence of $\vee$, resp. of $\exists$). It is in
prenex form if it is of the form $\exists\mathbf{x}.\phi$, where $\phi$ is
quantifier-free and $\mathbf{x}$ is a possibly empty vector of variables. A
symbolic heap is a prenex disjunction-free formula, i.e., a formula of the
form $\exists\mathbf{x}.\phi$, where $\phi$ is a separating conjunction of
atoms.

Let $\mathit{fv}(\phi)$ be the set of variables freely occurring in $\phi$. We
assume (using $\alpha$-renaming if needed) that all existential variables are
distinct from free variables and that distinct occurrences of quantifiers bind
distinct variables. A substitution $\sigma$ is a function mapping variables to
variables. The domain $\mathit{dom}(\sigma)$ of a substitution $\sigma$ is the
set of variables $x$ such that $\sigma(x)\not=x$, and we let
$\mathit{img}(\sigma)=\sigma(\mathit{dom}(\sigma))$. For any expression
(variable, tuple of variables or formula) $e$, we denote by $e\sigma$ the
expression obtained from $e$ by replacing every free occurrence of a variable
$x$ by $\sigma(x)$ and by $\\{x_{i}\leftarrow y_{i}\mid 1\leq i\leq n\\}$
(where the $x_{1},\dots,x_{n}$ are pairwise distinct) the substitution such
that $\sigma(x_{i})=y_{i}$ and
$\mathit{dom}(\sigma)\subseteq\\{x_{1},\dots,x_{n}\\}$. For all sets $E$,
$\mathit{card}(E)$ is the cardinality of $E$. For all sequences or words $w$,
$\|w\|$ denotes the length of $w$. We sometimes identify vectors with sets, if
the order is unimportant, e.g., we may write $\mathbf{x}\setminus\mathbf{y}$
to denote the vector formed by the components of $\mathbf{x}$ that do not
occur in $\mathbf{y}$.

We assume that the symbols in ${\cal P}_{S}\cup{\cal P}_{\cal T}\cup{\cal V}$
are words over a finite alphabet of some constant size, strictly greater than
$1$. For any expression $e$, we denote by $\mathit{size}(e)$ the size of $e$,
i.e., the number of occurrences of symbols111Each symbol $s$ in ${\cal
P}_{S}\cup{\cal P}_{\cal T}\cup{\cal V}$ is counted with a weight equal to its
length $\|s\|$, and all the logical symbols have weight $1$. in $e$. We define
the width of a formula as follows:

$\mathit{width}(\phi_{1}\vee\phi_{2})$ | $=$ | $\max(\mathit{width}(\phi_{1}),\mathit{width}(\phi_{2}))$ |  $\mathit{width}(\exists x.\phi)$ | $=$ | $\mathit{width}(\phi)+\mathit{size}(\exists x)$
---|---|---|---|---|---
$\mathit{width}(\phi_{1}*\phi_{2})$ | $=$ | $\mathit{width}(\phi_{1})+\mathit{width}(\phi_{2})+1$ |  |  |
$\mathit{width}(\phi)$ | $=$ |  $\mathit{size}(\phi)$ if $\phi$ is an atom |  |  |

Note that $\mathit{width}(\phi)$ coincides with $\mathit{size}(\phi)$ if
$\phi$ is disjunction-free.

#### Inductive Rules.

The semantics of the predicates in ${\cal P}_{S}$ is given by user-defined
inductive rules. To ensure decidability in the case where the theory only
contains the equality predicate, these rules must satisfy some additional
conditions (defined in [9]):

###### Definition 2

A (progressing and connected) set of inductive rules (pc-SID) ${\cal R}$ is a
finite set of rules of the form
$p(x_{1},\dots,x_{n})\Leftarrow\exists\mathbf{u}.~{}x_{1}\mapsto(y_{1},\dots,y_{\kappa})*\phi$
where
$\mathit{fv}(x_{1}\mapsto(y_{1},\dots,y_{\kappa})*\phi)\subseteq\\{x_{1},\ldots,x_{n}\\}\cup\mathbf{u}$,
$\phi$ is a possibly empty separating conjunction of predicate atoms and
${\cal T}$-formulas, and for every predicate atom $q(z_{1},\dots,z_{\\#(q)})$
occurring in $\phi$, we have $z_{1}\in\\{y_{1},\dots,y_{\kappa}\\}$. We let
$\mathit{size}(p(\mathbf{x})\Leftarrow\phi)=\mathit{size}(p(\mathbf{x}))+\mathit{size}(\phi)$,
$\mathit{size}({\cal R})=\Sigma_{\rho\in{\cal R}}\mathit{size}(\rho)$ and
$\mathit{width}({\cal R})=\max_{\rho\in{\cal R}}\mathit{size}(\rho)$.

In the following, ${\cal R}$ always denotes a pc-SID. Note that the right-hand
side of every inductive rule contains exactly one points-to atom, the left-
hand side of which is the first argument $x_{1}$ of the predicate symbol (this
condition is referred to as the progress condition), and that this points-to
atom contains the first argument of every predicate atom on the right-hand
side of the rule (the connectivity condition).

###### Definition 3

We write $p(x_{1},\dots,x_{\\#(p)})\Leftarrow_{{\cal R}}\phi$ if ${\cal R}$
contains a rule (up to $\alpha$-renaming)
$p(y_{1},\dots,y_{\\#(p)})\Leftarrow\psi$, where $x_{1},\dots,x_{\\#(p)}$ are
not bound in $\psi$, and $\phi=\psi\\{y_{i}\leftarrow x_{i}\mid
i\in\\{1,\dots,{\\#(p)}\\}\\}$.

The relation $\Leftarrow_{{\cal R}}$ is extended to all formulas as follows:
$\phi\Leftarrow_{{\cal R}}\phi^{\prime}$ if one of the following conditions
holds: (i) $\phi=\phi_{1}\bullet\phi_{2}$ (modulo AC, with
$\bullet\in\\{*,\vee\\}$), $\phi_{1}\Leftarrow_{{\cal R}}\phi_{1}^{\prime}$,
no free or existential variable in $\phi_{2}$ is bound in $\phi_{1}^{\prime}$
and $\phi^{\prime}=\phi_{1}^{\prime}\bullet\phi_{2}$; or (ii) $\phi=\exists
x.~{}\psi$, $\psi\Leftarrow_{{\cal R}}\psi^{\prime}$, $x$ is not bound in
$\psi^{\prime}$ and $\phi^{\prime}=\exists x.~{}\psi^{\prime}$. We denote by
$\Leftarrow_{{\cal R}}^{+}$ the transitive closure of $\Leftarrow_{{\cal R}}$,
and by $\Leftarrow_{{\cal R}}^{*}$ its reflexive and transitive closure. A
formula $\psi$ such that $\phi\Leftarrow_{{\cal R}}^{*}\psi$ is called an
${\cal R}$-unfolding of $\phi$. We denote by $\geq_{{\cal R}}$ the least
transitive and reflexive binary relation on ${\cal P}_{S}$ such that
$p\geq_{{\cal R}}q$ holds if ${\cal R}$ contains a rule of the form
$p(y_{1},\dots,y_{\\#(p)})\Leftarrow\psi$, where $q$ occurs in $\psi$. If
$\phi$ is a formula, we write $\phi\geq_{{\cal R}}q$ if $p\geq_{{\cal R}}q$
for some $p\in{\cal P}_{S}$ occurring in $\phi$.

#### Semantics.

###### Definition 4

Let ${\cal L}$ be a countably infinite set of locations. An SL-structure is a
pair $(\mathfrak{s},\mathfrak{h})$ where $\mathfrak{s}$ is a store, i.e. a
total function from ${\cal V}$ to ${\cal L}$, and $\mathfrak{h}$ is a heap,
i.e. a partial finite function from ${\cal L}$ to ${\cal L}^{\kappa}$ (written
as a relation: $\mathfrak{h}(\ell)=(\ell_{1},\dots,\ell_{\kappa})$ iff
$(\ell,\ell_{1},\dots,\ell_{\kappa})\in\mathfrak{h}$). The size of a structure
$(\mathfrak{s},\mathfrak{h})$ is the cardinality of
$\mathit{dom}(\mathfrak{h})$.

For every heap $\mathfrak{h}$, we define:
$\mathit{loc}(\mathfrak{h})=\\{\ell_{i}\mid(\ell_{0},\dots,\ell_{\kappa})\in\mathfrak{h},i=0,\dots,\kappa\\}$.
A location $\ell$ (resp. a variable $x$) is allocated in a heap $\mathfrak{h}$
(resp. in a structure ($\mathfrak{s},\mathfrak{h}$)) if
$\ell\in\mathit{dom}(\mathfrak{h})$ (resp.
$\mathfrak{s}(x)\in\mathit{dom}(\mathfrak{h})$). Two heaps
$\mathfrak{h}_{1},\mathfrak{h}_{2}$ are disjoint if
$\mathit{dom}(\mathfrak{h}_{1})\cap\mathit{dom}(\mathfrak{h}_{2})=\emptyset$,
in this case $\mathfrak{h}_{1}\uplus\mathfrak{h}_{2}$ denotes the union of
$\mathfrak{h}_{1}$ and $\mathfrak{h}_{2}$.

Let $\models_{{\cal T}}$ be a satisfiability relation between stores and
${\cal T}$-formulas, satisfying the following properties:
$\mathfrak{s}\models_{{\cal T}}x\approx y$ (resp. $\mathfrak{s}\models_{{\cal
T}}x\not\approx y$) iff $\mathfrak{s}(x)=\mathfrak{s}(y)$ (resp.
$\mathfrak{s}(x)\not=\mathfrak{s}(y)$), $\mathfrak{s}\not\models_{{\cal
T}}\mathtt{false}$ and $\mathfrak{s}\models_{{\cal T}}\chi*\xi$ iff
$\mathfrak{s}\models_{{\cal T}}\chi$ and $\mathfrak{s}\models_{{\cal T}}\xi$.
For all ${\cal T}$-formulas $\chi,\xi$, we write $\chi\models_{{\cal T}}\xi$
if $\mathfrak{s}\models_{{\cal T}}\chi\implies\mathfrak{s}\models_{{\cal
T}}\xi$ holds for all stores $\mathfrak{s}$.

###### Definition 5

Given formula $\phi$, a pc-SID ${\cal R}$ and a structure
$(\mathfrak{s},\mathfrak{h})$, we write
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$ and say that
$(\mathfrak{s},\mathfrak{h})$ is an ${\cal R}$-model (or simply a model if
${\cal R}$ is clear from the context) of $\phi$ if one of the following
conditions holds.

  * •

$\phi=x\mapsto(y_{1},\dots,y_{\kappa})$ and
$\mathfrak{h}=\\{(\mathfrak{s}(x),\mathfrak{s}(y_{1}),\dots,\mathfrak{s}(y_{\kappa}))\\}$.

  * •

$\phi$ is a ${\cal T}$-formula, $\mathfrak{h}=\emptyset$ and
$\mathfrak{s}\models_{{\cal T}}\phi$.

  * •

$\phi=\phi_{1}\vee\phi_{2}$ and $(\mathfrak{s},\mathfrak{h})\models_{{\cal
R}}\phi_{i}$, for some $i=1,2$.

  * •

$\phi=\phi_{1}*\phi_{2}$ and there exist disjoint heaps
$\mathfrak{h}_{1},\mathfrak{h}_{2}$ such that
$\mathfrak{h}=\mathfrak{h}_{1}\uplus\mathfrak{h}_{2}$ and
$(\mathfrak{s},\mathfrak{h}_{i})\models_{{\cal R}}\phi_{i}$, for all $i=1,2$.

  * •

$\phi=\exists x.~{}\phi$ and
$(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\phi$, for some store
$\mathfrak{s}^{\prime}$ coinciding with $\mathfrak{s}$ on all variables
distinct from $x$.

  * •

$\phi=p(x_{1},\dots,x_{\\#(p)})$, $p\in{\cal P}_{S}$ and
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\psi$ for some $\psi$ such that
$\phi\Leftarrow_{{\cal R}}\psi$.

If $\Gamma$ is a sequence of formulas, then we write
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\Gamma$ if
$(\mathfrak{s},\mathfrak{h})$ satisfies at least one formula in $\Gamma$.

We emphasize that a ${\cal T}$-formula is satisfied only in structures with
empty heaps. This convention is used to simplify notations, because it avoids
having to consider both standard and separating conjunctions. Note that
Definition 5 is well-founded because of the progress condition: the size of
$\mathfrak{h}$ decreases at each recursive call of a predicate atom. We write
$\phi\models_{{\cal R}}\psi$ if every ${\cal R}$-model of $\phi$ is an ${\cal
R}$-model of $\psi$ and $\phi\equiv_{{\cal R}}\psi$ if $\phi\models_{{\cal
R}}\psi$ and $\psi\models_{{\cal R}}\phi$.

Every formula can be transformed into prenex form using the well-known
equivalences: $(\exists x.\phi)\bullet\psi\equiv\exists x.(\phi\bullet\psi)$,
for all $\bullet\in\\{\vee,*\\}$, where $x\not\in\mathit{fv}(\psi)$.

#### Establishment.

The notion of establishment [9] is defined as follows:

###### Definition 6

A pc-SID is established if for every atom $\alpha$, every predicate-free
formula $\exists\mathbf{x}.\phi$ such that $\alpha\Leftarrow_{{\cal
R}}^{*}\exists\mathbf{x}.\phi$ (up to a transformation into prenex form) and
$\phi$ is quantifier-free, and every $x\in\mathbf{x}$, $\phi$ is of the form
$x^{\prime}\mapsto(y_{1},\dots,y_{\kappa})*\chi*\psi$, where $\chi$ is a
separating conjunction of equations (possibly $\mathtt{emp}$) such that
$\chi\models_{{\cal T}}x\approx x^{\prime}$.

In the remainder of the paper, we assume that every considered pc-SID is
established.

#### Sequents.

We consider sequents denoting entailment problems and defined as follows:

###### Definition 7

A sequent is an expression of the form $\phi_{0}\vdash_{{\cal
R}}\phi_{1},\dots,\phi_{n}$, where ${\cal R}$ is a pc-SID and
$\phi_{0},\dots,\phi_{n}$ are formulas. A sequent is disjunction-free if
$\phi_{0},\dots,\phi_{n}$ are disjunction-free, and established if ${\cal R}$
is established. We define:

$\displaystyle\mathit{size}(\phi_{0}\vdash_{{\cal R}}\phi_{1},\dots,\phi_{n})$
$\displaystyle=$
$\displaystyle\Sigma_{i=0}^{n}\mathit{size}(\phi_{i})+\mathit{size}({\cal
R}),\qquad\mathit{fv}(\phi_{1},\dots,\phi_{n})=\bigcup_{i=0}^{n}\mathit{fv}(\phi_{i}),$
$\displaystyle\mathit{width}(\phi_{0}\vdash_{{\cal
R}}\phi_{1},\dots,\phi_{n})$ $\displaystyle=$
$\displaystyle\max\\{\mathit{width}(\phi_{i}),\mathit{width}({\cal
R}),\mathit{card}(\bigcup_{i=0}^{n}\mathit{fv}(\phi_{i}))\mid 0\leq i\leq
n\\}.$

###### Definition 8

A structure $(\mathfrak{s},\mathfrak{h})$ is a countermodel of a sequent
$\phi\vdash_{{\cal R}}\Gamma$ iff $\mathfrak{s}$ is injective,
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$ and
$(\mathfrak{s},\mathfrak{h})\not\models_{{\cal R}}\Gamma$. A sequent is valid
if it has no countermodel. Two sequents are equivalent if they are both valid
or both non-valid222Hence two non-valid sequents with different countermodels
are equivalent..

The restriction to injective countermodels is for technical convenience only
and does not entail any loss of generality.

##  3 An Undecidability Result

This section contains the main result of the paper. It shows that no
terminating procedure for checking the validity of (established) sequents
possibly exists, even for theories with a very low expressive power.

###### Theorem 3.1

The validity problem is undecidable for established sequents
$\phi\vdash_{{\cal R}}\psi$ if ${\cal P}_{\cal T}$ contains predicates $S$ and
$\overline{S}$, where:

  * •

$S$ is interpreted as a relation ${\mathfrak{S}}$ satisfying the following
property: there exists a set of pairwise distinct locations
$\\{\alpha_{i},\alpha_{i}^{\prime},\alpha_{i}^{\prime\prime}\mid
i\in{\mathbb{N}}\\}$ such that for all $i\in{\mathbb{N}}$,
$(\alpha_{i},\alpha_{i}^{\prime})\in{\mathfrak{S}}$,
$(\alpha_{i}^{\prime\prime},\alpha_{i}^{\prime})\not\in{\mathfrak{S}}$, and
for all locations
$\ell\in\\{\alpha_{j},\alpha_{j}^{\prime},\alpha_{j}^{\prime\prime}\mid
j\in{\mathbb{N}}\\}$ if $\alpha_{i}\not=\ell$,
$(\alpha_{i},\ell)\in{\mathfrak{S}}$ and
$(\alpha_{i}^{\prime\prime},\ell)\not\in{\mathfrak{S}}$, then
$\ell=\alpha_{i}^{\prime}$;

  * •

$\overline{S}(x,y)$ and $\neg S(x,y)$ are interpreted equivalently when $x$
and $y$ refer to distinct locations.

For instance, the hypotheses of Theorem 3.1 are trivially satisfied on the
natural numbers if ${\mathfrak{S}}$ is the successor function or if
${\mathfrak{S}}$ is the usual order $\leq$, and $\overline{S}$ is $\geq$ (with
$\alpha_{i}=3.i$, $\alpha_{i}^{\prime}=3.i+1$,
$\alpha_{i}^{\prime\prime}=3.i+2$ in both cases, since
$\alpha_{i}+1\approx\ell\Rightarrow\alpha_{i}^{\prime}\approx\ell$ and
$\alpha_{i}\leq\ell\wedge\alpha_{i}^{\prime\prime}>\ell\wedge\ell\not=\alpha_{i}\Rightarrow\alpha_{i}^{\prime}\approx\ell$.
). More generally, the conditions hold if the domain is infinite and
${\mathfrak{S}}$ is any injective function $f$ such that $f(x)\not=x$. In this
case, the sequences $\alpha_{i},\alpha_{i}^{\prime},\alpha_{i}^{\prime\prime}$
may be constructed inductively: for every $i\in{\mathbb{N}}$, $\alpha_{i}$ is
any element $e$ such that both $e$ and $f(e)$ do not occur in
$\\{\alpha_{j},\alpha_{j}^{\prime},\alpha_{j}^{\prime\prime}\mid j<i\\}$,
$\alpha_{i}^{\prime}$ is $f(\alpha_{i})$ and $\alpha_{i}^{\prime\prime}$ is
any element not occurring in
$\\{\alpha_{j},\alpha_{j}^{\prime},\alpha_{j}^{\prime\prime}\mid
j<i\\}\cup\\{\alpha_{i},\alpha_{i}^{\prime}\\}$. Note that in this case the
locations $\alpha_{i}^{\prime\prime}$ are actually irrelevant, but these
locations play an essential rôle in the undecidability proof when
${\mathfrak{S}}$ is $\leq$. The remainder of the section is devoted the proof
of Theorem 3.1.

###### Proof

The proof goes by a reduction from the Post Correspondence Problem (PCP). We
recall that the PCP consists in determining, given two sequences of words
$u=(u_{1},\dots,u_{n})$ and $v=(v_{1},\dots,v_{n})$, whether there exists a
nonempty sequence $(i_{1},\dots,i_{k})\in\\{1,\dots,n\\}^{k}$ such that
$u_{i_{1}}.\dots,u_{i_{k}}=v_{i_{1}}.\dots,v_{i_{k}}$. It is well-known that
this problem is undecidable. We assume, w.l.o.g., that $\|u_{i}\|>1$ and
$\|v_{i}\|>1$ for all $i\in\\{1,\dots,n\\}$. A word $w$ such that
$w=u_{i_{1}}.\dots,u_{i_{k}}=v_{i_{1}}.\dots,v_{i_{k}}$ is called a witness.
Positions inside words of the sequences $(u_{1},\dots,u_{n})$ and
$(v_{1},\dots,v_{n})$ will be denoted by pairs $(i,j)$, encoding the $j$-nth
character of the words $u_{i}$ or $v_{i}$. More formally, if $p=(i,j)$, and
$w\in\\{u,v\\}$, then we denote by $w(p)$ the $j$-th symbol of the word
$w_{i}$, provided this symbol is defined. We write $p\triangleleft q$ if both
$u(p)$ and $v(q)$ are defined and $u(p)=v(q)$.

Let $m=\max\\{\|u_{i}\|,\|v_{i}\|\mid i\in\\{1,\dots,n\\}\\}$. We denote by
$\mathtt{P}$ the set of pairs of the form $(i,j)$ with $i\in\\{1,\dots,n\\}$
and $j\in\\{1,\dots,m\\}$, and by $\mathtt{B}$ the set of pairs of the form
$(i,1)$. For $w\in\left\\{u,v\right\\}$, we denote by $\mathtt{E}_{w}$ the set
of pairs of the form $(i,\|w_{i}\|)$, where $i\in\\{1,\dots,n\\}$, and we
write $(i,j)\rightarrow^{w}(i^{\prime},j^{\prime})$ either $i^{\prime}=i$,
$j<\|w_{i}\|$ and $j^{\prime}=j+1$, or $j=\|w_{i}\|$ and $j^{\prime}=1$. Note
that $i^{\prime}$ is arbitrary in the latter case (intuitively
$(i,j)\rightarrow^{w}(i^{\prime},j^{\prime})$ states that the character
corresponding to the position $(i,j)$ may be followed in a witness by the
character at position $(i^{\prime},j^{\prime})$). Let $\mathbf{v}$ be a vector
of variables, where all elements $p\in\mathtt{P}$ are associated with pairwise
distinct variables in $\mathbf{v}$. To simplify notations, we will also denote
by $p$ the variable associated with $p$. We assume the vector $\mathbf{v}$
also contains a special variable $\mathrm{\bot}$, distinct from the variables
$p\in\mathtt{P}$. We construct a representation of potential witnesses as
heaps. The encoding is given for $\kappa=6$, although in principle this
encoding could be defined with $\kappa=2$ by encoding tuples as binary trees.
Witnesses are encoded by linked lists, with links on the last argument, and
starting with a dummy element $(\mathrm{\bot},\dots,\mathrm{\bot})$. Except
for the first dummy element, each location in the list refers to two locations
associated with pairs $p,q\in\mathtt{P}$ denoting positions inside the two
sequences $u_{1},\dots,u_{n}$ and $v_{1},\dots,v_{n}$ respectively, and to
three additional allocated locations the rôle of which will be detailed below.

$W(x,\mathbf{v})$ | $\Leftarrow$ | $\exists x^{\prime}.~{}x\mapsto(\mathrm{\bot},\mathrm{\bot},\mathrm{\bot},\mathrm{\bot},\mathrm{\bot},x^{\prime})*W_{p,p}(x^{\prime},\mathbf{v})$
---|---|---
|  |  where $p\in\mathtt{B}$
$W_{p,q}(x,\mathbf{v})$ | $\Leftarrow$ | $\exists x^{\prime},y,z,u.~{}x\mapsto(p,q,y,z,u,x^{\prime})*W_{p^{\prime},q^{\prime}}(x^{\prime},\mathbf{v})*P(y,\mathrm{\bot})*P(z,\mathrm{\bot})$
|  |  $*\ P(u,\mathrm{\bot})$ where $p\triangleleft q$, $p\rightarrow^{u}p^{\prime}$ and $q\rightarrow^{v}q^{\prime}$
$W_{p,q}(x,\mathbf{v})$ | $\Leftarrow$ | $\exists y,z,u.~{}x\mapsto(p,q,y,z,u,\mathrm{\bot})*P(y,\mathrm{\bot})*P(z,\mathrm{\bot})$
|  |  $*\ P(u,\mathrm{\bot})$ where $p=(i,\|u_{i}\|)$, $q=(i,\|v_{i}\|)$, and $p\triangleleft q$
$P(x,y)$ | $\Leftarrow$ | $x\mapsto(y,y,y,y,y,y)$

By construction, the structures that validate $W(x,\mathbf{v})$ are of the
form $(\mathfrak{s},\mathfrak{h})$, where the store $\mathfrak{s}$ verifies:

  * •

$\mathfrak{s}(x)=\ell$ and $\mathfrak{s}(\mathrm{\bot})=\ell^{\prime}$;

  * •

for all $i=1,\dots,m^{\prime}$, $\mathfrak{s}(p_{i})=\ell^{p}_{i}$ and
$\mathfrak{s}(q_{i})=\ell^{q}_{i}$, where $p_{i},q_{i}\in\mathtt{P}$ are such
that $p_{i}\triangleleft q_{i}$, $p_{i}\rightarrow^{u}p_{i+1}$ and
$q_{i}\rightarrow^{v}q_{i+1}$,

and the heap $\mathfrak{h}$ is of the form (with
$\ell_{m^{\prime}+1}=\ell^{\prime}$):

$\displaystyle\mathfrak{h}\ =\
\left\\{(\ell,\ell^{\prime},\ell^{\prime},\ell^{\prime},\ell^{\prime},\ell^{\prime},\ell_{1})\right\\}$
$\displaystyle\cup$
$\displaystyle\left\\{(\ell_{i},\ell^{p}_{i},\ell^{q}_{i},\ell^{y}_{i},\ell^{z}_{i},\ell^{u}_{i},\ell_{i+1})\,\|\>i=1,\ldots,m^{\prime}\right\\}$
$\displaystyle\cup$
$\displaystyle\left\\{(\ell^{y}_{i},\ell^{\prime},\ell^{\prime},\ell^{\prime},\ell^{\prime},\ell^{\prime},\ell^{\prime})\,\|\>i=1,\ldots,m^{\prime}\right\\}$
$\displaystyle\cup$
$\displaystyle\left\\{(\ell^{z}_{i},\ell^{\prime},\ell^{\prime},\ell^{\prime},\ell^{\prime},\ell^{\prime},\ell^{\prime})\,\|\>i=1,\ldots,m^{\prime}\right\\}$
$\displaystyle\cup$
$\displaystyle\left\\{(\ell^{u}_{i},\ell^{\prime},\ell^{\prime},\ell^{\prime},\ell^{\prime},\ell^{\prime},\ell^{\prime})\,\|\>i=1,\ldots,m^{\prime}\right\\}.$

Still by construction, we have $p_{1}=q_{1}\in\mathtt{B}$,
$p_{m^{\prime}}\in\mathtt{E}_{u}$ and $q_{m^{\prime}}\in\mathtt{E}_{v}$, and
there exists $i$ such that $p_{m^{\prime}}$ and $q_{m^{\prime}}$ are of the
form $(i,\|u_{i}\|)$ and $(i,\|v_{i}\|)$, respectively. This entails that the
words $u(p_{1}).\dots,u(p_{m^{\prime}})$ and
$v(p_{1}).\dots,v(p_{m^{\prime}})$ are of form $u_{i_{1}}.\dots.u_{i_{k}}$ and
$v_{j_{1}}.\dots.v_{j_{k^{\prime}}}$, for some sequences $(i_{1},\dots,i_{k})$
and $(j_{1},\dots,j_{k^{\prime}})$ of elements in $\\{1,\dots,n\\}$, and both
words are identical. However the sequences $(i_{1},\dots,i_{k})$ and
$(j_{1},\dots,j_{k^{\prime}})$ may be distinct (but we have $i_{1}=j_{1}$ and
$i_{k}=j_{k^{\prime}}$). To check that the PCP has a solution, we must
therefore verify that there exists a structure of the form above such that
$(i_{1},\dots,i_{k})=(j_{1},\dots,j_{k^{\prime}})$. To this purpose, we
introduce predicates that are satisfied when this condition does not hold,
i.e., such that either $k\neq k^{\prime}$ or $i_{l}\neq j_{l}$ for some
$l\in\\{2,\dots,k-1\\}$. This is done by using the additional locations
$\ell^{y}_{i}$, $\ell^{z}_{i}$ and $\ell^{u}_{i}$ to relate the indices
$I_{l}=\|u_{i_{1}}.\dots,u_{i_{l-1}}\|+1$ and
$J_{l}=\|v_{j_{1}}.\dots,v_{j_{l-1}}\|+1$, corresponding to the beginning of
the words $u_{i_{l}}$ and $v_{j_{l}}$ respectively in
$u_{i_{1}}.\dots.u_{i_{k}}$ and $v_{j_{1}}.\dots.v_{j_{k^{\prime}}}$. The
predicates relate the locations of the form $\ell^{y}_{i}$, $\ell^{z}_{i}$ and
$\ell^{u}_{i}$ using the relation ${\mathfrak{S}}$. More precisely, they are
associated with rules that guarantee that all the countermodels of the right-
hand side of the sequent will satisfy the following properties:

  1. 1.

$k=k^{\prime}$ and for all $l\in\\{1,\dots,k\\}$,
$(\ell^{y}_{I_{l}},\ell^{z}_{J_{l}})\in{\mathfrak{S}}$ and
$(\ell^{u}_{I_{l}},\ell^{z}_{J_{l}})\not\in{\mathfrak{S}}$.

  2. 2.

$i_{l}=j_{l}$ for $1\leq l\leq k$.

Note that the hypothesis of the theorem ensures that the locations
$\ell^{y}_{i}$, $\ell^{z}_{i}$ and $\ell^{u}_{i}$ can be chosen in such a way
that there is a unique location $\ell^{z}_{i}$ satisfying
$(\ell^{y}_{I_{l}},\ell^{z}_{i})\in{\mathfrak{S}}\wedge(\ell^{u}_{J_{l}},\ell^{z}_{i})\notin{\mathfrak{S}}$,
thus property $1$ above can be used to relate the indices $I_{l}$ and $J_{l}$,
which, in turns, allows us to enforce property $2$. Two predicates are used to
guarantee that condition 1 holds for the countermodels. Predicate $A$ is
satisfied by those structures for which the condition is not satisfied for
$l=1$, and $B$ is satisfied for those structures for which either $k\neq
k^{\prime}$ or there is an $l\in\\{1,\dots,k-1\\}$ such that the condition is
satisfied at $l$, but not at $l+1$. Thus the structures that satisfy
$W(x,\mathbf{v})$ and that are countermodels of the disjunction of $A$ and $B$
are exactly the structures for which $k=k^{\prime}$ and
$(\ell^{y}_{I_{l}},\ell^{z}_{J_{l}})\in{\mathfrak{S}}\wedge(\ell^{u}_{I_{l}},\ell^{z}_{J_{l}})\notin{\mathfrak{S}}$
for $l=1,\ldots,k$. Predicate $C$ is then used to guarantee that for all
$1\leq l\leq k$, $p_{I_{l}}=q_{J_{l}}$: this predicate is satisfied by the
structures for which there is an $l$ such that
$(\ell^{y}_{I_{l}},\ell^{z}_{J_{l}})\in{\mathfrak{S}}\wedge(\ell^{u}_{I_{l}},\ell^{z}_{J_{l}})\notin{\mathfrak{S}}$
holds but $p_{I_{l}}\neq q_{J_{l}}$. We first give the rules for predicate
$A$. For conciseness, we allow for disjunctions in the right-hand side of the
rules (they can be eliminated by transformation into dnf).

$A(x,\mathbf{v})$ | $\Leftarrow$ | $\exists x^{\prime}.~{}x\mapsto(\mathrm{\bot},\mathrm{\bot},\mathrm{\bot},\mathrm{\bot},\mathrm{\bot},x^{\prime})*A^{\prime}(x^{\prime},\mathbf{v})$
---|---|---
$A^{\prime}(x,\mathbf{v})$ | $\Leftarrow$ | $\exists x^{\prime},y,z,u.~{}x\mapsto(p,q,y,z,u,x^{\prime})*W_{p^{\prime},q^{\prime}}(x,\mathbf{v})*P(y,\mathrm{\bot})$
|  |  $\qquad*\ P(z,\mathrm{\bot})*P(u,\mathrm{\bot})*(\overline{S}(y,z)\vee S(u,z))$, for every $p,q,p^{\prime},q^{\prime}\in\mathtt{P}$

Note that since $y,z,u$ are allocated in distinct predicates, they must be
distinct, hence $\overline{S}(y,z)$ is equivalent to $\neg S(y,z)$ and
$S(u,z)$ is equivalent to $\neg\overline{S}(u,z)$.

We now define the rules for predicate $B$, which is meant to ensure that the
condition “$(\ell^{y}_{I_{l}},\ell^{z}_{J_{l}})\in{\mathfrak{S}}$ and
$(\ell^{u}_{I_{l}},\ell^{z}_{J_{l}})\not\in{\mathfrak{S}}$” ($\dagger$)
propagates, i.e., that if it holds for some $l$ then it also holds for $l+1$.
This predicate has additional parameters
$y,y^{\prime},z,z^{\prime},u,u^{\prime}$ corresponding to the locations
$\ell^{y}_{I_{l}},\ell^{y}_{I_{l+1}},\ell^{z}_{J_{j}},\ell^{z}_{J_{j+1}},\ell^{u}_{I_{l}},\ell^{u}_{I_{l+1}}$
which “break” the propagation of $(\dagger)$. By definition
$y,y^{\prime},z,z^{\prime},u,u^{\prime}$ must be chosen in such a way that the
${\cal T}$-formula
$S(y,z)*\overline{S}(u,z)*(\overline{S}(y^{\prime},z^{\prime})\vee
S(u^{\prime},z^{\prime}))$ holds. The predicates $B_{a,b}$ with
$a,b\in\\{0,1,2\\}$ allocate all the locations
$\ell_{1},\dots,\ell_{m^{\prime}}$ and in particular the “faulty” locations
associated with $y,y^{\prime},z,z^{\prime},u,u^{\prime}$. Intuitively, $a$
(resp. $b$) denote the number of variables in $\\{y,y^{\prime}\\}$ (resp.
$\\{z,z^{\prime}\\}$) that have been allocated. The rules for predicates
$B_{a,b}$ are meant to guarantee that the following conditions are satisfied
for variables $y$ and $y^{\prime}$ (similar constraints hold for $z$ and
$z^{\prime}$):

  * •

$y$ is allocated before $y^{\prime}$,

  * •

$y$ is allocated for a variable $p$ corresponding to the beginning of a word
$(p\in\mathtt{B}$),

  * •

when $y$ has been allocated, no variable $p\in\mathtt{B}$ can occur on the
right-hand side of a points-to atom until $y^{\prime}$ is allocated.

Several cases are distinguished depending on whether the locations associated
with $y$ and $z$ (resp. $y^{\prime}$ and $z^{\prime}$) are in the same heap
image of a location or not. Note that $u$ and $u^{\prime}$ are allocated in
the same rules as $y$ and $y^{\prime}$ respectively. The predicate $B$ also
tackles the case where $k\not=k^{\prime}$. This corresponds to the case where
the recursive calls end with $B_{1,2}$ or $B_{2,1}$ in the last rule below,
meaning that $(\dagger)$ holds for some $i$, with either $i=k$ and
$i<k^{\prime}$ or $i=k^{\prime}$ and $i<k$. For the sake of conciseness and
readability, we denote by $\mathbf{w}$ the vector of variables
$\mathbf{v},y,y^{\prime},z,z^{\prime},u,u^{\prime}$ in the rules below. We
also denote by $\phi^{\prime}(y,z,u)$ the formula
$P(y,\mathrm{\bot})*P(z,\mathrm{\bot})*P(u,\mathrm{\bot})$.

$B(x,\mathbf{w})$ | $\Leftarrow$ | $x\mapsto(\mathrm{\bot},\mathrm{\bot},\mathrm{\bot},\mathrm{\bot},\mathrm{\bot},x^{\prime})*B_{0,0}(x^{\prime},\mathbf{w})$
---|---|---
|  | $\qquad*S(y,z)*\overline{S}(u,z)*(\overline{S}(y^{\prime},z^{\prime})\vee S(u^{\prime},z^{\prime}))$
$B_{a,b}(x,\mathbf{w})$ | $\Leftarrow$ | $\exists x^{\prime},y^{\prime\prime},z^{\prime\prime},u^{\prime\prime}.x\mapsto(p,q,y^{\prime\prime},z^{\prime\prime},u^{\prime\prime},x^{\prime})*B_{a,b}(x^{\prime},\mathbf{w})*\phi^{\prime}(y^{\prime\prime},z^{\prime\prime},u^{\prime\prime})$
|  |  if ($a\not=1$ or $p\not\in\mathtt{B}$) and ($b\not=1$ or $q\not\in\mathtt{B}$)
$B_{0,0}(x,\mathbf{w})$ | $\Leftarrow$ | $\exists x^{\prime}.x\mapsto(p,q,y,z,u,x^{\prime})*B_{1,1}(x^{\prime},\mathbf{w})*\phi^{\prime}(y,z,u)$
|  |  if $p,q\in\mathtt{B}$
$B_{0,1}(x,\mathbf{w})$ | $\Leftarrow$ | $\exists x^{\prime}.x\mapsto(p,q,y,z^{\prime},u,x^{\prime})*B_{1,2}(x^{\prime},\mathbf{w})*\phi^{\prime}(y,z^{\prime},u)$
|  |  if $p,q\in\mathtt{B}$
$B_{1,0}(x,\mathbf{w})$ | $\Leftarrow$ | $\exists x^{\prime}.x\mapsto(p,q,y^{\prime},z,u^{\prime},x^{\prime})*B_{2,1}(x^{\prime},\mathbf{w})*\phi^{\prime}(y^{\prime},z,u^{\prime})$
|  |  if $p,q\in\mathtt{B}$
$B_{1,1}(x,\mathbf{w})$ | $\Leftarrow$ | $\exists x^{\prime}.x\mapsto(p,q,y^{\prime},z^{\prime},u^{\prime},x^{\prime})*B_{2,2}(x^{\prime},\mathbf{w})*\phi^{\prime}(y^{\prime},z^{\prime},u^{\prime})$
|  |  if $p,q\in\mathtt{B}$
$B_{0,b}(x,\mathbf{w})$ | $\Leftarrow$ | $\exists x^{\prime},z^{\prime\prime}.x\mapsto(p,q,y,z^{\prime\prime},u,x^{\prime})*B_{1,b}(x^{\prime},\mathbf{w})*\phi^{\prime}(y,z^{\prime\prime},u)$
|  |  if $p\in\mathtt{B}$ and ($b\not=1$ or $q\not\in\mathtt{B}$)
$B_{1,b}(x,\mathbf{w})$ | $\Leftarrow$ | $\exists x^{\prime},z^{\prime\prime}.x\mapsto(p,q,y^{\prime},z^{\prime\prime},u^{\prime},x^{\prime})*B_{2,b}(x^{\prime},\mathbf{w})*\phi^{\prime}(y^{\prime},z^{\prime\prime},u^{\prime})$
|  |  if $p\in\mathtt{B}$ and ($b\not=1$ or $q\not\in\mathtt{B}$)
$B_{a,0}(x,\mathbf{w})$ | $\Leftarrow$ | $\exists x^{\prime},y^{\prime\prime},u^{\prime\prime}.x\mapsto(p,q,y^{\prime\prime},z,u^{\prime\prime},x^{\prime})*B_{a,1}(x^{\prime},\mathbf{w})*\phi^{\prime}(y^{\prime\prime},z,u^{\prime\prime})$
|  |  if $q\in\mathtt{B}$ and ($a\not=1$ or $p\not\in\mathtt{B}$)
$B_{a,1}(x,\mathbf{w})$ | $\Leftarrow$ | $\exists x^{\prime},y^{\prime\prime},u^{\prime\prime}.x\mapsto(p,q,y^{\prime\prime},z^{\prime},u^{\prime\prime},x^{\prime})*B_{a,2}(x^{\prime},\mathbf{w})*\phi^{\prime}(y^{\prime\prime},z^{\prime},u^{\prime\prime})$
|  |  if $q\in\mathtt{B}$ and ($a\not=1$ or $p\not\in\mathtt{B}$)
$B_{a,b}(x,\mathbf{w})$ | $\Leftarrow$ | $\exists y^{\prime\prime},z^{\prime\prime},u^{\prime\prime}.x\mapsto(p,q,y^{\prime\prime},z^{\prime\prime},u^{\prime\prime},\mathrm{\bot})*\phi^{\prime}(y^{\prime\prime},z^{\prime\prime},u^{\prime\prime})$
|  |  if $(a,b)\in\\{(2,2),(2,1),(1,2)\\}$

A straightforward induction permits to verify that if the considered structure
does not satisfy the formula $A(x,\mathbf{v})\vee\exists
y,z,y^{\prime},z^{\prime},u,u^{\prime}.B(x,\mathbf{w})$ then necessarily
$k=k^{\prime}$ and for all $l\in\\{1,\dots,k\\}$, we have
$(\ell^{y}_{I_{l}},\ell^{z}_{J_{l}})\in{\mathfrak{S}}\wedge(\ell^{u}_{I_{l}},\ell^{z}_{J_{l}})\not\in{\mathfrak{S}}$.

There remains to check that $p_{I_{i}}=q_{J_{i}}$ for all
$i\in\\{1,\dots,k\\}$. To this aim, we design an atom $C(x,\mathbf{v})$ that
will be satisfied by structures not validating this condition, assuming the
condition $(\dagger)$ above is fulfilled. This predicate allocates the
location $\ell$ and introduces existential variables $y,z,u$ denoting the
faulty locations $\ell^{y}_{I_{i}},\ell^{z}_{J_{i}}$ and $\ell^{u}_{I_{i}}$,
i.e., the locations corresponding to the index $i$ such that
$p_{I_{i}}\not=q_{J_{i}}$. By $(\dagger)$, these locations must be chosen in
such a way that the constraints $S(y,z)$ and $\overline{S}(y,z)$ are
satisfied. The predicate $C(x,\mathbf{v})$ also guesses pairs $p,q$ such that
$p\not=q$ (denoting the distinct pairs $p_{x_{i}}$ and $q_{y_{i}}$) and
invokes the predicate $C_{p,q}^{(0,0)}$ to allocate all the remaining
locations. As for the previous rules, the predicates $C_{p,q}^{a,b}$, for
$p,q\in\mathtt{B}$ $a,b\in\\{0,1\\}$ allocate
$\ell_{1},\dots,\ell_{m^{\prime}}$, where $a$ (resp. $b$) denotes the number
of variables in $\\{y\\}$ (resp. $\\{z\\}$) that have already been allocated.
In the rules below, we denote by $\mathbf{u}$ the vector $\mathbf{v},y,z,u$.
In all the rules we have $p^{\prime},q^{\prime}\in\mathtt{P}$.

$C(x,\mathbf{v})$ | $\Leftarrow$ | $\exists y,z,u.~{}x\mapsto(\mathrm{\bot},\mathrm{\bot},\mathrm{\bot},\mathrm{\bot},\mathrm{\bot},x^{\prime})*C_{p,q}^{0,0}(x^{\prime},\mathbf{u})*S(y,z)*\overline{S}(u,z)$
---|---|---
|  |  if $p\not=q$ and $p,q\in\mathtt{B}$
$C_{p,q}^{a,b}(x,\mathbf{u})$ | $\Leftarrow$ | $\exists x^{\prime},y^{\prime\prime},z^{\prime\prime},u^{\prime\prime}.x\mapsto(p^{\prime},q^{\prime},y^{\prime\prime},z^{\prime\prime},u^{\prime\prime},x^{\prime})*C_{p,q}^{a,b}(x,\mathbf{u})$
|  | $\qquad*\ \phi^{\prime}(y^{\prime\prime},z^{\prime\prime},u^{\prime\prime})$
$C_{p,q}^{0,0}(x,\mathbf{u})$ | $\Leftarrow$ | $\exists x^{\prime}.x\mapsto(p,q,y,z,u,x^{\prime})*C_{p,q}^{1,1}(x,\mathbf{u})*\phi^{\prime}(y,z,u)$
$C_{p,q}^{0,b}(x,\mathbf{u})$ | $\Leftarrow$ | $\exists x^{\prime},z^{\prime\prime}.x\mapsto(p,q^{\prime},y,z^{\prime\prime},u,x^{\prime})*C_{p,q}^{1,b}(x,\mathbf{u})*\phi^{\prime}(y,z^{\prime\prime},u)$
$C_{p,q}^{a,0}(x,\mathbf{u})$ | $\Leftarrow$ | $\exists x^{\prime},y^{\prime\prime},u^{\prime\prime}.x\mapsto(p^{\prime},q,y^{\prime\prime},z,u^{\prime\prime},x^{\prime})*C_{p,q}^{a,1}(x,\mathbf{u})*\phi^{\prime}(y^{\prime\prime},z,u^{\prime\prime})$
$C_{p,q}^{1,1}(x,\mathbf{u})$ | $\Leftarrow$ | $\exists y^{\prime\prime},z^{\prime\prime},u^{\prime\prime}.x\mapsto(p^{\prime},q^{\prime},y^{\prime\prime},z^{\prime\prime},u^{\prime\prime},\mathrm{\bot})*\phi^{\prime}(y^{\prime\prime},z^{\prime\prime},u^{\prime\prime})$

The PCP has a solution iff the sequent

$W(x,\mathbf{v})\vdash_{{\cal R}}A(x,\mathbf{v}),\exists
y,z,y^{\prime},z^{\prime},u,u^{\prime}.B(x,\mathbf{w}),C(x,\mathbf{u})$

has a countermodel. Indeed, if a structure satisfying the atom
$W(x,\mathbf{v})$ but not the disjunction $A(x,\mathbf{v})\vee\exists
y,z,y^{\prime},z^{\prime},u,u^{\prime}.B(x,\mathbf{w})\vee C(x,\mathbf{u})$
exists, then as explained above, there exists a word
$u_{i_{1}}.\dots.u_{i_{k}}=v_{j_{1}}.\dots.v_{j_{k^{\prime}}}$, with
$(i_{1},\dots,i_{k})=(j_{1},\dots,j_{k^{\prime}})$. Conversely, if a solution
of the PCP exists, then by using the locations
$\alpha_{l},\alpha_{l}^{\prime},\alpha_{l}^{\prime\prime}$ in the hypothesis
of the lemma as $\ell^{y}_{I_{l}},\ell^{z}_{J_{l}},\ell^{u}_{I_{l}}$ it is
easy to construct a a structure satisfying $W(x,\mathbf{v})$. Further, by
hypothesis, since $(\alpha_{l},\alpha_{l}^{\prime})\in{\mathfrak{S}}$ and
$(\alpha_{l}^{\prime\prime},\alpha_{l}^{\prime})\not\in{\mathfrak{S}}$, we
have $(\ell^{y}_{I_{l}},\ell^{z}_{J_{l}})\in{\mathfrak{S}}$ and
$(\ell^{u}_{I_{l}},\ell^{z}_{J_{l}})\notin{\mathfrak{S}}$ for all
$l=1,\dots,k$. Thus $A(x,\mathbf{v})$ and $\exists
y,z,y^{\prime},z^{\prime},u,u^{\prime}.B(x,\mathbf{w})$ do not hold. To
fulfill $\neg C(x,\mathbf{u})$ we have to ensure that, for all
$i,j\in\\{1,\dots,k\\}$, we have
$(\ell^{y}_{I_{i}},\ell^{z}_{J_{j}})\in{\mathfrak{S}}\wedge(\ell^{u}_{I_{i}},\ell^{z}_{J_{j}})\not\in{\mathfrak{S}}\implies
p_{I_{i}}=q_{J_{i}}$. Since the considered word is a solution of the PCP, we
have $p_{I_{i}}=q_{J_{i}}$ for all $i=1,\dots,k$, hence $\neg C(x,\mathbf{u})$
is satisfied. ∎

##  4 Eliminating Equations and Disequations

In this section, we show that the equations and disequations can always be
eliminated from established sequents (in exponential time), while preserving
equivalence. The intuition is that the equations can be discarded by
instantiating the inductive rules, while the disequations can be replaced by
assertions that the considered variables are allocated in disjoint parts of
the heap.

We first introduce an additional restriction on pc-SIDs that is meant to
ensure that the set of free variables allocated by a predicate atom is the
same in every unfolding. The pc-SID satisfying this condition are called
$\mathit{alloc}$-compatible. We will show that every pc-SID can be reduced to
an equivalent $\mathit{alloc}$-compatible set. Let $\mathit{alloc}$ be a
function mapping each predicate symbol $p$ to a subset of
$\\{1,\dots,\\#(p)\\}$. For any disjunction-free formula $\phi$, we denote by
$\mathit{alloc}(\phi)$ the set of variables $x\in\mathit{fv}(\phi)$ such that
$\phi$ contains an atom of the form $x\mapsto(y_{1},\dots,y_{\kappa})$ or
$p(z_{1},\dots,z_{n})$, with $x=z_{i}$ for some $i\in\mathit{alloc}(p)$.

###### Definition 9

An established pc-SID ${\cal R}$ is $\mathit{alloc}$-compatible if for all
rules $\alpha\Leftarrow\phi$ in ${\cal R}$, we have
$\mathit{alloc}(\alpha)=\mathit{alloc}(\phi)$ . A sequent $\phi\vdash_{{\cal
R}}\Gamma$ is $\mathit{alloc}$-compatible if ${\cal R}$ is
$\mathit{alloc}$-compatible.

###### Lemma 1

There exists an algorithm which, for every sequent $\phi\vdash_{{\cal
R}}\Gamma$, computes an equivalent $\mathit{alloc}$-compatible sequent
$\phi^{\prime}\vdash_{{\cal R}^{\prime}}\Gamma^{\prime}$. Moreover, this
algorithm runs in exponential time and
$\mathit{width}(\phi^{\prime}\vdash_{{\cal
R}^{\prime}}\Gamma^{\prime})=\mathcal{O}(\mathit{width}(\phi\vdash_{{\cal
R}}\Gamma)^{2})$.

###### Proof

We associate all pairs $(p,A)$ where $p\in{\cal P}_{S}$ and
$A\subseteq\\{1,\dots,\\#(p)\\}$ with fresh, pairwise distinct predicate
symbols $p_{A}\in{\cal P}_{S}$, with the same arity as $p$, and we set
$\mathit{alloc}(p_{A})=A$. For each disjunction-free formula $\phi$, we denote
by $\phi^{*}$ the set of formulas obtained from $\phi$ by replacing every
predicate atom $p(\mathbf{x})$ by an atom $p_{A}(\mathbf{x})$ with
$A\subseteq\\{1,\dots,\\#(p)\\}$. Let ${\cal R}^{\prime}$ be the set of
$\mathit{alloc}$-compatible rules of the form
$p_{A}(\mathbf{x})\Leftarrow\psi$, where $p(\mathbf{x})\Leftarrow\phi$ is a
rule in ${\cal R}$ and $\psi\in\phi^{*}$. Note that the symbols $p_{A}$ may be
encoded by words of length $\mathcal{O}(\|p\|+\\#(p))$, thus for every
$\psi\in\phi^{*}$ we have
$\mathit{width}(\psi)=\mathcal{O}(\mathit{width}(\phi)^{2})$, hence
$\mathit{width}({\cal R}^{\prime})=\mathcal{O}(\mathit{width}({\cal R})^{2})$.
We show by induction on the satisfiability relation that the following
equivalence holds for every structure $(\mathfrak{s},\mathfrak{h})$:
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$ iff there exists
$\psi\in\phi^{*}$ such that $(\mathfrak{s},\mathfrak{h})\models_{{\cal
R}^{\prime}}\psi$. For the direct implication, we also prove that
$\mathit{alloc}(\psi)=\\{x\in\mathit{fv}(\phi)\mid\mathfrak{s}(x)\in\mathit{dom}(\mathfrak{h})\\}$.

  * •

The proof is immediate if $\phi$ is a ${\cal T}$-formula, since
$\phi^{*}=\\{\phi\\}$, and the truth value of $\phi$ does not depend on the
considered pc-SID. Also, by definition $\mathit{alloc}(\phi)=\emptyset$ and
all the models of $\phi$ have empty heaps.

  * •

If $\phi$ is of the form $x\mapsto(y_{1},\dots,y_{n})$, then
$\phi^{*}=\\{\phi\\}$ and the truth value of $\phi$ does not depend on the
considered pc-SID. Also, $\mathit{alloc}(\phi)=\\{x\\}$ and we have
$\mathit{dom}(\mathfrak{h})=\\{\mathfrak{s}(x)\\}$ for every model
$(\mathfrak{s},\mathfrak{h})$ of $\phi$.

  * •

Assume that $\phi=p(x_{1},\dots,x_{\\#(p)})$. If
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$ then there exists a
formula $\gamma$ such that $\phi\Leftarrow_{{\cal R}}\gamma$ and
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\gamma$. By the induction
hypothesis, there exists $\psi\in\gamma^{*}$ such that
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}^{\prime}}\psi$ and
$\mathit{alloc}(\psi)=\\{x\in\mathit{fv}(\gamma)\mid\mathfrak{s}(x)\in\mathit{dom}(\mathfrak{h})\\}$.
Let
$A=\\{i\in\\{1,\dots,\\#(p)\\}\mid\mathfrak{s}(x_{i})\in\mathit{dom}(\mathfrak{h})\\}$,
so that $\mathit{alloc}(\psi)=\\{x_{i}\mid i\in A\\}$. By construction
$p_{A}(x_{1},\dots,x_{n})\Leftarrow\psi$ is $\mathit{alloc}$-compatible, and
therefore $p_{A}(x_{1},\dots,x_{n})\Leftarrow_{{\cal R}^{\prime}}\psi$, which
entails that $(\mathfrak{s},\mathfrak{h})\models_{{\cal
R}^{\prime}}p_{A}(x_{1},\dots,x_{n})$. By definition of $A$,
$\mathit{alloc}(p_{A}(x_{1},\dots,x_{n}))=\\{x\in\mathit{fv}(\phi)\mid\mathfrak{s}(x)\in\mathit{dom}(\mathfrak{h})\\}$.

Conversely, assume that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\psi$
for some $\psi\in\phi^{*}$. Necessarily $\psi$ is of the form
$p_{A}(x_{1},\dots,x_{n})$ with $A\subseteq\\{1,\dots,\\#(p)\\}$. We have
$p_{A}(x_{1},\dots,x_{n})\Leftarrow_{{\cal R}^{\prime}}\psi^{\prime}$ and
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\psi^{\prime}$ for some formula
$\psi^{\prime}$. By definition of ${\cal R}^{\prime}$, we deduce that
$p(x_{1},\dots,x_{n})\Leftarrow_{{\cal R}}\gamma$, for some $\gamma$ such that
$\psi\in\gamma^{*}$. By the induction hypothesis,
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\gamma$, thus
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}p(x_{1},\dots,x_{\\#(p)})$.
Since $p(x_{1},\dots,x_{\\#(p)})=\phi$, we have the result.

  * •

Assume that $\phi=\phi_{1}*\phi_{2}$. If
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$ then there exist disjoint
heaps $\mathfrak{h}_{1},\mathfrak{h}_{2}$ such that
$(\mathfrak{s},\mathfrak{h}_{i})\models_{{\cal R}}\phi_{i}$, for all $i=1,2$
and $\mathfrak{h}=\mathfrak{h}_{1}\uplus\mathfrak{h}_{2}$. By the induction
hypothesis, this entails that there exist formulas $\psi_{i}\in\phi_{i}^{*}$
for $i=1,2$ such that $(\mathfrak{s},\mathfrak{h}_{i})\models_{{\cal
R}^{\prime}}\psi_{i}$ and
$\mathit{alloc}(\psi_{i})=\\{x\in\mathit{fv}(\phi_{i})\mid\mathfrak{s}(x)\in\mathit{dom}(\mathfrak{h}_{i})\\}$.
Let $\psi=\psi_{1}*\psi_{2}$. It is clear that
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}^{\prime}}\psi_{1}*\psi_{2}$ and
$\mathit{alloc}(\psi)=\mathit{alloc}(\psi_{1}*\psi_{2})=\mathit{alloc}(\psi_{1})\cup\mathit{alloc}(\psi_{2})=\\{x\in\mathit{fv}(\phi_{1})\cup\mathit{fv}(\phi_{2})\mid\mathfrak{s}(x)\in\mathit{dom}(\mathfrak{h})\\}=\\{x\in\mathit{fv}(\phi)\mid\mathfrak{s}(x)\in\mathit{dom}(\mathfrak{h})\\}$.
Since $\psi_{1}*\psi_{2}\in\phi^{*}$, we obtain the result.

Conversely, assume that there exists $\psi\in\phi^{*}$ such that
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}^{\prime}}\psi$. Then
$\psi=\psi_{1}*\psi_{2}$ with $\psi_{i}\in\phi_{i}^{*}$, and we have
$(\mathfrak{s},\mathfrak{h}_{i})\models_{{\cal R}^{\prime}}\psi_{i}$, for
$i=1,2$ with $\mathfrak{h}=\mathfrak{h}_{1}\uplus\mathfrak{h}_{2}$. Using the
induction hypothesis, we get that
$(\mathfrak{s},\mathfrak{h}_{i})\models_{{\cal R}}\phi_{i}$, hence
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$.

  * •

Assume that $\phi=\exists y.\gamma$. If
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$ then
$(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\gamma$, for some store
$\mathfrak{s}^{\prime}$ coinciding with $\mathfrak{s}$ on every variable
distinct from $y$. By the induction hypothesis, this entails that there exists
$\psi\in\gamma^{*}$ such that
$(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}^{\prime}}\psi$ and
$\mathit{alloc}(\psi)=\\{x\in\mathit{fv}(\gamma)\mid\mathfrak{s}^{\prime}(x)\in\mathit{dom}(\mathfrak{h})\\}$.
Then $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}^{\prime}}\exists y.\psi$,
and we have $\exists y.\psi\in\phi^{*}$. Furthermore, $\mathit{alloc}(\exists
y.\psi)=\mathit{alloc}(\psi)\setminus\\{y\\}=\\{x\in\mathit{fv}(\gamma)\setminus\\{y\\}\mid\mathfrak{s}^{\prime}(x)\in\mathit{dom}(\mathfrak{h})\\}=\\{x\in\mathit{fv}(\phi)\mid\mathfrak{s}(x)\in\mathit{dom}(\mathfrak{h})\\}$.

Conversely, assume that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\psi$,
with $\psi\in\phi^{*}$. Then $\psi$ is of the form $\exists y.\psi^{\prime}$,
with $\psi^{\prime}\in\gamma^{*}$, thus there exists a store
$\mathfrak{s}^{\prime}$, coinciding with $\mathfrak{s}$ on all variables other
than $y$ such that $(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal
R}}\psi^{\prime}$. By the induction hypothesis, this entails that
$(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\psi$, thus
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\exists y.\gamma$. Since
$\exists y.\gamma=\phi$, we have the result.

Let $\phi^{\prime},\Gamma^{\prime}$ be the sequence of formulas obtained from
$\phi,\Gamma$ by replacing every atom $\alpha$ by the disjunction of all the
formulas in $\alpha^{*}$. It is clear that
$\mathit{width}(\phi^{\prime}\vdash_{{\cal
R}^{\prime}}\Gamma^{\prime})\leq\mathit{width}(\phi\vdash_{{\cal
R}}\Gamma)^{2}$. By the previous result, $\phi^{\prime}\vdash_{{\cal
R}^{\prime}}\Gamma^{\prime}$ is equivalent to $\phi\vdash_{{\cal R}}\Gamma$,
hence $\phi^{\prime}\vdash_{{\cal R}^{\prime}}\Gamma^{\prime}$ fulfills all
the required properties. Also, since each predicate $p$ is associated with
$2^{\\#(p)}$ predicates $p_{A}$, it is clear that $\phi^{\prime}\vdash_{{\cal
R}^{\prime}}\Gamma^{\prime}$ can be computed in time
$\mathcal{O}(2^{\mathit{size}(\phi\vdash_{{\cal R}}\Gamma)})$. ∎

###### Definition 10

Let $P\subseteq{\cal P}_{\cal T}$. A formula $\phi$ is $P$-constrained if for
every formula $\psi$ such that $\phi\Leftarrow_{{\cal R}}\psi$, and for every
symbol $p\in{\cal P}_{\cal T}$ occurring in $\psi$, we have $p\in P$. A
sequent $\phi\vdash_{{\cal R}}\Gamma$ is $P$-constrained if all the formulas
in $\phi,\Gamma$ are $P$-constrained.

###### Theorem 4.1

Let $P\subseteq{\cal P}_{\cal T}$. There exists an algorithm that transforms
every $P$-constrained established sequent $\phi\vdash_{{\cal R}}\Gamma$ into
an equivalent $(P\setminus\\{\approx,\not\approx\\})$-constrained established
sequent $\phi^{\prime}\vdash_{{\cal R}^{\prime}}\Gamma^{\prime}$. This
algorithm runs in exponential time and
$\mathit{width}(\phi^{\prime}\vdash_{{\cal R}^{\prime}}\Gamma^{\prime})$ is
polynomial w.r.t. $\mathit{width}(\phi\vdash_{{\cal R}}\Gamma)$.

###### Proof

We consider a $P$-constrained established sequent $\phi\vdash_{{\cal
R}}\Gamma$. This sequent is transformed in several steps.

Step 1. The first step consists in transforming all the formulas in
$\phi,\Gamma$ into disjunctions of symbolic heaps. Then for every symbolic
heap $\gamma$ occurring in the obtained sequent, we add all the variables
freely occurring in $\phi$ or $\Gamma$ as parameters of every predicate symbol
occurring in unfoldings of $\gamma$ (their arities are updated accordingly,
and these variables are passed as parameters to each recursive call of a
predicate symbol). We obtain an equivalent sequent $\phi_{1}\vdash_{{\cal
R}_{1}}\Gamma_{1}$, and if
$v=\mathit{card}(\mathit{fv}(\phi)\cup\mathit{fv}(\Gamma))$ denotes the total
number of free variables occurring in $\phi,\Gamma$, then it is easy to check
(since the size of each of these variables is bounded by
$\mathit{width}(\phi\vdash_{{\cal R}}\Gamma)$) that
$\mathit{width}(\phi_{1}\vdash_{{\cal R}_{1}}\Gamma_{1})\leq
v\cdot\mathit{width}(\phi\vdash_{{\cal R}}\Gamma)^{2}$. By Definition 7, we
have $v\leq\mathit{width}(\phi\vdash_{{\cal R}}\Gamma)$, thus
$\mathit{width}(\phi_{1}\vdash_{{\cal
R}_{1}}\Gamma_{1})=\mathcal{O}(\mathit{width}(\phi\vdash_{{\cal
R}}\Gamma)^{3})$.

Step 2. All the equations involving an existential variable can be eliminated
in a straightforward way by replacing each formula of the form $\exists
x.(x\approx y*\phi)$ with $\phi\\{x\leftarrow y\\}$. We then replace every
formula $\exists\mathbf{y}.\phi$ with free variables $x_{1},\dots,x_{n}$ by
the disjunction of all the formulas of the form
$\exists\mathbf{z}.\phi\sigma*\scaleobj{1.5}{*}_{z\in\mathbf{z},z^{\prime}\in\mathbf{z}\cup\\{x_{1},\dots,x_{n}\\},z\not=z^{\prime}}z\not\approx
z^{\prime}$ , where $\sigma$ is a substitution such that
$\mathit{dom}(\sigma)\subseteq\mathbf{y}$,
$\mathbf{z}=\mathbf{y}\setminus\mathit{dom}(\sigma)$ and
$\mathit{img}(\sigma)\subseteq\mathbf{y}\cup\\{x_{1},\dots,x_{n}\\}$.
Similarly we replace every rule
$p(x_{1},\dots,x_{n})\Leftarrow\exists\mathbf{y}.\phi$ by the the set of rules
$p(x_{1},\dots,x_{n})\Leftarrow\exists\mathbf{z}.\phi\sigma*\scaleobj{1.5}{*}_{z\in\mathbf{z},z^{\prime}\in\mathbf{z}\cup\\{x_{1},\dots,x_{n}\\},z\not=z^{\prime}}z\not\approx
z^{\prime}$, where $\sigma$ is any substitution satisfying the conditions
above. Intuitively, this transformation ensures that all existential variables
are associated to pairwise distinct locations, also distinct from any location
associated to a free variable. The application of the substitution $\sigma$
captures all the rule instances for which this condition does not hold, by
mapping all variables that are associated with the same location to a unique
representative. We denote by $\phi_{2}\vdash_{{\cal R}_{2}}\Gamma_{2}$ the
sequent thus obtained. Let $v^{\prime}$ be the maximal number of existential
variables occurring in a rule in ${\cal R}$. We have
$v^{\prime}\leq\mathit{width}(\phi\vdash_{{\cal R}}\Gamma)$ (since the
transformation in Step $1$ adds no existential variable). Since at most one
disequation is added for every pair of variables, and since the size of every
variable is bounded by $\mathit{width}(\phi\vdash_{{\cal R}}\Gamma)$, it is
clear that $\mathit{width}(\phi_{2}\vdash_{{\cal
R}_{2}}\Gamma_{2})=\mathit{width}(\phi_{1}\vdash_{{\cal
R}_{1}}\Gamma_{1})+v^{\prime}\cdot(v+v^{\prime})\cdot(1+2*\mathit{width}(\phi\vdash_{{\cal
R}}\Gamma))=\mathcal{O}(\mathit{width}(\phi\vdash_{{\cal R}}\Gamma)^{3})$.

Step 3. We replace every atom $\alpha=p(x_{1},\dots,x_{n})$ occurring in
$\phi_{2},\Gamma_{2}$ or ${\cal R}_{2}$ with pairwise distinct variables
$x_{i_{1}},\dots,x_{i_{m}}$ (with $m\leq n$ and $i_{1}=1$), by an atom
$p_{\alpha}(x_{i_{1}},\dots,x_{i_{m}})$, where $p_{\alpha}$ is a fresh
predicate symbol, associated with rules of the form
$p_{\alpha}(y_{i_{1}},\dots,y_{i_{m}})\Leftarrow\psi\\{y_{i}\leftarrow
x_{i}\mid i\in\\{1,\dots,n\\}\\}\theta$, where
$p(y_{1},\dots,y_{n})\Leftarrow\psi$ is a rule in ${\cal R}$ and $\theta$
denotes the substitution $\\{x_{i_{k}}\leftarrow y_{i_{k}}\mid
i\in\\{1,\dots,m\\}\\}$. By construction,
$p_{\alpha}(x_{i_{1}},\dots,x_{i_{m}})$ is equivalent to $\alpha$. We denote
by $\phi_{3}\vdash_{{\cal R}_{3}}\Gamma_{3}$ the resulting sequent. It is
clear that $\phi_{3}\vdash_{{\cal R}_{3}}\Gamma_{3}$ is equivalent to
$\phi\vdash_{{\cal R}}\Gamma$.

By a straightforward induction on the derivation, we can show that all atoms
occurring in an unfolding of the formulas in the sequent
$\phi_{3}\vdash_{{\cal R}_{3}}\Gamma_{3}$ are of the form
$q(y_{1},\dots,y_{\\#(q)})$, where $y_{1},\dots,y_{\\#(q)}$ are pairwise
distinct, and that the considered unfolding also contains the disequation
$y_{i}\not\approx y_{j}$, for all $i\not=j$ such that either $y_{i}$ or
$y_{j}$ is an existential variable (note that if $y_{i}$ and $y_{j}$ are both
free then $y_{i}\not\approx y_{j}$ is valid, since the considered stores are
injective). This entails that the rules that introduce a trivial equality
$u\approx v$ with $u\not=v$ are actually redundant, since unfolding any atom
$q(y_{1},\dots,y_{\\#(q)})$ using such a rule yields a formula that is
unsatisfiable. Consequently such rules can be eliminated without affecting the
status of the sequent. All the remaining equations are of form $u\approx u$
hence can be replaced by $\mathtt{emp}$. We may thus assume that the sequent
$\phi_{3}\vdash_{{\cal R}_{3}}\Gamma_{3}$ contains no equality. Note that by
the above transformation all existential variables must be interpreted as
pairwise distinct locations in any interpretation, and also be distinct from
all free variables. It is easy to see that the fresh predicates $p_{\alpha}$
may be encoded by words of size at most $\mathit{width}(\phi\vdash_{{\cal
R}}\Gamma)$, thus $\mathit{width}(\phi_{3}\vdash_{{\cal
R}_{3}}\Gamma_{3})\leq\mathit{width}(\phi\vdash_{{\cal
R}}\Gamma)\cdot\mathit{width}(\phi_{2}\vdash_{{\cal
R}_{2}}\Gamma_{2})=\mathcal{O}(\mathit{width}(\phi\vdash_{{\cal
R}}\Gamma)^{4})$. By Lemma 1, we may assume that $\phi_{3}\vdash_{{\cal
R}_{3}}\Gamma_{3}$ is $\mathit{alloc}$-compatible (note that the
transformation given in the proof of Lemma 1 does not affect the disequations
occurring in the rules).

Step 4. We now ensure that all the locations that are referred to are
allocated. Consider a symbolic heap $\gamma$ occurring in
$\phi_{3},\Gamma_{3}$ and any ${\cal R}_{3}$-model
$(\mathfrak{s},\mathfrak{h})$ of $\gamma$, where $\mathfrak{s}$ is injective.
For the establishment condition to hold, the only unallocated locations in
$\mathfrak{h}$ of $\gamma$ must correspond to locations $\mathfrak{s}(x)$
where $x$ is a free variable. We assume the sequent contains a free variable
$u$ such that, for every tuple
$(\ell_{0},\dots,\ell_{\kappa})\in\mathfrak{h}$, we have
$\mathfrak{s}(u)=\ell_{\kappa}$. This does not entail any loss of generality,
since we can always add a fresh variable $u$ to the considered problem: after
Step $1$, $u$ is passed as a parameter to all predicate symbols, and we may
replace every points-to atom $z_{0}\mapsto(z_{1},\dots,z_{\kappa})$ occurring
in $\phi_{3}$, $\Gamma_{3}$ or ${\cal R}_{3}$, by
$z_{0}\mapsto(z_{1},\dots,z_{\kappa},u)$ (note that this increases the value
of $\kappa$ by $1$). It is clear that this ensures that $\mathfrak{h}$ and $u$
satisfy the above property. We also assume, w.l.o.g., that the sequent
contains at least one variable $u^{\prime}$ distinct from $u$. Note that,
since $\mathfrak{s}$ is injective, the tuple
$(\mathfrak{s}(u^{\prime}),\dots,\mathfrak{s}(u^{\prime}))$ cannot occur in
$\mathfrak{h}$, because its last component is distinct from $\mathfrak{s}(u)$.
We then denote by $\phi_{4}\vdash_{{\cal R}_{4}}\Gamma_{4}$ the sequent
obtained from $\phi_{3}\vdash_{{\cal R}_{3}}\Gamma_{3}$ by replacing every
symbolic heap $\gamma$ in $\phi_{3},\Gamma_{3}$ by
$\left(\scaleobj{1.5}{*}_{x\in(\mathit{fv}(\phi_{3})\cup\mathit{fv}(\Gamma_{3}))\setminus\mathit{alloc}(\gamma)}x\mapsto(u^{\prime},\dots,u^{\prime})\right)*\gamma$
It is straightforward to check that $(\mathfrak{s},\mathfrak{h})\models\gamma$
iff there exists an extension $\mathfrak{h}^{\prime}$ of $\mathfrak{h}$ such
that
$(\mathfrak{s},\mathfrak{h}^{\prime})\models\left(\scaleobj{1.5}{*}_{x\in(\mathit{fv}(\phi_{3})\cup\mathit{fv}(\Gamma_{3}))\setminus\mathit{alloc}(\gamma)}x\mapsto(u^{\prime},\dots,u^{\prime})\right)*\gamma$,
with
$\mathit{loc}(\mathfrak{h})=\mathit{loc}(\mathfrak{h}^{\prime})=\mathit{dom}(\mathfrak{h}^{\prime})$
and
$\mathfrak{h}^{\prime}(\ell)=(\mathfrak{s}(u^{\prime}),\dots,\mathfrak{s}(u^{\prime}))$
for all
$\ell\in\mathit{dom}(\mathfrak{h}^{\prime})\setminus\mathit{dom}(\mathfrak{h})$.
This entails that $\phi_{4}\vdash_{{\cal R}_{4}}\Gamma_{4}$ is valid if and
only if $\phi\vdash_{{\cal R}}\Gamma$ is valid.

Consider a formula $\gamma$ in $\phi_{4},\Gamma_{4}$ and some unfolding
$\gamma^{\prime}$ of $\gamma$. Thanks to the transformation in this step and
the establishment condition, if $\gamma^{\prime}$ contains a (free or
existential) variable $x$ then it also contains an atom
$x^{\prime}\mapsto\mathbf{y}$ and a separating conjunction of equations $\chi$
such that $\chi\models_{{\cal T}}x\approx x^{\prime}$. Since all equations
have been removed, $\chi=\mathtt{emp}$, thus $x=x^{\prime}$. Consequently, if
$\gamma^{\prime}$ contains a disequation $x_{1}\not\approx x_{2}$ with
$x_{1}\not=x_{2}$, then it also contains atoms $x_{1}\mapsto\mathbf{y}_{1}$
and $x_{2}\mapsto\mathbf{y}_{2}$. This entails that the disequation
$x_{1}\not\approx x_{2}$ is redundant, since it is a logical consequence of
$x_{1}\mapsto\mathbf{y}_{1}*x_{2}\mapsto\mathbf{y}_{2}$. We deduce that the
satisfiability status of $\phi_{4}\vdash_{{\cal R}_{4}}\Gamma_{4}$ is
preserved if all disequations are replaced by $\mathtt{emp}$. ∎

###### Example 1

We illustrate all of the steps in the proof above.

Step 1.

Consider the sequent $p(x_{1},x_{2})\vdash_{{\cal R}}r(x_{1})*r(x_{2})$, where
${\cal R}$ is defined as follows: ${\cal R}=\left\\{r(x)\Leftarrow
x\mapsto(x)\right\\}$. After Step 1 we obtain the sequent
$p(x_{1},x_{2})\vdash_{{\cal
R}_{1}}r^{\prime}(x_{1},x_{2})*r^{\prime}(x_{2},x_{1})$, where ${\cal
R}_{1}=\left\\{r^{\prime}(x,y)\Leftarrow x\mapsto(x)\right\\}$.

Step 2.

This step transforms the formula $\exists y_{1}\exists
y_{2}.\,p(x,y_{1})*p(x,y_{2})$ into the disjunction:

$\begin{array}[]{rl}\exists
y_{1},y_{2}.\,p(x,y_{1})*p(x,y_{2})*y_{1}\not\approx y_{2}*y_{1}\not\approx
x*y_{2}\not\approx x&\vee\\\ \exists
y_{2}.\,p(x,x)*p(x,y_{2})*y_{2}\not\approx x&\vee\\\ \exists
y_{1}.\,p(x,y_{1})*p(x,x)*y_{1}\not\approx x&\vee\\\ p(x,x)*p(x,x)\end{array}$

Similarly, the rule $p(x)\leftarrow\exists z\exists u.~{}x\mapsto(z)*q(z,u)$
is transformed into the set:

$\begin{array}[]{lll}p(x)&\leftarrow&x\mapsto(x)*q(x,x)\\\
p(x)&\leftarrow&\exists z.~{}x\mapsto(z)*q(z,x)*z\not\approx x\\\
p(x)&\leftarrow&\exists u.~{}x\mapsto(x)*q(x,u)*u\not\approx x\\\
p(x)&\leftarrow&\exists z\exists u.~{}x\mapsto(z)*q(z,u)*z\not\approx
x*u\not\approx x*z\not\approx u\\\ \end{array}$

Step 3.

Assume that ${\cal R}$ contains the rules $p(y_{1},y_{2},y_{3})\Leftarrow
y_{1}\mapsto(y_{2})*q(y_{2},y_{3})*y_{1}\approx y_{3}$ and
$p(y_{1},y_{2},y_{3})\Leftarrow
y_{1}\mapsto(y_{2})*r(y_{2},y_{3})*y_{1}\approx y_{2}$ and consider the
sequent $p(x,y,x)\vdash_{{\cal R}}\mathtt{emp}$. Step 3 generates the sequent
$p_{\alpha}(x,y)\vdash_{{\cal R}^{\prime}}\mathtt{emp}$ (with
$\alpha=p(x,y,x)$) where ${\cal R}^{\prime}$ contains the rules
$p_{\alpha}(y_{1},y_{2})\Leftarrow
y_{1}\mapsto(y_{2})*q(y_{2},y_{1})*y_{1}\approx y_{1}$ and
$p_{\alpha}(y_{1},y_{2})\Leftarrow
y_{1}\mapsto(y_{2})*r(y_{2},y_{1})*y_{1}\approx y_{2}$. The second rule is
redundant, because $p_{\alpha}(y_{1},y_{2})$ is used only in a context where
$y_{1}\not\approx y_{2}$ holds.

Step 4.

Let
$\gamma=p(x,y,z,z^{\prime})*q(x,y,z,z^{\prime})*z^{\prime}\mapsto(z^{\prime})$,
assume $\mathit{alloc}(\gamma)=\left\\{x,z\right\\}$, and consider the sequent
$\gamma\vdash_{{\cal R}}\mathtt{emp}$. Then $\gamma$ is replaced by
$p(x,y,z,z^{\prime},u)*q(x,y,z,z^{\prime},u)*z^{\prime}\mapsto(z^{\prime},u)*u\mapsto(x,x)*y\mapsto(x,x)$
(all non-allocated variables are associated with $(x,x)$, where $x$ plays the
rôle of the variable $u^{\prime}$ in Step $4$ above). Also, every points-to
atom $z_{0}\mapsto(z_{1})$ in ${\cal R}$ is replaced by
$z_{0}\mapsto(z_{1},u)$.

##  5 Discussion

The presented undecidability result is very tight. Theorem 3.1 applies to most
theories and the proof only uses very simple data structures (namely simply
linked lists). The proof of Theorem 3.1 could be adapted (at the cost of
cluttering the presentation) to handle quantifier-free entailments and even
simpler inductive systems with at most one predicate atom on the right-hand
side of each rule, in the spirit of word automata.

Our logic has only one sort of variables, denoting locations, thus one cannot
directly describe structures in which the heap maps locations to tuples
containing both locations and data, ranging over disjoint domains. This is
actually not restrictive: indeed, data can be easily encoded in our framework
by considering a non-injective function $\mathtt{d}(x)$ mapping locations to
data, and adding theory predicates constructed on this function, such as
$\mathtt{d}(x)\approx\mathtt{d}(y)$ to state that two (possibly distinct)
locations $x,y$ are mapped to the same element. The obtained theory falls
within the scope of Theorem 3.1 (using $\mathtt{d}(x)\approx\mathtt{d}(y)$ as
the relation $S(x,y)$), provided the domain of the data is infinite. This
shows that entailments with data disjoint from locations are undecidable, even
if the theory only contains equations and disequations, except when the data
domain is finite.

### Acknowledgments.

This work has been partially funded by the the French National Research Agency
(ANR-21-CE48-0011). The authors wish to thank Radu Iosif for his comments on
an earlier version of the paper and for fruitful discussions.

## References

  * [1] J. Berdine, C. Calcagno, and P. W. O’Hearn.  A decidable fragment of separation logic.  In Proc. of FSTTCS’04, volume 3328 of LNCS. Springer, 2004\.
  * [2] Cristiano Calcagno, Hongseok Yang, and Peter W O’hearn.  Computability and complexity results for a spatial assertion language for data structures.  In FST TCS 2001, Proceedings, pages 108–119. Springer, 2001.
  * [3] B. Cook, C. Haase, J. Ouaknine, M. J. Parkinson, and J. Worrell.  Tractable reasoning in a fragment of separation logic.  In Proc. of CONCUR’11, volume 6901 of LNCS. Springer, 2011\.
  * [4] Stéphane Demri, Didier Galmiche, Dominique Larchey-Wendling, and Daniel Méry.  Separation logic with one quantified variable.  In CSR’14, volume 8476 of LNCS, pages 125–138. Springer, 2014.
  * [5] Mnacho Echenim, Radu Iosif, and Nicolas Peltier.  Entailment checking in separation logic with inductive definitions is 2-exptime hard.  In LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020, volume 73 of EPiC Series in Computing, pages 191–211. EasyChair, 2020.
  * [6] Mnacho Echenim, Radu Iosif, and Nicolas Peltier.  Decidable entailments in separation logic with inductive definitions: Beyond establishment.  In CSL 2021: 29th International Conference on Computer Science Logic, EPiC Series in Computing. EasyChair, 2021.
  * [7] Constantin Enea, Ondrej Lengál, Mihaela Sighireanu, and Tomás Vojnar.  Compositional entailment checking for a fragment of separation logic.  Formal Methods Syst. Des., 51(3):575–607, 2017.
  * [8] Constantin Enea, Mihaela Sighireanu, and Zhilin Wu.  On automated lemma generation for separation logic with inductive definitions.  In ATVA 2015, Proceedings, pages 80–96, 2015.
  * [9] Radu Iosif, Adam Rogalewicz, and Jiri Simacek.  The tree width of separation logic with recursive definitions.  In Proc. of CADE-24, volume 7898 of LNCS, 2013.
  * [10] Radu Iosif, Adam Rogalewicz, and Tomás Vojnar.  Deciding entailments in inductive separation logic with tree automata.  In Franck Cassez and Jean-François Raskin, editors, ATVA 2014, Proceedings, volume 8837 of LNCS, pages 201–218. Springer, 2014.
  * [11] Samin S Ishtiaq and Peter W O’Hearn.  Bi as an assertion language for mutable data structures.  In ACM SIGPLAN Notices, volume 36, pages 14–26, 2001.
  * [12] Quang Loc Le.  Compositional satisfiability solving in separation logic.  In Fritz Henglein, Sharon Shoham, and Yakir Vizel, editors, Verification, Model Checking, and Abstract Interpretation - 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17-19, 2021, Proceedings, volume 12597 of Lecture Notes in Computer Science, pages 578–602. Springer, 2021.
  * [13] Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang.  Local reasoning about programs that alter data structures.  In Laurent Fribourg, editor, Computer Science Logic, 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL, Paris, France, September 10-13, 2001, Proceedings, volume 2142 of LNCS, pages 1–19. Springer, 2001.
  * [14] Jens Pagel, Christoph Matheja, and Florian Zuleger.  Complete entailment checking for separation logic with inductive definitions, 2020.  arXiv:2002.01202.
  * [15] Juan Antonio Navarro Pérez and Andrey Rybalchenko.  Separation logic modulo theories.  In Chung-chieh Shan, editor, Programming Languages and Systems \- 11th Asian Symposium, APLAS 2013, Melbourne, VIC, Australia, December 9-11, 2013. Proceedings, volume 8301 of LNCS, pages 90–106. Springer, 2013\.
  * [16] Ruzica Piskac, Thomas Wies, and Damien Zufferey.  Automating separation logic using SMT.  In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of LNCS, pages 773–789. Springer, 2013.
  * [17] Xiaokang Qiu, Pranav Garg, Andrei Stefanescu, and Parthasarathy Madhusudan.  Natural proofs for structure, data, and separation.  In Hans-Juergen Boehm and Cormac Flanagan, editors, ACM SIGPLAN PLDI ’13, pages 231–242. ACM, 2013.
  * [18] J.C. Reynolds.  Separation Logic: A Logic for Shared Mutable Data Structures.  In Proc. of LICS’02, 2002.
  * [19] Zhaowei Xu, Taolue Chen, and Zhilin Wu.  Satisfiability of compositional separation logic with tree predicates and data constraints.  In Leonardo de Moura, editor, CADE 26, volume 10395 of LNCS, pages 509–527. Springer, 2017.


# Rough Approximate Subgroups

Arturo Rodríguez Fanlo and Frank O. Wagner  Hebrew University of Jerusalem,
Israel  Université Lyon 1; CNRS; Institut Camille Jordan UMR 5208, 21 avenue
Claude Bernard, 69622 Villeurbanne-cedex, France<EMAIL_ADDRESS><EMAIL_ADDRESS>
(Date: 27th August 2024)

###### Abstract.

Given a $T$-rough definably amenable $T$-rough approximate subgroup $A$ of a
group in some first-order structure, there is a type-definable subgroup $H$
normalised by $A$ and contained in $A^{4}$ of bounded index in $\langle
A\rangle$.

###### Key words and phrases:

rough approximate subgroup, rough definable amenability, Lie model

###### 2010 Mathematics Subject Classification:

03C98, 11P70, 20A15

First author supported by the Israel Academy of Sciences and Humanities &
Council for Higher Education Excellence Fellowship Program for International
Postdoctoral Researchers.

Second author supported by GeoMod (ANR-DFG AAPG2019)

## Introduction

In [2, Theorem 4.2], Hrushovski found a fundamental connexion between
approximate subgroups and Lie groups. This result, now known as the Lie Model
Theorem, was the starting point used to finally give a complete classification
of finite approximate subgroups by Breuillard, Green and Tao [1].

The proof of [2, Theorem 4.2] first shows that, for any definable approximate
subgroup $A$, under a certain definable amenability condition, there is a
type-definable normal subgroup $S$ of bounded index of $\langle A\rangle$
contained in $A^{4}$. For this first fundamental step, Hrushovski proves a
general Stabilizer Theorem [2, Theorem 3.5], working with an $S_{1}$ ideal of
definable sets which, in addition, is invariant under translations and
automorphisms. Then, in [2, Theorem 4.2], this general Stabilizer Theorem is
applied for the $S_{1}$ ideal of sets of measure zero. However, in order for
this ideal to become invariant under automorphism, one needs to work with an
expansion of the starting language.

In a joint work with Massicot, the second named author provided in [4] an
alternative proof of Hrushovski’s Lie Model Theorem avoiding any expansion of
the language. While Hrushovski’s original proof only uses the ideal of measure
zero subsets, the argument in [4] fundamentally exploits the additivity of the
measure.

In [5], the first named author adapted [2, Theorem 3.5] and[2, Theorem 4.2]
for hyperdefinable sets, providing in particular a generalisation of the Lie
Model Theorem for rough approximate subgroups. This result was later used in
[3] for the particular case of metric groups. The argument in [5] uses again a
general version of the Stabilizer Theorem (now for hyperdefinable sets), and
so the applications in [3] require again to work with an expansion of the
starting language.

The aim of this paper is to adapt the alternative technique provided in [4]
for the case studied in [3]. This is not a straightforward task — while the
ideal used for the original Lie Model Theorem is directly given by a measure,
the ideal in [3] is not associated with a measure at all. Instead, the ideal
in [3] is built as the inf-limit of the zero ideals of a sequence of
subadditive set functions. Hence, in [3], we lack of the additivity property
that is fundamentally used in [4]. Fortunately, a careful analysis of the
properties of these subadditive set functions shows that, although they are
not completely additive, they still keep some rough additivity that could be
exploited.

Notations: Through this paper, fix a many sorted first order language
$\mathtt{L}$, a $\kappa$-saturated $\mathtt{L}$-structure $\mathfrak{M}$ with
$\kappa\geq|\mathtt{L}|$, a definable group $G$ and a definable symmetric
subset $A$ of $G$. We always use product notation and, unless otherwise
stated, we consider the group acting on itself on the left. A subset $X$ of
$G$ is called symmetric if $1\in X=X^{-1}$. For subsets $X$ and $Y$ of $G$, we
write $XY$ for the set of pairwise products and call it the $Y$-thickening of
$X$. For $n\in\mathbb{N}$, abbreviate $X^{n}\coloneqq XX^{n-1}$ and
$X^{-n}\coloneqq(X^{-1})^{n}$. We say that $X$ normalises $Y$ if
$x^{-1}Yx\subseteq Y$ for every $x\in X$.

##  1\. Rough Measures

Through this section, let $T\subseteq G$ be a symmetric subset and
$\mathcal{A}$ a boolean algebra of definable subsets of $G$ containing $A$ and
closed under $T$-thickenings.

######  Definition 1.

A _$T$ -rough measure_ on $\mathcal{A}$ is an increasing subadditive set
function $\mu:\,\mathcal{A}\to\mathbb{R}_{\geq 0}\cup\\{\infty\\}$ which is
additive modulo $T$, i.e. for $X,Y\in\mathcal{A}$ with $Y\cap ZT=\emptyset$ we
have $\mu(Y\cup Z)=\mu(Y)+\mu(Z)$. For a type-definable set $Y$ we put
$\mu(Y)\coloneqq\inf\\{\mu(\bar{Y})\mathrel{:}\bar{Y}\supseteq Y\mathrm{\
definable}\\}$. We say that $\mu$ is _normalised_ at $A$ if $\mu(A)=1$.

######  Lemma 2.

Let $\mu$ be a $T$-rough measure on $\mathcal{A}$. Then, for any
$S_{0},\ldots,S_{n-1}\in\mathcal{A}$, we have

$\mu\left(\textstyle{\bigcup_{i<n}}S_{i}\right)\geq\sum_{i<n}\mu(S_{i})-\sum_{\mathclap{i<j<n}}\min\\{\mu(S_{i}\cap
S_{j}T),\mu(S_{i}T\cap S_{j})\\}.$

###### Proof.

For $n<2$, there is nothing to prove. For $n=2$, by subadditivity,

$\mu(S_{0})\leq\mu(S_{0}\setminus S_{1}T)+\mu(S_{0}\cap S_{1}T).$

Hence, by additivity modulo $T$, we get

$\displaystyle\mu(S_{0}\cup S_{1})$ $\displaystyle\geq\mu((S_{0}\setminus
S_{1}T)\cup S_{1})=\mu(S_{0}\setminus S_{1}T)+\mu(S_{1})$
$\displaystyle\geq\mu(S_{0})+\mu(S_{1})-\mu(S_{0}\cap S_{1}T).$

By symmetry, $\mu(S_{0}\cup S_{1})\geq\mu(S_{0})+\mu(S_{1})-\mu(S_{0}T\cap
S_{1})$, and the result follows.

Suppose the assertion is true for $n$, and consider
$S_{0},\ldots,S_{n}\in\mathcal{A}$. Put

$I=\\{i<n\mathrel{:}\mu(S_{i}\cap S_{n}T)\leq\mu(S_{i}T\cap S_{n})\\},$

and set $X=\bigcup_{i\in I}S_{i}$ and $X^{\prime}=\bigcup_{i\in n\setminus
I}S_{i}$. Suppose $x\in X^{\prime}\cap(S_{n}\setminus X^{\prime}T)T$; say
$x=yt$ with $y\in S_{n}\setminus X^{\prime}T$ and $t\in T$. Then,
$y=xt^{-1}\in X^{\prime}T$, a contradiction. Therefore, $(X\cup
X^{\prime})\cap(S_{n}\setminus X^{\prime}T)T\subseteq X\cap S_{n}T$. Thus,

$\displaystyle\mu\left(\textstyle{\bigcup_{i\leq n}}S_{i}\right)$
$\displaystyle\geq\mu(X\cup X^{\prime}\cup(S_{n}\setminus X^{\prime}T))$
$\displaystyle\geq\mu(X\cup X^{\prime})+\mu(S_{n}\setminus
X^{\prime}T)-\mu((X\cup X^{\prime})\cap(S_{n}\setminus X^{\prime}T)T)$
$\displaystyle\geq\mu(X\cup X^{\prime})+\mu(S_{n})-\mu(S_{n}\cap
X^{\prime}T)-\mu(X\cap S_{n}T)$ $\displaystyle\geq\sum_{i\leq
n}\mu(S_{i})-\sum_{\mathclap{i<j<n}}\min\\{\mu(S_{i}\cap
S_{j}T),\mu(S_{i}T\cap S_{j})\\}$
$\displaystyle\phantom{\geq}-\sum_{\mathclap{i\in n\setminus I}}\mu(S_{i}T\cap
S_{n})-\sum_{i\in I}\mu(S_{i}\cap S_{n}T)$ $\displaystyle=\sum_{i\leq
n}\mu(S_{i})-\sum_{\mathclap{i<j\leq n}}\min\\{\mu(S_{i}\cap
S_{j}T),\mu(S_{i}T\cap S_{j})\\}.$

∎

######  Remark 3.

The above lemma also holds for type-definable sets, i.e. bounded intersections
of definable sets in $\mathcal{A}$, by taking limits.

######  Definition 4.

Let $X$ be definable subset of $G$. A definable subset $Y$ of $G$ is _$t$
-thick in $X$_ if, for any $t+1$ elements $g_{0},\ldots,g_{t}$ of $X$, there
are $0\leq i\neq j\leq t$ such that $g_{i}^{-1}g_{j}\in Y$. A type-definable
subset of $G$ is _thick in $X$_ if every definable superset is $t$-thick in
$X$ for some $t\in\mathbb{N}$.

Note that, if $Y$ is $t$-thick in $X$, then $t$ left translates of $Y$ cover
$X$. Conversely, if $t$ left translates of $Y$ cover $X$, then $Y^{-1}Y$ is
$t$-thick in $X$.

######  Lemma 5.

Let $X$ be a definable subset of $G$. A finite intersection of subsets of $G$
which are $t$-thick in $X$ is $t^{\prime}$-thick in $X$, for some
$t^{\prime}\in\mathbb{N}$. An intersection of subsets thick in $X$ is still
thick in $X$.

###### Proof.

By Ramsey’s Theorem. ∎

######  Lemma 6.

Let $\mu$ be a $T$-rough measure on $\mathcal{A}$ normalised at $A$. Suppose
that $0<\mu(A^{2m})<\infty$. Let $t>0$ be an integer and $B\subseteq A^{m}$
definable with $\mu(B)\geq 2\mu(A^{2m})/t$. Put

$S(B)=\left\\{g\in A^{2m}\mathrel{:}\min\\{\mu(B\cap gBT),\mu(gB\cap
BT)\\}\geq\frac{2\mu(A^{2m})}{t^{2}}\right\\}.$

Then, $S(B)$ is $t$-thick in $A^{m}$.

Note that any $g\in G$ with $B\cap gBT$ or $gB\cap BT$ non-empty must be in
$BTB^{-1}$. In particular, $S(B)\subseteq BTB^{-1}$.

###### Proof.

Suppose, aiming a contradiction, that the conclusion is false, and consider a
counter-example $(g_{i}\mathrel{:}i\leq t)$. Then, there is $\delta>0$ such
that

$\min\\{\mu(g_{i}B\cap g_{j}BT),\mu(g_{i}BT\cap
g_{j}B)\\}\leq\frac{2\mu(A^{2m})}{t^{2}}-\delta,$

for all $0\leq i<j\leq t$. By Lemma 2,

$\displaystyle\mu(A^{2m})$
$\displaystyle\geq\mu\Big{(}\textstyle{\bigcup_{i\leq t}}\,g_{i}B\Big{)}$
$\displaystyle\geq\sum_{i\leq t}\mu(g_{i}B)-\sum_{\mathclap{0\leq i<j\leq
t}}\min\\{\mu(g_{i}B\cap g_{j}BT),\mu(g_{i}BT\cap g_{j}B)\\}$
$\displaystyle\geq(t+1)\cdot\frac{2\mu(A^{2m})}{t}-\frac{(t+1)t}{2}\cdot\left(\frac{2\mu(A^{2m})}{t^{2}}-\delta\right)$
$\displaystyle=\mu(A^{2m})\cdot\frac{t+1}{t}+\frac{(t+1)t}{2}\delta>\mu(A^{2m}),$

a contradiction. ∎

##  2\. Rough Definable Amenability

Through this section, let $\mathfrak{u}$ be a non-principal ultrafilter on
$\mathbb{N}$ and $T=(T_{i}\mathrel{:}i\in\mathbb{N})$ a sequence of definable
subsets of $G$ such that, for each $i\in\mathbb{N}$, $T_{i}$ is symmetric,
$T_{i+1}^{2}\subseteq T_{i}$ and $T_{i+1}^{A}\subseteq T_{i}$. Write
$T_{\infty}=\bigcap_{i\in\mathbb{N}}T_{i}$; note that $T_{\infty}$ is a type-
definable subgroup of $G$ normalised by $A$.

######  Definition 7.

We say that $A$ is _$T$ -rough definably amenable_ if for all $i\in\mathbb{N}$
there is $T_{i}$-rough measure $\mu_{i}$ invariant under left translations on
the boolean algebra of definable subsets of $G$ which is normalised at $A$.

######  Remark 8.

We do not really need $\mu_{i}$ to be defined on all definable subsets of $G$,
but just on a certain boolean subalgebra $\mathcal{A}$ closed under left
translation by elements of $G$ and $T_{i}$-thickenings for $i\in\mathbb{N}$.

######  Lemma 9.

Let $P$ be a partially ordered set and
$f_{0},\ldots,f_{r-1}:\,P\rightarrow\mathbb{R}_{>0}$ be monotonous increasing
functions. Suppose there are $a,b\in\mathbb{R}_{>0}$ such that $a\leq
f_{i}(x)\leq b$ for all $x\in P$. Then, for any
$\varepsilon_{0},\ldots,\varepsilon_{r-1}\in\mathbb{R}_{>0}$, there is $x\in
P$ such that, for any $y\in P$ with $y<x$, $f_{i}(y)>(1-\varepsilon_{i})\cdot
f_{i}(x)$.

###### Proof.

Aiming a contradiction, suppose otherwise. Then, we can recursively construct
a decreasing sequence $(x_{n})_{n\in\mathbb{N}}$ in $P$ such that, for any
$n\in\mathbb{N}$, there is $i<r$ with $f_{i}(x_{m})\leq
f_{i}(x_{n+1})\leq(1-\varepsilon_{i})\cdot f_{i}(x_{n})$ for all
$m\in\mathbb{N}$ with $m>n$. Since $r\in\mathbb{N}$ is finite, there is $i<r$
and $N\subseteq\mathbb{N}$ infinite such that
$f_{i}(x_{m})\leq(1-\varepsilon_{i})\cdot f_{i}(x_{n})$ for any $n,m\in N$
with $m>n$. Thus, for any $n\in N$, $a\leq
f_{i}(x_{n})\leq(1-\varepsilon_{i})^{\alpha}\cdot
f_{i}(x_{n})\leq(1-\varepsilon_{i})^{\alpha}b$ with $\alpha\coloneqq|\\{m\in
N\mathrel{:}m<n\\}|$, getting a contradiction when
$\alpha>\ln(a/b)/\ln(1-\varepsilon_{i})$. ∎

######  Proposition 10.

Let $A\subseteq G$ be $T$-rough definably amenable, and $m$, $r$,
$(K_{i}\mathrel{:}i\in\mathbb{N})$ be integers with $\mu_{i}(A^{2m+r})\leq
K_{i}$. Suppose $B\subseteq A^{m}$ is type-definable and thick in $A$. Then,
there is a type-definable subset $S\subseteq B^{2}\subseteq A^{2m}$ thick in
$A^{m}$ such that $S^{r}\subseteq B^{4}T_{\infty}$.

###### Proof.

For $i,t,n\in\mathbb{N}$, define recursively the following families
$\mathscr{T}^{t}_{i,n}$ of definable subsets of $A^{m}$. For $n=0$,
$X\in\mathscr{T}^{t}_{i,0}$ if $X\neq\emptyset$. Given $\mathscr{T}^{t}_{i,n}$
for all $i,t\in\mathbb{N}$, set $X\in\mathscr{T}^{t}_{i,n+1}$ if

$S^{t}_{i,n}(X)\coloneqq\left\\{g\in A^{2m}\mathrel{:}X\cap gXT_{i},X\cap
g^{-1}XT_{i}\in\mathscr{T}^{t^{2}}_{i,n}\right\\}$

is $t$-thick in $A^{m}$.

These families are clearly definable, i.e.
$\\{b\mathrel{:}X(b)\in\mathscr{T}^{t}_{i,n}\\}$ is definable for any
definable family $X(b)$ of subsets of $A^{m}$. Also, we easily see by
induction that $Y\in\mathscr{T}^{t}_{i,n}$ implies $X\in\mathscr{T}^{s}_{i,h}$
and $S^{t}_{i,n}(Y)\subseteq S^{s}_{i,h}(X)$ whenever $n\geq h$, $t\leq s$ and
$Y\subseteq X$. On the other hand, by Lemma 6, we see that any definable
subset $X\subseteq A^{m}$ with $\mu(X)\geq 2K_{i}/t$ satisfies
$X\in\mathscr{T}^{t}_{i,n}$ for all $n\in\mathbb{N}$.

Pick a sequence of definable subsets $(B_{i}\mathrel{:}i\in\mathbb{N})$ such
that $B=\bigcap_{i\in\mathbb{N}}B_{i}$, $B_{i+1}\subseteq B_{i}$ for all
$i\in\mathbb{N}$ and $B_{0}\subseteq A^{m}$. Since finitely many translates of
$B_{i}$ cover $A$, we have $\mu_{i}(B_{i})>0$. Set $t_{i,n}\coloneqq\lceil
2K_{i}/\mu_{i}(B_{i})\rceil^{2^{n}}$, so $B_{i}\in\mathscr{T}^{t_{i,0}}_{i,n}$
for all $i,n\in\mathbb{N}$. Set $\varepsilon_{i}=\mu_{i}(B_{i})/2rK_{i}$.

Now, we define recursively sequences $(X_{i,n}\mathrel{:}i,n\in\mathbb{N})$
and $(S_{n}\mathrel{:}n\in\mathbb{N})$ such that $X_{i,n+1}\subseteq X_{i,n}$,
$S_{n+1}\subseteq S_{n}$, $S_{n}$ is thick in $A^{m}$ and
$X_{i,n}\in\mathscr{T}^{t_{i,n}}_{i,h}$ for any $h\in\mathbb{N}$.

For $n=0$, set $X_{0}=(B_{i})_{i\in\mathbb{N}}$. Given
$X_{n}=(X_{i,n}\mathrel{:}i\in\mathbb{N})$, set
$S_{n}=\bigcap_{i,h\in\mathbb{N}}S^{t_{i,n}}_{i,h}(X_{i,n})$; since
$X_{i,n}\in\mathscr{T}^{t_{i,n}}_{i,h}$ for every $h\in\mathbb{N}$, it follows
that $S_{n}$ is thick in $A^{m}$. Given $X_{n}=(X_{i,n})_{i\in\mathbb{N}}$ and
$S_{n}$, we take $X_{i,n+1}=X_{i,n}\cap gX_{i,n}T_{i}$ where $g\in S_{n}$
satisfies for some $k<r$ that

$\mu_{i}(X_{i,n+1}T_{i}^{k}B_{i}T_{i}^{k}\cap
A^{2m+r})\leq(1-\varepsilon_{i})\mu_{i}(X_{i,n}T_{i}^{k}B_{i}T_{i}^{k}\cap
A^{2m+r}),$

or, if there is no such $g\in S_{n}$, we take $X_{i,n+1}=X_{i,n}$. Since
$X_{i,n}\in\mathscr{T}^{t_{i,n}}_{i,h}$ for all $h\in\mathbb{N}$, we conclude
that $X_{i,n+1}\in\mathscr{T}^{t_{i,n+1}}_{i,h}$ for all $h\in\mathbb{N}$. Put
$X=\bigcap_{i,n\in\mathbb{N}}X_{i,n}$ and $S=\bigcap_{n\in\mathbb{N}}S_{n}$.
Thus, $X$ and $S$ are type-definable, and $S\subseteq X^{2}T\cap A^{2m}$ is
thick in $A^{m}$.

Fix $i\in\mathbb{N}$. Since $X_{i,n}\subseteq B_{i}\subseteq A^{m}$ for every
$n\in\mathbb{N}$, we conclude that

$\mu_{i}(B_{i})\leq\mu_{i}(X_{i,n+1}T_{i}^{k}B_{i}T_{i}^{k}\cap
A^{2m+r})\leq\mu_{i}(A^{2m+r})\leq K_{i}$

by monotonicity and invariance under left translations of $\mu_{i}$.
Consequently, by Lemma 9 applied to the functions
$X\mapsto\mu_{i}(XT_{i}^{k}B_{i}T_{i}^{k}\cap A^{2m+r})$, there is
$n_{i}\in\mathbb{N}$ such that

$\mu_{i}((X_{i,n_{i}}\cap gX_{i,n_{i}}T_{i})T_{i}^{k}B_{i}T_{i}^{k}\cap
A^{2m+r})>(1-\varepsilon_{i})\cdot\mu_{i}(X_{i,n_{i}}T_{i}^{k}B_{i}T_{i}^{k}\cap
A^{2m+r})$

for all $g\in S_{n_{i}}$ and each $k<r$. On the other hand, since
$S_{n}\subseteq S_{n_{i}}$ for all $n>n_{i}$, we get that, for any $n\geq
n_{i}$, all $g\in S_{n}$ and each $k<r$,

$\mu_{i}((X_{i,n}\cap gX_{i,n}T_{i})T_{i}^{k}B_{i}T_{i}^{k}\cap
A^{2m+r})>(1-\varepsilon_{i})\cdot\mu_{i}(X_{i,n}T_{i}^{k}B_{i}T_{i}^{k}\cap
A^{2m+r}).$

Then, for any $n\geq n_{i}$, all $g\in S$ and each $k<r$, we have

$\displaystyle\mu_{i}(X_{i,n}T_{i}^{k}B_{i}T_{i}^{k}\cap
gX_{i,n}T_{i}^{k+1}B_{i}T_{i}^{k}\cap A^{2m+r})$
$\displaystyle\geq\mu_{i}((X_{i,n}\cap
gX_{i,n}T_{i})T_{i}^{k}B_{i}T_{i}^{k}\cap A^{2m+r})$
$\displaystyle>(1-\varepsilon_{i})\cdot\mu_{i}(X_{i,n}T_{i}^{k}B_{i}T_{i}^{k}\cap
A^{2m+r}).$

Hence,

$\displaystyle\mu_{i}((X_{i,n}T_{i}^{k}B_{i}T_{i}^{k}\setminus
gX_{i,n}T_{i}^{k+1}B_{i}T_{i}^{k+1})$ $\displaystyle\cap A^{2m+r})$
$\displaystyle\leq\mu_{i}(X_{i,n}T_{i}^{k}B_{i}T_{i}^{k}\cap A^{2m+r})-$
$\displaystyle\mathrel{\phantom{\leq}}\mu_{i}(X_{i,n}T_{i}^{k}B_{i}T_{i}^{k}\cap
gX_{i,n}T_{i}^{k+1}B_{i}T_{i}^{k}\cap A^{2m+r})$
$\displaystyle<\big{(}1-(1-\varepsilon_{i})\big{)}\cdot\mu_{i}(X_{i,n}T_{i}^{k}B_{i}T_{i}^{k}\cap
A^{2m+r})$ $\displaystyle\leq\varepsilon_{i}\,K_{i}.$

Take $g_{0},\ldots,g_{r-1}\in S$ arbitrary and write $g_{<k}\coloneqq
g_{0}\cdots g_{k-1}$ for each $k<r$. It follows that

$\displaystyle\mu_{i}((X_{i,n}B_{i}\setminus g_{<r}X_{i,n}T_{i}^{r}$
$\displaystyle B_{i}T_{i}^{r})\cap A^{2m})$
$\displaystyle\leq\mu_{i}\left(\textstyle{\bigcup_{k<r}}\,g_{<k}(X_{i,n}T_{i}^{k}B_{i}T_{i}^{k}\setminus
g_{k}X_{i,n}T_{i}^{k+1}B_{i}T_{i}^{k+1})\cap A^{2m}\right)$
$\displaystyle\leq\sum_{k<r}\mu_{j}(g_{<k}(X_{i,n}T_{i}^{k}B_{i}T_{i}^{k}\setminus
g_{k}X_{i,n}T_{i}^{k+1})B_{i}T_{i}^{k+1}\cap A^{2m})$
$\displaystyle\leq\sum_{k<r}\mu_{j}((X_{i,n}T_{i}^{k}B_{i}T_{i}^{k}\setminus
g_{k}X_{i,n}T_{i}^{k+1}B_{i}T_{i}^{k+1})\cap A^{2m+r})$
$\displaystyle<r\,\varepsilon_{i}\,K_{i}<\mu_{i}(B_{i})\leq\mu_{i}(X_{i,n}B_{i}\cap
A^{2m}).$

In particular, $X_{i,n}B_{i}\cap
g_{<r}X_{i,n}T_{i}^{r}B_{i}T_{i}^{r}\neq\emptyset$. By compactness, $XB\cap
g_{<r}XBT_{\infty}\neq\emptyset$ (recall that $T_{\infty}$ is normalised by
$A$, whence by $B$). As $g_{0},\ldots,g_{r-1}\in S$ are arbitrary, we conclude
$S^{r}\subseteq B^{4}T\subseteq A^{4m}T_{\infty}$.∎

######  Theorem 11.

Assume $A$ is $T$-rough definably amenable and suppose that for every
$m\in\mathbb{N}$ there is $i_{m}\in\mathbb{N}$ such that
$\mu_{i}(A^{m})<\infty$ for all $i>i_{m}$. Then, there is a type-definable
normal subgroup $N$ of $\langle AT_{\omega}\rangle$ of bounded index such that
$T\subseteq N\subseteq A^{4}T_{\omega}$.

###### Proof.

We iterate Proposition 10. Put $A_{0}=A$ and, given $A_{n}\subseteq
A^{2^{n}}$, we apply Proposition 10 with $2^{n}$ in place of $m$, $8$ in place
of $r$, the subsequence $(T_{i}\mathrel{:}i>i_{2^{n+1}+8})$, $A_{n}$ in place
of $B$ and set $A_{n+1}$ in place of $S$. Note that $A_{n+1}\subseteq
A_{n}^{2}\subseteq A^{2^{n+1}}$. Clearly,
$H=\bigcap_{n\in\mathbb{N}}A_{n}^{4}T_{\omega}$ is a type-definable subgroup
contained in $A^{4}T_{\omega}$. Note that $H$ is thick in each $A^{m}$ for all
$m$, whence in $A^{m}T_{\omega}$. Thus, the index of $H$ in $\langle
AT_{\omega}\rangle$ is bounded. Now, as $H$ has bounded index in $\langle
AT_{\omega}\rangle$, the intersection of all $\langle
AT_{\omega}\rangle$-conjugates of $H$ is a bounded intersection, whence a
type-definable normal subgroup $N$ in $\langle AT_{\omega}\rangle$ of bounded
index. ∎

######  Definition 12.

Let $K>0$ be an integer and $Z\subseteq G$ a symmetric subset. We say that
$A\subseteq G$ is a $Z$-rough $K$-approximate subgroup if there is a finite
set $E$ of size $K$ such that $A^{2}\subseteq EAZ$.

######  Lemma 13.

Assume $A$ is $T$-rough definably amenable, and suppose $\mu_{i+3}(A^{4})\leq
K_{i}$ for $i\in\mathbb{N}$. Then, $A^{2}$ is a $T_{i}$-rough
$K_{i}^{2}$-approximate subgroup for each $i\in\mathbb{N}$.

###### Proof.

This is just a rough version of Ruzsa’s Covering Lemma. Suppose
$(g_{k}\mathrel{:}k\leq K_{i})$ are in $A^{3}$ with $g_{k}A\cap
g_{k^{\prime}}AT_{i+3}=\emptyset$ for $k\neq k^{\prime}$. Hence,

$K_{i}\geq\mu_{i+3}(A^{4})\geq(K_{i}+1)\mu_{i+3}(A)=K_{i}+1,$

a contradiction. Thus, there is $E\subseteq A^{3}$ of size at most $K_{i}$
such that, for any $g\in A^{3}$, there is $e\in E$ with $gA\cap
eAT_{i+3}\neq\emptyset$, whence $A^{3}\subseteq EAT_{i+3}A\subseteq
EA^{2}T_{i+2}$.

It follows that

$(A^{2})^{2}=A^{3}\cdot A\subseteq EA^{2}T_{i+2}\cdot A=EA^{3}T_{i+1}\subseteq
E^{2}A^{2}T_{i+1}T_{i+2}\subseteq E^{2}A^{2}T_{i},$

concluding that $A^{2}$ is a $T_{i}$-rough $K_{i}^{2}$-approximate.∎

######  Corollary 14.

Assume $A\subseteq G$ is $T$-rough definably amenable, and suppose that
$\mu_{i}(A^{4}T)<\infty$ for all $i\in\mathbb{N}$. Then,
$\mu_{i}(A^{m})<\infty$ for all $m,i\in\mathbb{N}$. In particular, by Theorem
11, there is a type-definable normal subgroup of bounded index of $\langle
AT\rangle$ contained in $A^{4}T$.

###### Proof.

By Lemma 13, $A^{2}$ is a $T_{j}$-rough approximate subgroup for all
$j\in\mathbb{N}$. Thus, for any $m\in\mathbb{N}$, there is $E$ finite such
that $A^{m}\subseteq EA^{2}T_{j}$. Since $\mu_{i}(A^{2}T)<\infty$, there is
$j\in\mathbb{N}$ such that $\mu_{i}(A^{2}T_{j})<\infty$. Thus,
$\mu_{i}(A^{m})\leq|E|\cdot\mu_{i}(A^{2}T_{j})<\infty$. ∎

##  3\. Applications to Metric Groups

We now show how to apply Theorem 11 to get [3, Theorem 20]. Recall that a
_metric group_ is a group $G$ together with a metric $\mathrm{d}$ invariant
under left translations. We denote by $\bar{\mathbb{D}}_{r}$ the closed ball
of radius $r$ at the identity. For $\ell\in\mathbb{N}_{>0}$ and
$r\in\mathbb{R}_{>0}$, a subset $A\subseteq G$ is _$(\ell,r)$ -Lipschitz_ if
every right translation by an element of $A$ is $\ell$-Lipschitz in
$\bar{\mathbb{D}}_{r}$, i.e. $\mathrm{d}(xa,ya)\leq\ell\mathrm{d}(x,y)$ for
any $a\in A$ and $x,y\in\bar{\mathbb{D}}_{r}$. For a subset $Y\subseteq G$, we
define $\mathrm{N}_{r}(Y)\coloneqq\max\\{|Z|\mathrel{:}Z\subseteq Y$ and
$\mathrm{d}(z,z^{\prime})>r$ for all $z,z^{\prime}\in Z$ with $z\neq
z^{\prime}\\}$.

Fix natural numbers $\ell$ and $(K_{i}\mathrel{:}i\in\mathbb{N})$. Let
$(G_{m},A_{m},r_{i,m})_{i\leq m\in\mathbb{N}}$ be a sequence such that

  1. (1)

$G_{m}$ is a metric group,

  2. (2)

$A_{m}$ is an $(\ell,r_{0,m})$-Lipschitz symmetric subset,

  3. (3)

$r_{m}=(r_{i,m})_{i\leq m}$ is a sequence positive real numbers with
$\max\\{\ell,2\\}\cdot r_{i,m}\leq r_{i-1,m}$ and

$\mathrm{N}_{r_{i,m}}(A^{4}_{m})\leq
K_{i}\cdot\mathrm{N}_{r_{i,m}}(A_{m})<\infty.$

Consider the language of groups enriched with a predicate for $X_{m}$ and
predicates for $\bar{\mathbb{D}}_{r_{i,m}}$ for each $i\in\mathbb{N}$ — where
$r_{i,m}=r_{m,m}$ for $i\geq m$; write $\mathtt{L}$ for this language. We
consider $(G_{m},X_{m},r_{i,m})_{i\leq m\in\mathbb{N}}$ as a sequence of
$\mathtt{L}$-structures. Pick a non-principal ultrafilter $\mathfrak{u}$ and
let $(G,A,r)$ be the corresponding ultraproduct. Set
$T_{i}\coloneqq\bar{\mathbb{D}}_{r_{i}}$ and $T=\bigcap T_{i}$.

######  Theorem 15.

$A$ is $T$-rough definably amenable with respect to
$\mu_{i}(Y)\coloneqq\frac{\mathrm{N}_{r_{i}}(Y)}{\mathrm{N}_{r_{i}}(A)}$ and
$\mu_{i}(A^{4}T)<\infty$ for any $i\in\mathbb{N}_{>0}$.

###### Proof.

As $A$ is $(\ell,r_{0})$-Lipschitz and $\ell r_{i+1}\leq r_{i}$,
$T_{i+1}^{A}\subseteq T_{i}$. Since $2r_{i+1}\leq r_{i}$,
$T_{i+1}T_{i+1}\subseteq T_{i}$. Obviously, $\mathrm{N}_{r_{i}}$ is a
$T_{i}$-rough measure on the boolean algebra of definable subsets invariant
under left translations. Hence, $A$ is $T$-rough definably amenable with
respect to the normalisation $\mu_{i}$. Finally, note that
$\mu_{i}(A^{4}T)\leq\mu_{i}(A^{4}T_{i+2})\leq\mu_{i-1}(A^{4})\leq K_{i-1}$ for
any $i\in\mathbb{N}_{>0}$. ∎

By Corollary 14, we conclude that that there is a type-definable normal
subgroup $N$ of $\langle AT\rangle$ of bounded index such that $T\subseteq
N\subseteq A^{4}T$. In other words, we get [3, Theorem 20(1)].

For [3, Theorem 20(2)], note that, when $(K_{i}\mathrel{:}i\in\mathbb{N})$ is
constant, by Lemma 13, $A^{2}$ is a $T_{\omega}$-rough $K$-approximate
subgroup. Thus, by [5, Theorem 3.31], we conclude that $AT$ has a connected
Lie model $\pi:\,H\rightarrow L$, i.e. a group homomorphism with dense image
to a connected Lie group $L$ defined on a subgroup $H\leq\langle AT\rangle$
with kernel $T\trianglelefteq\ker(\pi)\subseteq A^{8}T$ such that

(1) $H\cap A^{4}T$ and $A^{2}T$ are commensurable,

(2) $H\cap A^{8}T$ generates $H$,

(3) $\pi[H\cap A^{4}]$ is a compact neighbourhood of the identity of $L$, and

(4) $\pi$ is continuous and proper from the logic topology of $\mathtt{L}$
using countably many parameters.

## References

  * [1] Breuillard, E.; Green, B. & Tao, T. (2012).  “The structure of approximate groups”,  Pubilcations mathématiques de l’IHÉS 116: 115–221.  DOI:10.1007/s10240-012-0043-9.
  * [2] Hrushovski, E. (2011).  “Stable group theory and approximate subgroups”,  Journal of the American Mathematical Society 25(1): 189–243.  DOI:10.1090/S0894-0347-2011-00708-X.
  * [3] Hrushovski, E. & Rodríguez Fanlo, A. (2022).  On metric approximate subgroups.  arXiv:2209.01262.
  * [4] Massicot, J.-C. & Wagner, F. O. (2015).  “Approximate subgroups”,  Journal de l’École polytechnique—Mathématiques 2: 55–63.  DOI:10.5802/jep.17.
  * [5] Rodríguez Fanlo, A. (2020).  On piecewise hyperdefinable groups.  arXiv:2011.11669v4