Complexity Analysis of Tree Share Structure†

Xuan-Bach Le†

Aquinas Hobor‡,∗‡∗

University of Oxford

Yale-NUS College

Anthony W. Lin†

National University of Singapore

Abstract. The tree share structure proposed by Dockins et al. is anelegant model for tracking disjoint ownership in concurrent separation
logic, but decision procedures for tree shares are hard to implement due
to a lack of a systematic theoretical study. We show that the first-ordertheory of the full Boolean algebra of tree shares (that is, with all treeshare constants) is decidable and has the same complexity as of the firstorder theory of Countable Atomless Boolean Algebras. We prove thatcombining this additive structure with a constant-restricted unary multiplicative “relativization” operator has a non-elementary lower bound.
We examine the consequences of this lower bound and prove that it comesfrom the combination of both theories by proving an upper bound on a
generalization of the restricted multiplicative theory in isolation.

1

Introduction

One general challenge in concurrent program verification is how to specify theownership of shared resources among threads. A common solution is to tag sharedresources with fractional shares that track “how much” of a resource is owned
by an actor. A policy maps ownership quanta with permitted behaviour. For
example, a memory cell can be “fully owned” by a thread, permitting both
reading and writing; “partially owned”, permitting only reading; or “unowned”,
permitting nothing; the initial model of fractional shares [8] was rationals in [0, 1].
Since their introduction, many program logics have used a variety of flavors offractional permissions to verify programs [8, 7, 33, 18, 3, 37, 2, 24, 38, 15, 26, 14].
Rationals do not mix cleanly with concurrent separation logic [31] because
they do not preserve the “disjointness” property of separation logic [32]. Dockins
et al. [13] proposed a “tree share” model that do preserve this property, and soa number of program logics have incorporated them [19, 18, 37, 2, 26].
In addition to their good metatheoretic properties, tree shares have desirable
computational properties, which has enabled several highly-automated verification tools to incorporate them [37, 20] via heuristics and decision procedures [25,28]. As we shall explain in §2.2, tree shares have both “additive” and “multiplicative” substructures. All of the verification tools used only a restricted fragmentof the additive substructure (in particular, with only one quantifier alternation)
because the general theory’s computational structure was not well-understood.
These structures are worthy of further study both because even short programs
can require hundreds of tree share entailment queries in the permitted formalism [16, Ch4:§2,§6.4,§6.6], and because recent program logics have shown how
the multiplicative structures aid program verification [2, 26].

Recently, Le et al. did a more systematic analysis of the computational complexity of certain classes of tree share formulae [27]; briefly:– the additive structure forms a Countable Atomless Boolean Algebra, giving
a well-understood complexity for all first-order formulae so long as they only
use the distinguished constants “empty” 0 and “full” 1;– the multiplicative structure has a decidable existential theory but an undecidable first-order theory; and– the additive theory in conjunction with a weakened version of the multiplicative theory—in particular, only permitting multiplication by constantson the right-hand side—regained first-order decidability.
Contributions. We address significant gaps in our theoretical understandingof tree shares that deter their use in automated tools for more sophisticated tasks.
§3 Moving from a restricted fragment of a first-order additive theory to themore general setting of unrestricted first-order formulae over Boolean operations is intuitively appealing due to the increased expressibility of the logic.
This expressibility even has computational consequences, as we demonstrateby using it to remove a common source of quantifier alternations. However,verifications in practice often require formulae that incorporate more general
constants than 0 and 1, limiting the application of the analysis from [27] inpractice. This is unsurprising since it is true in other settings: many Presburger formulae that arise in engineering contexts, for example, are litteredwith application-specific constants, e.g., ∀x.(∃y.x + y = 7) ⇒ (x + 13 < 21).
A recent benchmark using tree shares for program verification [28] supports
this intuition: it made 16k calls in the supported first-order additive fragment, and 21.1% (71k/335k) of the constants used in practice were neither
0 nor 1. Our main contribution on the additive side is to give a polynomialtime algorithm that reduces first-order additive formulae with arbitrary treeshare constants to first-order formulae using only 0 and 1, demonstratingO(1)that the additive structure’s exact complexity is STA(∗, 2n, n)-complete
and closing the theory/practice gap between [27] and [28].
§4 We examine the combined additive/restricted multiplicative theory proved
decidable in [27]. We prove a nonelementary lower bound for this theory, via
a reduction from the combined theory into the string structure with suffix
successors and a prefix relation, closing the complexity gap in the theory.
§5 We investigate the reasons for, and mitigants to, the above nonelementary
lower bound. First, we show that the first-order restricted-multiplicative theory on its own (i.e., without the Boolean operators) has elementary complexity via an efficient isomorphism with strings equipped with prefix and suffix
successors. Thus, the nonelementary behavior comes precisely from the combination of both theories. Lastly, we examine the kinds of formulae that we
expect in practice—for example, those coming from biabduction problems
discussed in [26]—and notice that they have elementary complexity.

The other sections of our paper support our contributions by (§2) overviewing tree shares, related work, and several basic complexity results; and by (§6)
discussing directions for future work and concluding.

2

Preliminaries

Here we document the preliminaries for our result. Some are standard (§2.1)
while others are specific to the domain of tree shares (§2.2–§2.4).
2.1

Complexity preliminaries

We assume that the readers are familiar with basic concepts in computational
complexity such as Turing machine, many-one reduction, space and time complexity classes such as NP and PSPACE. A problem is nonelementary if it cannot
be solved by any deterministic Turing machine that can be time-bounded by oneof the exponent functions exp(1) = 2n , exp(n + 1) = 2exp(n) . Let A, R be complexity classes, a problem P is ≤R -complete for A iff P is in A and every problem
in A is many-one reduced into P via Turing machines in R. In addition, we use≤R-lin to assert linear reduction that belongs to R and only uses linear spacewith respect to the problem’s size. In particular, ≤log-lin is linear log-space reduction. Furthermore, we denote STA(p(n), t(n), a(n)) the class of alternating
Turing machine [9] that uses at most p(n) space, t(n) time and a(n) alternations
between universal states and existential states or vice versa for input of lengthn. If any of the three bounds is not specified, we replace it with the symbolO(1)∗, e.g. STA(∗, 2n, n) is the class of alternating Turing machines that haveexponential time complexity and use at most n alternations.
2.2

Overview of tree share structure

A tree share is a binary tree with Boolean leaves ◦ (white leaf) and • (black leaf).
Full ownership is represented by • and no ownership by ◦. For fractional ownership, one can use, e.g. • ◦, to represent the left half-owned resource. Importantly
and usefully, ◦ • is a distinct tree share representing the other right half. We require tree shares are in canonical form, that is, any subtree τ τ where τ ∈ {•, ◦}needs to be rewritten into τ . For example, both • ◦ andrepresent the••◦◦◦same tree share but only the former tree is canonical and thus valid. As a result,the set of tree shares T is a strict subset of the set of all Boolean binary trees.
Tree shares are equipped with Boolean operators t (union), u (intersection) and¯· (complement). When applied to tree shares of height zero, i.e. {•, ◦}, these operators give the same results as in the case of binary BA. Otherwise, our tree
shares need to be unfolded and folded accordingly before and after applying theoperators leaf-wise, e.g.
•◦=◦•

∼
∼
•◦•t◦◦•=•◦••t◦◦◦•=•◦••=•◦• .

The additive operator ⊕ can be defined using t and u, i.e. disjoint union:defa ⊕ b = c = a t b = c ∧ a u b = ◦.
Tree shares also have a multiplicative operator ./ called “bowtie”, where τ1 ./ τ2
is defined by replacing each black leaf • of τ1 with an instance of τ2 , e.g.
•◦◦•./ ◦ • =◦•◦◦◦•.

While the ⊕ operator has standard additive properties such as commutativity, associativity and cancellativity, the ./ operator enjoys the unit •, is associative, injective over non-◦ arguments, and distributes over {t, u, ⊕} on theleft [13]. However, ./ is not commutative, e.g.:• ◦ ./ ◦ • = ◦ • ◦ 6= ◦ • ◦ = ◦ • ./ • ◦The formalism of these binary operators can all be found in [13].
2.3Tree shares in program verification

Fractional permissions in general, or tree shares in particular, are integrated
into separation logic to reason about ownership. In detail, the mapsto predicateπx 7→ v is enhanced with the permission π, denoted as x 7−
→ v, to assert that π isassigned to the address x associated with the value v. This notation of fractional
mapsto predicate allows us to split and combine permissions conveniently using
the additive operator ⊕ and disjoint conjunction ?:
π ⊕π

π

π

2
1
2
x 7−−1−−→v a` x 7−→v ? x 7−→v.

(1)

The key difference between tree share model hT, ⊕i and rational model hQ, +i
is that the latter fails to preserve the disjointness property of separation logic.
For instance, while the predicate x 7→ 1 ? x 7→ 1 is unsatisfiable, its rational
0.5
0.5
1
version x 7−−→ 1 ? x 7−−→ 1, which is equivalent to x 7−
→ 1 by (1), is satisfiable.
•◦•◦
On the other hand, the tree share version x 7−−→ ?x 7−−→ remains unsatisfiable
as the sum • ◦ ⊕ • ◦ is undefined. Such defect of the rational model gives riseto the deformation of recursive structures or elevates the difficulties of modular
reasoning, as first pointed out by [32].
Recently, Le and Hobor [26] proposed a proof system for disjoint permissions
using the structure hT, ⊕, ./i. Their system introduces the notion of predicate
multiplication where π · P asserts that the permission π is associated with thepredicate P . To split the permission, one can apply the following bi-entailment:
π · P a` (π ./ • ◦) · P ? (π ./ ◦ •) · P.
which requires the following property of tree shares to hold:∀π. π = (π ./ • ◦) ⊕ (π ./ ◦ •).

(2)

Note that the above property demands a combined reasoning of both ⊕and ./. While such property can be manually proved in theorem provers suchas Coq [12] using inductive argument, it cannot be handled automatically by
known tree share solvers [25, 28] due to the shortness of theoretical insights.
2.4

Previous results on the computational behavior of tree shares

The first sophisticated analysis of the computational properties of tree shareswere done by Le et al. [27]. They showed that the structure hT, t, u,¯·i is a
Countable Atomless BA and thus is complete for the Berman complexity class
O(1)STA(∗, 2n, n)—problems solved by alternating exponential-time Turing machines with unrestricted space and n alternations—i.e. the same complexity as
the first-order theory over the reals hR, +, 0, 1i with addition but no multiplication [4]. However, this result is restrictive in the sense that the formula classonly contains {•, ◦} as constants, whereas in practice it is desirable to permit
arbitrary tree constants, e.g. ∃a∃b. a t b = • ◦.
When the multiplication operator ./ is incorporated, the computational nature of the language becomes harder. The structure hT, ./i—without the Boolean
operators—is isomorphic to word equations [27]. Accordingly, its first-order theory is undecidable while its existential theory is decidable with continuously
improved complexity bounds currently at PSPACE and NP-hard (starting from
Makanin’s argument [29] in 1977 and continuing with e.g. [22]).
Inspired by the notion of “semiautomatic structures” [21], Le et al. [27] restricted ./ to take only constants on the right-hand side, i.e. to a family of
defunary operators indexed by constants ./τ (x) = x ./ τ . Le et al. then examineddef

C = hT, t, u,¯·, ./τ i. Note that the verification-sourced sentence (2) from §2.3 fits
perfectly into C: ∀π. π = ./ (π) ⊕ ./ (π). Le et al. encoded C into tree•◦◦•automatic structures [6], i.e., logical structures whose constants can be encoded
as trees, and domains and predicates finitely represented by tree automata. As
a result, its first-order theory—with arbitrary tree constants—is decidable [6, 5,36], but until our results in §4 the true complexity of C was unknown.

3

defComplexity of Boolean structure A = hT, t, u,¯·iExisting tree share solvers [25, 28] only utilize the additive operator ⊕ in certain restrictive first-order segments. Given the fact that ⊕ is defined from theBoolean structure A = hT, t, u,¯·i, it is compelling to establish the decidability
and complexity results over the general structure A. More importantly, operators
in A can help reduce the complexity of a given formula. For example, consider
the following separation logic entailment:
••◦
•◦
τ
a 7−
→ 1 ? a 7−−−−→ ` a 7−−→ 1 ? >.

To check the above assertion, entailment solvers have to extract and verify
the following corresponding tree share formula by grouping shares from same
heap addresses using ⊕ and then applying equality checks:∀τ ∀τ 0 .τ ⊕ • • ◦ = τ 0 → ∃τ 00 .τ 00 ⊕ • ◦ = τ 0 .
By using Boolean operators, the above ∀∃ formula can be simplified into a ∀formula by specifying that either the share in the antecedent is not possible, orthe share in the consequent is a ‘sub-share’ of the share in the antecedent:∀τ. ¬(τ u • • ◦ = ◦) ∨ (• ◦ v τ ⊕ • • ◦).
where the ‘sub-share’ relation v is defined using Boolean union:defa v b = a t b = b.
In this section, we will prove the following precise complexity of A:
Theorem 1. The first-order theory of A is ≤log -complete for STA(∗, 2neven if we allow arbitrary tree constants in the formulae.

O(1)

, n),

One important implication of the above result is that the same complexity
result still holds even if the additive operator ⊕ is included into the structure:
Corollary 1. The Boolean tree share structure with addition A⊕ = hT, ⊕, t, u,¯·iO(1)is ≤log -complete for STA(∗, 2n, n), even with arbitrary tree constants in theformulae.
Proof. Recall that ⊕ can be defined in term of t and u without additional
quantifier variable:
a⊕b=c

def

=

a t b = c ∧ a u b = ◦.

As a result, one can transform, in linear time, any additive constraint into
Boolean constraint using the above definition. Hence the result follows.
tu
Theorem 1 is stronger than the result in [27] which proved the same complexity but for restricted tree share constants in the formulae:
Proposition 1 ([27]). The first-order theory of A, where tree share constantsO(1)are {•, ◦}, is ≤log -complete for STA(∗, 2n, n).
The hardness proof for lower bound of Theorem 1 is obtained directly from
Prop. 1. To show that the same complexity holds for upper bound, we construct an O(n2 ) algorithm flatten (Alg. 1) that transforms arbitrary tree shareformula into an equivalent tree share formula whose constants are {•, ◦}:Lemma 1. Suppose flatten(Φ) = Φ0 . Then:Algorithm 1 Flattening a Boolean tree share formula
1: function flatten(Φ)
Require: Φ is a Boolean tree sentence
Ensure: Return an equivalent formula of height zero2:
if height(Φ) = 0 then return Φ
3:
else
4:
let s be the shape of Φ5:for each atomic formula Ψ in Φ: t1 = t2 or t1 op t2 = t3 , op ∈ {t, u} do
6:[ti1 , . . . tin ] ← split(ti , s) for i = 1 . . . n . n is the number of leaves in s7:
Ψi ← ti1 = ti2 or ti1 opVti2 = ti3 for i = 1 . . . n8:Φ ← replace Ψ with n
i=1 Ψi9:end for10:
for each quantifier Qv in Φ do
11:
[v1 , . . . , vn ] ← split(v, s)
12:Φ ← replace Qv with Qv1 . . . Qvn
13:
end for14:
return Φ
15:
end if
16: end function
17:
18: function split(t, s)
Require: t is either a variable or a constant, s is a shape
Ensure: Return a list of decomposing components of t according to shape s
19:
if s = ∗ then return [t]20:else let s = s0 s1 in
21:
22:

if t is • or ◦ then return concat(split(t, s0 ), split(t, s1 ))else if let t = t1 t2 in then return concat(split(t0 , s0 ), split(t1 , s1 ))23:
elset is a variable return concat(split(t0 , s0 ), split(t1 , s1 ))24:
end if25:
end if
26: end function

1. Φ0 only contains {•, ◦} as constants.
2. Φ and Φ0 have the same number of quantifier alternations.
3. Φ and Φ0 are equivalent with respect to A.
4. flatten is O(n2 ). In particular, if the size of Φ is n then Φ0 has size O(n2 ).
Proof of Theorem 1. The lower bound follows from Prop. 1. By Lemma 1,
we can use flatten in Alg. 1 to transform a tree formula Φ into an equivalent
formula Φ0 of size O(n2 ) that only contains {•, ◦} as constants and has thesame number of quantifier alternations as in Φ. By Prop. 1, Φ0 can be solved in
O(1)STA(∗, 2n, n). This proves the upper bound and thus the result follows. tuIt remains to prove the correctness of Lemma 1. But first, we will provide a
descriptive explanation for the control flow of flatten in Alg. 1. On line 2, it
checks whether the height of Φ, which is defined to be the height of the highest tree constant in Φ, is zero. If it is the case then no further computation isneeded as Φ only contains {•, ◦} as constants. Otherwise, the shape s (Defini-tion 1) is computed on line 4 to guide the subsequent decompositions. On lines
5-9, each atomic sub-formula Ψ is decomposed into sub-components according
to the shape s by the function split described on lines 18-26. Intuitively, split
decomposes a tree τ into subtrees (line 21-22) or a variables v into new variables
with appropriate binary subscripts (line 23). V
On line 8, the formula Ψ is replacednwith the conjunction of its sub-components i=1 Ψi . Next, each quantifier variable Qv in Φ is also replaced with a sequence of quantifier variables Qv1 . . . Qvn(lines 10-13). Finally, the modified formula Φ is returned as the result on line
14. The following example demonstrates the algorithm in action:
Example 1. Let Φ : ∀a∃b. a t b = • ◦ ◦ ∨ ¬(ā = ◦ • ◦). Then height(Φ) = 2 > 0
and its shape s is

. Also, Φ contains the following atomic sub-formulae:∗∗∗∗Ψ : atb=•◦◦and Ψ 0 : ā = ◦ • ◦ .

After applying the split function to Ψ and Ψ 0 with shape s, we acquire thefollowing components:
1. Ψ1 : a00 t b00 = •, Ψ2 : a01 t b01 = ◦, Ψ3 : a10 t b10 = ◦, Ψ4 : a11 t b11 = ◦.
2. Ψ10 : a00 = ◦, Ψ20 : a01 = ◦, Ψ30 : a10 = •, Ψ40 : a11 = ◦.
V4
The following result formula is obtained by replacing Ψ with i=1 Ψi , Ψ 0 withV40
i=1 Ψi , ∀a with ∀a00 ∀a01 ∀a10 ∀a11 , and ∃b with ∃b00 ∃b01 ∃b10 ∃b11 :∀a00 ∀a01 ∀a10 ∀a11 ∃b00 ∃b01 ∃b10 ∃b11 .

4^

Ψi ∨ ¬(i=14^

Ψi0 ).

i=1

Definition 1 (Tree shape). A shape of a tree τ , denoted by hτ i, is obtainedby replacing its leaves with ∗, e.g. h• • ◦i = ∗ ∗ ∗. The combined shape s1 t s2
is defined by overlapping s1 and s2 , e.g. ∗ ∗ ∗ t ∗ ∗ ∗ =. The shape of a∗∗∗∗formula Φ, denoted by hΦi, is the combined shape of its tree constants and ∗.
Note that tree shapes are not canonical, otherwise all shapes are collapsed
into a single shape ∗. We are now ready to prove the first three claims ofLemma 1:
Proof of Lemma 1.1, 1.2 and 1.3. Observe that the shape of each atomic
sub-formula Ψ is ‘smaller’ than the shape of Φ, i.e. hΨ i t hΦi = hΦi. As a result,each formula in the decomposition of split(Ψ, hΦi) always has height zero, i.e.
its only constants are {•, ◦}. This proves claim 1.
Next, recall that the number of quantifier alternations is the number of times
where quantifiers are switched from ∀ to ∃ or vice versa. The only place thatflatten modifies quantifiers is on line 12 in which the invariant for quantifier
alternations is preserved. As a result, claim 2 is also justified.
We are left with the claim that flatten is O(n2 ) where n is the size of the
input formula Φ. By a simple analysis of flatten, it is essentially equivalentto show that the result formula has size O(n2 ). First, observe that the formulashape hΦi has size O(n) and thus we need O(n) decompositions for each atomic
sub-formula Ψ and each quantifier variable Qv of Φ. Also, each component in
the decomposition of Ψ (or Qv) has size at most the size of Ψ (or Qv). As aresult, the size of the formula Φ0 only increases by a factor of O(n) compared tothe size of Φ. Hence Φ0 has size O(n2 ).
tu
To prove claim 4, we first establish the following result about the split
function. Intuitively, this lemma asserts that one can use split together withsome tree shape s to construct an isomorphic Boolean structure whose elements
are lists of tree shares:def) = [• ◦, •, •].
(∗∗∗ •◦•
Then splits is an isomorphism from A to A0 = hTn , t0 , u0 ,¯·0 i where n is thenumber of leaves in s and each operator in M0 is defined component-wise fromthe corresponding operator in A, e.g. [a1 , a2 ] t0 [b1 , b2 ] = [a1 t a2 , b1 t b2 ].

Lemma 2. Let splits = λτ. split(τ, s), e.g. split

Proof. W.l.o.g. we will only prove the case s = ∗ ∗ as similar argument can beobtained for the general case. By inductive arguments, we can prove that splits
is a bijection from T to T × T. Furthermore:
1. splits (a)  splits (b) = splits (c) iff a  b = c for  ∈ {t, u}.
2. splits (τ̄ ) = splits (τ ) .
Hence splits is an isomorphism from A to A0 = hT × T, t0 , u0 ,¯·0 i.

tuProof of Lemma 1.4. By Lemma 2, the function splits allows us to transform formulae in A into equivalent formulaes over tree share lists in A0 =hTn , t0 , u0 ,¯·0 i. On the other hand, observe that formulae in A0 can be rewritten
into equivalent formulae in A using conjunctions and extra quantifier variables,e.g. ∃a∀b. at0 b = [◦ •, •] is equivalent to ∃a1 ∃a2 ∀b1 ∀b2 . a1 tb1 = ◦ • ∧a2 tb2 = •.
Hence the result follows.
tu
The correctness of Lemma 1 is now fully justified. We end this section by
pointing out a refined complexity result for the existential theory of A, whichcorresponds to the satisfiability problem of quantifier-free formulae. Note thatthe number of quantifier alternations for this fragment is zero, and thus TheoO(1)rem 1 only gives us an upper bound STA(∗, 2n, 0), which is exponential timecomplexity. Instead, we can use Lemma 1 to acquire the precise complexity:
Corollary 2. The existential theory of A, with arbitrary tree share constants,
is NP-complete.
Proof. Recall a classic result that existential theory of Countably Atomless BAs
is NP-complete [30]. As A belongs to this class, the lower bound is justified.
To see why the upper bound holds, we use the function flatten to transformthe input formula into standard BA formula and thus the result follows from
Lemma 1.
t
u

4

def

Complexity of combined structure C = hT, t, u,¯·, ./τ i

In addition to the Boolean operators in §3, recall from §2.2 that tree shares also
possess a multiplicative operator ./ that resembles the multiplication of rational
permissions. As mentioned in §2.4, [27] showed that ./ is isomorphic to string
concatenation, implying that the first-order theory of hT, ./i is undecidable, andso of course the first-order theory of hT, t, u,¯·, ./i is likewise undecidable.
By restricting multiplication to have only constants on the right-hand side,def
however, i.e. to the family of unary operators ./τ (x) = x ./ τ , Le et al.
showed that decidability of the first-order theory was restored for the combineddefstructure C = hT, t, u,¯·, ./τ i. However, Le et al. were not able to specify any
particular complexity class. In this section, we fill in this blank by proving thatthe first-order theory of C is nonelementary, i.e. that it cannot be solved by any
resource-bound (space or time) algorithm:
Theorem 2. The first-order theory of C is non-elementary.
To prove Theorem 2, we reduce the binary string structure with prefix relation [11], which is known to be nonelementary, into C. Here we recall thedefinition and complexity result of binary strings structure:
Proposition 2 ([11, 35]). Let K = h{0, 1}∗ , S0 , S1 , i be the binary string
structure in which {0, 1}∗ is the set of binary strings, Si is the successor function
s.t. Si (s) = s · i, and  is the binary prefix relation s.t. x  y iff there exists z
satisfies x · z = y. Then the first-order theory of K is non-elementary.
Before going into the technical detail, we briefly explain the many-one reduction from K into C. The key idea is that the set of binary strings {0, 1}∗ canbe bijectively mapped into the set of unary trees U(T), trees that have exactly
one black leaf, e.g. {•, • ◦, ◦ •, ◦ • ◦, · · · }. For convenience, we use the symbol L
to represent the left tree • ◦ and R for the right tree ◦ •. Then:
Lemma 3. Let g map h{0, 1}∗ , S0 , S1 , i into hT, t, u,¯·, ./τ i such that:
1. g() = •, g(0) = L, g(1) = R.
2. g(b1 . . . bn ) = g(b1 ) ./ . . . ./ g(bn ), bi ∈ {0, 1}.
3. g(S0 ) = λs. ./L (g(s)), g(S1 ) = λs. ./R (g(s)).
def

4. g(x  y) = g(y) v g(x) where τ1 v τ2 = τ1 t τ2 = τ2 .
Then g is a bijection from {0, 1}∗ to U(T), and x  y iff g(y) v g(x).
Proof. The routine proof that g is bijective is done by induction on the string
length. Intuitively, the binary string s corresponds to the path from the tree rootin g(s) to its single black leaf, where 0 means ‘go left’ and 1 means ‘go right’. For
example, the tree g(110) = R ./ R ./ L = ◦ • ./ ◦ • ./ • ◦ = ◦corresponds◦•◦
to the path right→right→left.

Now observe that if τ1 , τ2 are unary trees then τ1 v τ2 (i.e. the black-leaf
path in τ2 is a sub-path of the black-leaf path in τ1 ) iff there exists a unary tree
τ3 such that τ2 ./ τ3 = τ1 (intuitively, τ3 represents the difference path between
τ2 and τ1 ). Thus x  y iff there exists z such that xz = y, iff g(x) ./ g(z) = g(y),which is equivalent to g(y) v g(x) by the above observation.
tu
In order for the reduction to work, we need to express the type of unary
trees using operators from C. The below lemma shows that the type of U(T) isexpressible via a universal formula in C:
Lemma 4. A tree τ is unary iff it satisfies the following ∀-formula:τ 6= ◦ ∧∀τ 0 . τ 0 ./ L @ τ ↔ τ 0 ./ R @ τ .

defwhere τ1 @ τ2 = τ1 t τ2 = τ2 ∧ τ1 6= τ2 .
Proof. The ⇒ direction is proved by induction on the height of τ . The key
observation is that if τ1 ./ τ2 @ τ3 and τ2 , τ3 are unary then τ1 is also unary,τ1 v τ3 and thus τ1 ./ τ2 @ τ3 . Note that both L, R are unary and L = R, hence
the result follows.
For ⇐, assume τ is not unary. As τ 6= ◦, it follows that τ contains at least two
black leaves in its representation. Let τ1 be the tree that represents the path toone of the black leaves in τ , we have τ1 @ τ and for any unary tree τ2 , if τ1 @ τ2
then τ2 6v τ . As τ1 is unary, we can rewrite τ1 as either τ10 ./ L or τ10 ./ R for someunary tree τ10 . The latter disjunction together with the equivalence in the premise
give us both τ10 ./ L @ τ and τ10 ./ R @ τ . Also, we have τ1 @ τ10 and thus τ10 6v τby the aforementioned observation. Hence τ10 = τ1 ./ • = τ10 ./ (L t R) v τwhich is a contradiction.
tu
Proof of Theorem 2. We employ the reduction technique in [17] where formulae in K are interpreted using the operators from C. The interpretation of
constants and operators is previously mentioned and justified in Lemma 3. We
then replace each sub-formula ∃x. Φ with ∃x. x ∈ U(T) ∧ Φ and ∀x. Φ with∀x. x ∈ U(T) → Φ using the formula in Lemma 4. It follows that the first-ordercomplexity of C is bounded below by the first-order complexity of K. Hence byProp. 2, the first-order complexity of C is nonelementary.
tu5Causes of, and mitigants to, the nonelementary bound

Having proven the nonelementary lower bound for the combined theory in §4, we
discuss causes and mitigants. In §5.1 we show that the nonelementary behaviorof C comes from the combination of both the additive and multiplicative theories
by proving an elementary upper bound on a generalization of the multiplicative
theory, and in §5.2 we discuss why we believe that verification tools in practicewill avoid the nonelementary lower bound.

5.1

def

Complexity of multiplicative structure B = hT,τ ./, ./τ i

Since the first-order theory over hT, ./i is undecidable, it may seem plausiblethat the nonelementary behaviour of C comes from the ./τ subtheory rather
than the “simpler” Boolean subtheory A, even though the specific proof of thelower bound given in §4 used both the additive and multiplicative theories (e.g.
in Lemma 4). This intuition, however, is mistaken. In fact, even if we generalize
the theory to allow multiplication by constants on either side—i.e., by addingdefdefτ ./(x) = τ ./ x to the language—the restricted multiplicative theory B =hT,τ ./, ./τ i is elementary. Specifically, we will prove that the first-order theoryof B is STA(∗, 2O(n) , n)-complete and thus elementarily decidable:
Theorem 3. The first-order theory of B is ≤log-lin -complete for STA(∗, 2O(n) , n).
Therefore, the nonelementary behavior of C arises precisely because of the combination of both the additive and multiplicative subtheories.
We prove Theorem 3 by solving a similar problem in which two tree shares{•, ◦} are excluded from the tree domain T. That is, let T+ = T\{•, ◦} andB + = hT+ ,τ ./, ./τ i, we want:
Lemma 5. The complexity of Th(B + ) is ≤log-lin -complete for STA(∗, 2O(n) , n).
By using Lemma 5, the proof for the main theorem is straightforward:
Proof of Theorem 3. The hardness proof is direct from the fact that membership constraint in B + can be expressed using membership constraint in B:τ ∈ B + iff τ ∈ B ∧ τ 6= ◦ ∧ τ 6= •.
As a result, any sentence from B + can be transformed into equivalent sentencein B by rewriting each ∀v.Φ with ∀v.(v 6= ◦ ∧ v 6= •) → Φ and each ∃v.Φ with∃v.v 6= ◦ ∧ v 6= • ∧ Φ.
To prove the upper bound, we use the guessing technique as in [27]. In detail,we partition the domain T into three disjoint sets:
S1 = {◦}

S2 = {•}

S3 = T+ .

Suppose the input formula contains n variables, we then use a ternary vectorof length n to guess the partition domain of these variables, e.g., if a variable
v is guessed with the value i ∈ {1, 2, 3} then v is assigned to the domain Si . In
particular, if v is assigned to S1 or S2 , we substitute v for ◦ or • respectively.
Next, each bowtie term ./τ (a) or τ ./(a) that contains tree share constants • or
◦ is simplified using the following identities:
τ ./ • = • ./ τ = τ

τ ./ ◦ = ◦ ./ τ = ◦ .

After this step, all the atomic sub-formulae that contain ◦ or • are reduced
into either variable equalities v1 = v2 , v = τ or trivial constant equalities suchas • = •, • ◦ = ◦ that can be replaced by either > or ⊥. As a result, thenew equivalent formula is free of tree share constants {•, ◦} whilst all variables
are quantified over the domain T+ . Such formula can be solved using the Turingmachine that decides Th(B + ). The whole guessing process can be integrated into
the alternating Turing machine without increasing the formula size or numberof quantifiers (i.e. the alternating Turing machine only needs to make two extra
guesses • and ◦ for each variable and the simplification only takes linear time).
Hence this justifies the upper bound.
tu
The rest of this section is dedicated to the proof of Lemma 5. To provethe complexity Th(B + ), we construct an efficient isomorphism from B + to thestructure of ternary strings in {0, 1, 2}∗ with prefix and suffix successors. The
existence of such isomorphism will ensure the complexity matching between thetree structure and the string structure. Here we recall a result from [34] about
the first-order complexity of the string structure with successors:
Proposition 3 ([34]). Let S = h{0, 1}∗ , P0 , P1 , S0 , S1 i be the structure of binary strings with prefix successors P0 , P1 and suffix successors S0 , S1 such that:
P0 (s) = 0 · s

P1 (s) = 1 · s

S0 (s) = s · 0

S1 (s) = s · 1.

Then the first-order theory of S is ≤log-lin -complete for STA(∗, 2O(n) , n).
The above result cannot be used immediately to prove our main theorem.
Instead, we use it to infer a more general result where successors are not only
restricted to 0 and 1, but also allowed to be any string s in a finite alphabet:
Lemma 6. Let Σ be a finite alphabet of size k ≥ 2 and S 0 = hΣ ∗ , Ps , Ss i thestructure of k-ary strings with infinitely many prefix successors Ps and suffix
successors Ss where s ∈ Σ ∗ such that:Ps (s0 ) = s · s0

Ss (s0 ) = s0 · s.

Then the first-order theory of S 0 is ≤log-lin -complete for STA(∗, 2O(n) , n).
Proof. Although the proof in [34] only considers binary alphabet, the same result
still holds even for finite alphabet Σ of size k ≥ 2 with k prefix and suffix
successors. Let s = a1 . . . an where ai ∈ Σ, the successors Ps and Ss can be
defined in linear size from successors in S as follows:def

Ps = λs0 . Pa1 (. . . Pan (s0 ))def

Ss = λs0 . San (. . . Sa1 (s0 )).

These definitions are quantifier-free and thus the result follows.

tu

Next, we recall some key results from [27] that establishes the fundamental
connection between trees and strings in word equation:
Proposition 4 ([27]). We call a tree τ in T+ prime if τ = τ1 ./ τ2 implies
either τ1 = • or τ2 = •. Then for each tree τ in T+ , there exists a uniquesequence of prime trees {τi }ni=1 such that τ = τ1 ./ · · · ./ τn . As a result, eachtree in T+ can be treated as a string in a word equation in which the alphabet isP, the countably infinite set of prime trees, and ./ is the string concatenation.

For example, the factorization of◦•◦◦◦•◦is • ◦ • ./ • ◦ ./ ◦ •, which is

unique. Prop. 4 asserts that by factorizing tree shares into prime trees, we caneffectively transform multiplicative tree share constraints into equivalent word
equations. Ideally, if we can represent each prime tree as a unique letter in thealphabet then Lemma 5 would follow from Lemma 6. Unfortunately, the set ofprime trees P are infinite [27] while Lemma 6 requires a finite alphabet. As aresult, our tree encoding needs to be more sophisticated than the naı̈ve way. The
key observation here is that, as P is countably infinite, there must be a bijective
encoding function I : P 7→ {0, 1}∗ that encodes each prime tree into binary
string, including the empty string . We need not to know the construction of I
in advance, but it is important to keep in mind that I exists and the delay of
its construction is intentional. We then extend I into Iˆ that maps tree shares in
T+ into ternary string in {0, 1, 2}∗ where the letter 2 purposely represents thedelimiter between two consecutive prime trees:
Lemma 7. Let Iˆ : T+ 7→ {0, 1, 2}∗ be the mapping from tree shares into ternary
strings such that for prime trees τi ∈ P where i ∈ {1, . . . , n}, we have:ˆ 1 ./ . . . ./ τn ) = I(τ1 ) · 2 . . . 2 · I(τn ).
I(τBy Prop. 4, Iˆ is bijective. Furthermore, let τ1 , τ2 ∈ T+ then:ˆ 1 ./ τ2 ) = I(τˆ 1 ) · 2 · I(τˆ 2 ).
I(τHaving the core encoding function Iˆ defined, it is now routine to establish
the isomorphism from the tree structure B + to the string structure S 0 :Lemma 8. Let f be a function that maps the tree structure hT+ ,τ ./, ./τ i into
the string structure h{0, 1, 2}, Ps2 , S2s i such that:defˆ ).
1. For each tree τ ∈ T+ , we let f (τ ) = I(τdef

2. For each function τ ./, we let f (τ ./) = PI(τˆ )2 .
def

3. For each function ./τ , we let f (./τ ) = S2I(τˆ ).
Then f is an isomorphism from B + to S 0 .
Proof of Lemma 5. For the upper bound, observe that the function f inLemma 8 can be used to transform tree share formulae in B + to string formulae
in S 0 . It remains to ensure that the size of the string formula is not exponentiallyexploded. In particular, it suffices to construct Iˆ such that if a tree τ ∈ T+ˆ ) has linear size O(n). Recall that Iˆ is
has size n, its corresponding string I(τextended from I which can be constructed in many different ways. Thus to
avoid the size explosion, we choose to specify the encoding function I on the
fly after observing the input tree share formula. To be precise, given a formulaΦ in B, we first factorize all its tree constants into prime trees, which can bedone in log-space [27]. Suppose the formula has n prime trees {τi }ni=1 sorted inthe ascending order of their sizes, we choose the most efficient binary encoding
by letting I(τi ) = si where si is the ith string in length-lexicographic (shortlex)order of {0, 1}∗ ,i.e. {, 0, 1, 00, 01, . . .}. This encoding ensures that the size of τiand the length of si only differ by a constant factor. Given thethat a tree
Pn fact
ˆ i )) bits toshare in its factorized form τ1 ./ . . . ./ τn only requires O( i=1 I(τˆ ) also
represent, we infer that its size and the length of its string counterpart I(τdiffer by a constant factor. Hence, the upper bound complexity is justified.
To prove the lower bound, we need to construct the inverse function f −1that maps the string structure S 0 into the tree share structure B. Although theexistence of f −1 is guaranteed since f is isomorphism, we also need to take careof the size explosion problem. It boils down to construct an efficient mapping
I −1 from binary strings to prime trees by observing the input string formula Φ.
For each string constant s1 2 . . . 2sn in Φ where si ∈ {0, 1}∗ , we extract all of
the binary strings si . We then maps each distinct binary string si to a uniqueprime tree τi as follows. Let k(0) = • ◦, k(1) = ◦ • and assume si = a0 . . . am forai ∈ {0, 1}, we compute τ = k(a0 ) ./ . . . ./ k(am ). Then the mapped tree sharefor the string si is constructed as τi = • τ (if si =  then τi = • ◦ ). It follows
that τi is prime and this skewed tree has size O(n) where n is the length of si .
Thus the result follows.
tu
Example 2. Consider the tree formula ∀a∃b∃c. a = b ./ ◦ • ◦ ∧ b = ◦ • ◦ ./ c.
This formula contains two constants whose factorizations are below:
c1 = ◦ • ◦ = • ◦ ./ ◦ •c2 = ◦ • ◦ = ◦ • ./ • ◦ .

We choose I such that I(• ◦) =  and I(◦ •) = 0. Our encoding gives s1 = 20
and s2 = 02. This results in the string formula ∀a∃b∃c. a = S220 (b) ∧ b = P022 (c)whose explicit form is ∀a∃b∃c. a = b220 ∧ b = 022c.
Now suppose that we want to transform the above string formula into equivalent tree formula. Following the proof of Lemma 5, we extract from the formula
two binary strings s1 =  and s2 = 0 which are mapped to the prime trees
τ1 = • ◦ and τ2 = • • ◦ respectively. Hence the equivalent tree share formulais ∀a∃b∃c.a =./τ1 ./τ2 (b) ∧ b =τ2 ./τ1 ./ (c). It is worth noticing the difference
between this tree formula and the original tree formula, which suggests the factthat the representation of the alphabet (i.e. prime trees) is not important.
5.2

Combined C formulae in practiceThe source of the nonelementary behavior comes from two factors. First, as
proven just above, it comes from the combination of both the additive andmultiplicative operations of tree shares. Second, it comes from the number ofquantifier alternations in the formula being analyzed, due to the encoding of C
in tree automata [27] and the resulting upper bound (the transformed automata
of first-order formulae of tree automatic structures have sizes bounded by a towerof exponentials whose height is the number of quantifier alternations [6, 5]).

Happily, in typical verifications, especially in highly-automated verifications
such as those done by tools like HIP/SLEEK [28], the number of quantifier alternations in formulae is small, even when carrying out complex verifications or inference. For example, consider the following biabduction problem (a separationlogic-based inference procedure) handled by the ShareInfer tool from [26]:πa 7→ (b, c, d) ? • ◦ · π · tree(c) ? ◦ • · π · tree(d) ? [??] ` • ◦ · π · tree(a) ? [??]
π ./ ◦ •ShareInfer will calculate • ◦ · π · tree(d) for the antiframe and a 7−−−−−→ (b, c, d) ?
◦ • · π · tree(d) for the inference frame. Although these guesses are a bit sophisticated, verifing them depends on [16] the following quantifier-alternation-free
C sentence: ∀π, π 0 . π = π 0 ⇒ ./(π)⊕ ./(π) = π 0 . Even with com•◦•◦plex loop invariants, more than one alternation would be surprising because e.g.
verification tools tend to maintain formulae in well-chosen canonical forms.
Moreover, because tree automata are closely connected to other well-studied
domains, we can take advantage of existing tools such as MONA [23]. As anexperiment we have hand-translated C formulae into WS2S, the language of
MONA, using the techniques of [10]. The technical details of the translation areprovided in appendix §A. For the above formula, MONA reported 205 DAG hits
and 145 nodes, with essentially a 0ms running time.
Lastly, heuristics are well-justified both because of the restricted problem
formats we expect in practice as well as because of the nonelementary worstcase lower bound we proved in §4, opening the door to newer techniques likeantichain/simulation [1].

6

Future work and conclusion

We have developed a tighter understanding of the complexity of the tree share
O(1)model. As Boolean Algebras, their first-order theory is STA(∗, 2n, n)-complete,even with arbitrary tree constants in the formulas. Although the first-order theory over tree multiplication is undecidable [27], we have found that by restricting
multiplication to be by a constant (on both the left τ./ and right ./τ sides) we
obtain a substructure B whose first-order theory is STA(∗, 2O(n) , n)-complete.
Accordingly, we have two structures whose first-order theory has elementarycomplexity. Interestingly, their combined theory is still decidable but nonelementary, even if we only allow multiplication by a constant on the right ./τ .
We have several directions for future work. It is natural to investigate theprecise complexity of the existential theory with the Boolean operators and rightsided multiplication ./τ (structure C). The encoding into tree-automatic structures from [27] provides only an exponential-time upper bound (because of theresult for the corresponding fragment in tree-automatic structures, e.g., see [36]),
and there is the obvious NP lower bound that comes from propositional logic
satisfiability. We do not know if the Boolean operators (t, u,¯·) in combination

with the left-sided multiplication τ./ is decidable (existential or first order, withor without the right-sided multiplication ./τ ). Determining if the existential theory with the Boolean operators and unrestricted multiplication ./ is decidable
also seems challenging. We would also like to know if the monadic second-ordertheory over these structures is decidable.
Acknowledgement. We would like to thank anonymous referees for their constructive reviews. Le and Lin are partially supported by the European ResearchCouncil (ERC) under the European Unions Horizon 2020 research and innovation programme (grant agreement no 759969). Le and Hobor are partially
supported under Yale-NUS College grant R-607-265-322-121.

References
1. Parosh Aziz Abdulla, Yu-Fang Chen, Lukás Holı́k, Richard Mayr, and Tomás Vojnar. When simulation meets antichains. In TACAS, pages 158–174, 2010.
2. A. W. Appel, R. Dockins, A. Hobor, L. Beringer, J. Dodds, G. Stewart, S. Blazy,and X. Leroy. Program Logics for Certified Compilers. Cambridge U. Press, 2014.
3. Andrew W. Appel, Robert Dockins, and Aquinas Hobor. Mechanized semantic
library, 2009.
4. Leonard Berman. The complexity of logical theories. Theoretical Computer Science, 11(1):71–77, May 1980.
5. A. Blumensath. Automatic Structures. PhD thesis, RWTH Aachen, 1999.
6. A. Blumensath and E. Grade. Finite presentations of infinite structures: automata
and interpretations. In Theory of Computer Systems, pages 641–674, 2004.
7. Richard Bornat, Cristiano Calcagno, Peter O’H, and Matthew Parkinson. Permission accounting in separation logic. In POPL, pages 259–270, 2005.
8. John Boyland. Checking interference with fractional permissions. In SAS, pages
55–72, 2003.
9. Ashok K. Chandra, Dexter C. Kozen, and Larry J. Stockmeyer. Alternation. J.
ACM, 28(1):114–133, January 1981.
10. Thomas Colcombet and Christof Löding. Transforming structures by set interpretations. Logical Methods in Computer Science, 3(2), 2007.
11. K. J. Compton and C. W. Henson. A uniform method for proving lower bounds
on the computational complexity of logical theories. APAL 1990.
12. The Coq development team. The Coq proof assistant reference manual. LogiCal
Project, 2004. Version 8.0.
13. Robert Dockins, Aquinas Hobor, and Andrew W. Appel. A fresh look at separation
algebras and share accounting. In APLAS, pages 161–177, 2009.
14. J. Dohrau, A. J. Summers, C. Urban, S. Münger, and P. Müller. Permission
inference for array programs. In CAV, 2018.
15. Marko Doko and Viktor Vafeiadis. Tackling real-life relaxed concurrency with
FSL++. In ESOP, pages 448–475, 2017.
16. Cristian A. Gherghina. Efficiently Verifying Programs with Rich Control Flows.
PhD thesis, National University of Singapore, 2012.
17. Erich Grädel. Simple interpretations among complicated theories. Information
Processing Letters, 35(5):235 – 238, 1990.
18. Hobor and Cristian Gherghina. Barriers in concurrent separation logic. In ESOP,
pages 276–296, 2011.

19. Aquinas Hobor. Oracle Semantics. PhD thesis, Princeton University, Departmentof Computer Science, Princeton, NJ, October 2008.
20. Aquinas Hobor and Cristian Gherghina. Barriers in concurrent separation logic:
Now with tool support! Logical Methods in Computer Science, 8(2), 2012.
21. Sanjay Jain, Bakhadyr Khoussainov, Frank Stephan, Dan Teng, and Siyuan Zou.
Semiautomatic structures. In CSR, pages 204–217, 2014.
22. Artur Jez. Recompression: A simple and powerful technique for word equations.
J. ACM, 63(1):4:1–4:51, 2016.
23. Nils Klarlund and Anders Møller. MONA Version 1.4 User Manual. BRICS,
Department of Computer Science, Aarhus University, January 2001.
24. Duy-Khanh Le, Wei-Ngan Chin, and Yong Meng Teo. Threads as resource for
concurrency verification. In PEPM, pages 73–84, 2015.
25. Xuan-Bach Le, Cristian Gherghina, and Aquinas Hobor. Decision procedures oversophisticated fractional permissions. In APLAS, 2012.
26. Xuan-Bach Le and Aquinas Hobor. Logical reasoning over disjoint fractional permissions. In ESOP, 2018.
27. Xuan-Bach Le, Aquinas Hobor, and Anthony W. Lin. Decidability and complexityof tree shares formulas. In FSTTCS, 2016.
28. Xuan-Bach Le, Thanh-Toan Nguyen, Aquinas Hobor, and Wei-Ngan Chin. A
certified decision procedure for tree shares. In ICFEM, 2017.
29. G. S Makanin. The problem of solvability of equations in a free semigroup. In
Mat. Sbornik, pages 147–236, 1977.
30. Kim Marriott and Martin Odersky. Negative boolean constraints. In TheoreticalComputer Science 160, pages 365–380, 1996.
31. Peter W. OHearn. Resources, concurrency, and local reasoning. Theor. Comput.
Sci., 375(1-3):271–307, April 2007.
32. Matthew Parkinson. Local Reasoning for Java. PhD thesis, University of Cambridge, 2005.
33. Matthew J. Parkinson, Richard Bornat, and Peter W. O’Hearn. Modular verification of a non-blocking stack. In POPL 2007, pages 297–302, 2007.
34. Tatiana Rybina and Andrei Voronkov. Upper bounds for a theory of queues. In
ICALP, pages 714–724, 2003.
35. L. Stockmeyer. The complexity of decision problems in automata theory and logic.
PhD thesis, M.I.T., 1974.
36. A. W. To. Model Checking Infinite-State Systems: Generic and Specific Approaches.
PhD thesis, LFCS, School of Informatics, University of Edinburgh, 2010.
37. Jules Villard. Heaps and Hops. Ph.D. thesis, Laboratoire Spécification etVérification, École Normale Supérieure de Cachan, France, February 2011.
38. T.D. Young, P.R. Pinto, K.J. Andersen, and L. Birkedal. Caper: Automatic verification for fine-grained concurrency. In ESOP 2017, 2017.

A

Appendix

Fig. 1 contains the MONA WS2S encoding of the following tree share formula∀π, π 0 . π = π 0 ⇒ (π ./ ◦ •) ⊕ (π ./ • ◦) = π 0 .
where lower case letters are for variables of binary strings and upper case letters are for second-order monadic predicates. The last three lines in the code

ws2s;
pred ant(var2 Y) =all1 x,y: (x~=y & x in Y & y in Y) => (~(x<=y) & ~(y<=x));
pred maxt(var2 X,var2 Y) =X sub Y & ex1 r:all1 x: x in X =>(r <= x & all1 z: r <= z => ex1 x’: x’ in X & (z <= x’ | x’ <= z));pred roott(var1 x,var2 X) =all1 y: y in X & x <= y & all1 z:all1 y’:y’ in X & z <= y’ => x <= z;pred subt(var2 X, var2 Y) =all1 x1:all2 X’:(maxt(X’,X) & roott(x1,X’)) =>(ex2 Y’:maxt(Y’,Y) => roott(x1,Y’));
pred eqt(var2 X, var2 Y) =subt(X,Y) & subt(Y,X);
pred singleton(var2 X) =ex1 x: x in X & (all1 y: y in X => x = y);pred uniont(var2 X,var2 Y,var2 Z) =Z = X union Y & empty(X inter Y);
pred mint(var2 X) =all2 Y: maxt(Y,X) => singleton(Y);pred sub0(var2 X, var2 X0) =all1 x:x in X <=> x.0 in X0;
pred sub1(var2 X, var2 X0) =all1 x:x in X <=> x.1 in X0;
pred leftMul(var2 X,var2 X’) =all2 Y:(eqt(X,Y) & mint(Y)) => sub0(Y,X’);pred rightMul(var2 X,var2 X’) =all2 Y:(eqt(X,Y) & mint(Y)) => sub1(Y,X’);all2 X,X’,XL,XR,XU:(ant(X) & ant(X’) & ant(XL) & ant(XR) & ant(XU) & eqt(X,X’) &leftMul(X,XL) & rightMul(X,XR) & uniont(XL,XR,XU)) => (eqt(XU,X’));Fig. 1. The transformation of tree share formula in §5.2 into equivalent WS2S formula.

are the formulas with a number of macros defined in the previous lines. Essentially, each tree share is represented by a second-order variable whose elements
are antichains that describes a single path to one of its black leaves. Roughly
speaking, the eqt predicate checks whether two tree shares are equal, leftMuland ./
respecand rightMul correspond to the multiplicative predicates ./•◦◦•tively, and uniont computes the additive operator ⊕. Other additional predicates are necessary for the consistent representation of the tree shares. In detail,singleton(X) means that X has exactly one element, ant makes sure any two
antichains in the same tree are neither prefix of the other, maxt(X,Y) enforcesthat X is the maximal antichain of Y, roott(x,X) asserts x is the root of X,
subt is a subset-like relation betweens two trees, while mint specifies the canonical form. Lastly, we have sub0 and sub1 as the intermediate predicates for themultiplicative predicates.