Decidability and Complexity of Tree Share
FormulasXuan Bach Le1 , Aquinas Hobor2 , and Anthony W. Lin3
1
2
3

School of Computing, National University of Singapore
lxbach@comp.nus.edu.sg
Yale-NUS College and School of Computing, National University of Singapore
hobor@comp.nus.edu.sg
Yale-NUS College
anthony.w.lin@yale-nus.edu.sg

Abstract
Fractional share models are used to reason about how multiple actors share ownership of resources.
We examine the decidability and complexity of reasoning over the “tree share” model of Dockins
et al. using first-order logic, or fragments thereof. We pinpoint a connection between the basic
operations on trees union t, intersection u, and complement  and countable atomless Boolean
algebras, allowing us to obtain decidability with the precise complexity of both first-order andexistential theories over the tree share model with the aforementioned operations. We establish
a connection between the multiplication operation ./ on trees and the theory of word equations,allowing us to derive the decidability of its existential theory and the undecidability of its full
first-order theory. We prove that the full first-order theory over the model with both the Boolean
operations (t, u, ) and the restricted multiplication operation (./ with constants on the righthand side) is decidable via an embedding to tree-automatic structures.
1998 ACM Subject Classification F.1.1 Models of Computation, F.3.1 Specifying and Verifying
and Reasoning about Programs, F.4.1 Mathematical Logic, F.4.3 Formal Languages
Keywords and phrases Fractional Share Models, Resource Accounting, Countable Atomless
Boolean Algebras, Word Equations, Tree Automatic Structures
Digital Object Identifier 10.4230/LIPIcs.FSTTCS.2016.

1

Introduction

The state of the art: Fractional shares enable reasoning about shared ownership ofresources between multiple parties, e.g. ownership of memory cells by different threads in a
concurrent program [7]. Threads are then allowed to take actions depending on the amountof ownership they have, e.g. with full ownership allowing both reading and writing, partial
ownership allowing only reading, and empty ownership allowing nothing. Although rational
numbers are the most obvious model for fractional shares, they are unfortunately not a goodmodel for realistic program verification because they do not satisfy the so-called “disjointness”
axiom [3], i.e. ∀x, y. x + x = y ⇒ x = y = 0. Dockins et al. proposed a better model
for fractional shares based on binary trees with Boolean leaves [10]. A tree share τ ∈ T is
inductively defined as follows: τ , ◦ | • | τ τ , where ◦ denotes an “empty” leaf while •a “full” leaf. The tree ◦ is thus the empty share, and • the full share. There are two “half”
shares: ◦ • and • ◦, and four “quarter” shares, beginning with. It is a feature•◦◦that the two half shares in T are distinct, as compared to the two half shares in Q, 0.5 and 0.5,
© X. Bach Le, Aquinas Hobor, and Anthony W. Lin;
licensed under Creative Commons License CC-BY
36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science(FSTTCS 2016).
Editors: Akash Lal, S. Akshay, Saket Saurabh, and Sandeep Sen; Article No. ; pp. :1–:14Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

XX:2

Decidability and Complexity of Tree Share Formulas

which are of course equal. The ability to represent distinct partial shares of “equal measure”
is closely related to why the disjointness axiom holds. The basic operations for combining
trees are union t, intersection u, and complement ; these will be defined formally in §2.
=
but to a first approximation they are all defined leafwise, e.g. ◦ • t
•

◦

◦

•

◦

•

A number of program logics incorporate tree shares to model fractional ownership [11, 12,29, 3], but it has been unclear how to reason about them automatically, which has posed asignificant barrier to their use in verification tools. One reason for this barrier is the lack offoundational results regarding decidability and complexity of theories over tree shares. The
only published result of this kind proves the decidability of entailment between systems ofequations over tree shares, a less-expressive format than general first-order formulae [19].
In addition to union, intersection, and complement, Dockins et al. defined a “multiplication” operator on tree shares, written τ1 ./ τ2 [10]. The basic idea is that you take each • leafin τ1 and replace it with a full copy of τ2 , e.g.
./ ◦ • =
.
•

◦

◦

•

◦

•

◦

◦

◦

•

Dockins et al. showed that ./ could be used to split any nonempty tree τ into two nonempty
trees that joined together to equal the original since ∀τ. τ = (τ ./ • ◦) t (τ ./ ◦ •). Moregenerally, the ./ operator can be used as a kind of “scoping” or “gluing” operator to combine
different uses of tree shares together. Although ./ has been used in metatheory [3], it has
never been used in an automated tool because its decidability properties were unclear.
Contributions: In this paper, we provide the first systematic study of decidability andcomplexity of theories over the tree share model.
First (§3), we show that the tree share model M , (u, t, , ◦, •) is a Countable Atomless
Boolean Algebra (CABA), which are known to be unique up to isomorphism [28]. The
first-order theory over CABAs is known to be decidable and, in fact, complete for the class
STA(∗, 2cn , n) of problems solvable by an alternating Turing machine with n alternations in
exponential time [17], the same complexity class as the first-order theory over (R, +, 0, 1) [4].
In addition, the full existential theory over CABAs is known to be NP-complete [24]. Ourconnection shows that these decidability and complexity results transfer to M.
We then (§4) proceed to decision problems over the tree shares with the multiplication
operator ./. Our main result here is that the tree share model S , (T, ./) that only allows ./(i.e. but not t, u, and ) is—in a technical sense—“equivalent” to the logical structure ofwords with the concatenation operator. Makanin [20] showed that reasoning about a single
equation over this structure (a.k.a. word equations) is decidable. More complex problems
are known to be reducible to this basic case in polynomial-time, e.g. the existential theory
over the structure [8]. Accordingly, we deduce that the existential theory over S is decidable
in polynomial space but NP-hard, whereas the first-order theory over S is undecidable.
Finally (§5), we consider restrictions on ./ that admit a decidable theory. We define
the family of one-argument functions indexed by tree constants that applies bowtie on
the right-hand side ./ , i.e. ./τ (τ 0 ) , τ 0 ./ τ . We prove that the combined theory ofT , (T, u, t, , ./ ) has an embedding into tree-automatic structures. Since the firstorder theory of tree-automatic structures is decidable [6], we obtain the decidability of thefirst-order theory of this extension of the tree share model with ./ . This suggests thepotential application of powerful heuristics for automata (e.g. antichain and simulation [1])for providing a practical decision procedure for the tree share model.

X. Bach Le, Aquinas Hobor, and Anthony W. Lin

2

XX:3

Formal preliminaries: the Tree Share model T of Dockins et al. [10]Here we summarize additional details of tree shares and their associated theory from [10].
Canonical forms. In the first paragraph of §1 we presented the first quarter share as
instead of e.g.
. This is deliberate: the second choice is not a valid
•

◦

◦

•

◦

◦

◦

share because the tree is not in canonical form. A tree is in canonical form when it is in its
most compact representation under the inductively-defined equivalence relation ∼
=:
τ1 ∼
= τ10
◦∼
=◦

•∼
=•

◦∼
=◦

•∼
=•

◦

•

τ1

τ2

τ2 ∼
= τ20
∼
= τ0

1

τ20

As we will see, operations on tree shares sometimes need to fold/unfold trees to/from canonicalform, a practice we will indicate using the symbol ∼=. Canonicality is needed to guarantee
some of the algebraic properties of tree shares; managing it requires a little care in the proofs
but does not pose any fundamental difficulties to the overall theory.
Boolean algebra operations. The connectives t and u first unfold both trees to thesame shape; then calculate leafwise using the rules ◦ t τ = τ t ◦ = τ , • t τ = τ t • = •,◦ u τ = τ u ◦ = ◦, and • u τ = τ u • = τ ; and finally refold back into canonical form, e.g:
•

•

◦

◦

◦

◦

∼
=

t
◦

•

•

◦

t
•

◦

◦

◦

∼
=

u
◦

•

•

◦

◦

•

•

◦

u
•

◦

◦

◦

∼
=

=
•

•

•

◦

∼
=

=
◦

•

•

◦

◦

◦

◦

•

•

◦

◦

◦

Complementation is simpler, since flipping leaves between ◦ and • does not affect whether atree is in canonical form, e.g.:=. Using these definitions we get all of
•

◦

◦

◦

•

•

the usual properties for Boolean algebras, e.g. τ1 u τ2 = τ1 t τ2 . Moreover, we can define apartial ordering between trees using intersection in the usual way, i.e. τ1 v τ2 , τ1 u τ2 = τ1 .
We can enjoy a strict partial order as well: τ1 @ τ2 , τ1 v τ2 ∧ τ1 6= τ2 .
Properties of tree multiplication ./. Since it is nonstandard, the “tree multiplication”
operator ./ deserves some additional attention. The good news first: ./ is associative, has an
identity •, and is injective for non-◦ elements, i.e. S + , (T \ {◦}, ./) forms a cancellative
monoid. Somewhat unsurprisingly, multiplication by the “additive identity” ◦ reduces to ◦.
Unfortunately, ./ is not commutative (• ◦ ./ ◦ • =6== ◦ • ./ • ◦),
◦

•

◦

◦

•

◦

although we do enjoy a distributive property over t and u on the right hand side. Accordingly:
I Lemma 1 (Properties of ./).
Associativity :τ1 ./ (τ2 ./ τ3 ) = (τ1 ./ τ2 ) ./ τ3(1)

Identity element :τ ./ • = • ./ τ = τ(2)Zero element :τ ./ ◦ = ◦ ./ τ = ◦(3)

Left cancellation :τ 6= ◦ ⇒ τ ./ τ1 = τ ./ τ2 ⇒ τ1 = τ2

(4)

Right cancellation :τ 6= ◦ ⇒ τ1 ./ τ = τ2 ./ τ ⇒ τ1 = τ2

(5)
(6)

Typical use of T in program verification. A standard way to use fractional shares inprogram verification is by modifying the standard maps-to predicate of separation logic to

FSTTCS 2016

XX:4

Decidability and Complexity of Tree Share Formulasπtake a share as an additional argument. The predicate x 7→ y then means that the heap hasa cell at address x, which is owned with nonempty fraction π 6= ◦ and whose value is y. We
use π here because we often use share variables rather than concrete trees τ .
To combine divided fractional ownership stakes back together it is traditional to use the“join” relation, written τ1 ⊕ τ2 = τ3 . The join relation is defined in turn using the primitive
Boolean algebra operators: τ1 ⊕ τ2 = τ3 , τ1 t τ2 = τ3 ∧ τ1 u τ2 = ◦. In other words, the join
relation is a kind of disjoint union; it is partial because e.g. • ⊕ • is undefined. Critically forverification ⊕ does satisfy the disjointness axiom: ∀x, y. x ⊕ x = y ⇒ x = y = ◦. Using ⊕we can state the following relationship between the spatial conjunction ∗ and the underlyingππ
π1 ⊕π2
Boolean operators as x 7→1 y ∗ x 7→2 z a` y = z ∧ x 7−
→ y ( using a` for bientailment).
It is common that we want to “split” a share π into sub-shares π1 , π2 so that the permission
can be transferred. This can be done within M , (u, t, , ◦, •) using the following rule:
π 6= ◦ππ1

πx 7→ v a` ∃π1 , π2 . (x 7→ v ∗ x 7→2 v) ∧ π1 ⊕ π2 = π ∧ π1 6= ◦ ∧ π2 6= ◦SplitJoin

This rule has some drawbacks. The most obvious is the lengthy size of the entailment’s
consequent, even though we only split π into two pieces. Second, existential quantifiers are
expensive in program verification since they tend to increase the size of the proof obligations
and here we introduce two of them. Third, we have no control over what the shares π1 andπ2 are—that is, π1 and π2 are not uniquely determined. Moreover, they are indistinguishable,
which makes it difficult to assign different permitted actions for them.
On the other hand, each of these issues can be solved nicely using ./ due to its right
distributivity over (u, t), and thus over ⊕, yielding the following rules:
τ1 ⊕ . . . ⊕ τn = τn^π 6= ◦

τi 6= ◦
i=1
π./τn

π./τ

π./τ

x 7−→ v a` x 7−→1 v ∗ . . . ∗ x 7−→ v

3SplitJoin ./(7)

Tree Shares are a model for Countable Atomless Boolean Algebras

In this section, we pinpoint the fact that M = (u, t, , ◦, •) is a model for Countable Atomless
Boolean Algebra (CABA). Let B = (∩, ∪, , 0, 1) be a Boolean Algebra (BA), we define apartial order ⊆ on B (v for M, resp.): a1 ⊆ a2 , a1 ∩a2 = 0 and a1 ⊂ a2 , a1 ⊆ a2 ∧a2 6⊆ a1 .
B is atomless if ∀a. 0 ⊂ a ⇒ ∃a0 . 0 ⊂ a0 ⊂ a. B is countable if its domain is countable.
Dockins et al. [10] proved that M is a model for BA where 0 , ◦, 1 , •, t , ∪, u , ∩. The
atomless property can be derived from the Infinite Splitability property of tree shares [19]:let a A ◦ and a1 , a2 6= ◦ such that a1 ⊕ a2 = a. This implies a1 t a2 = a ∧ a1 u a2 = ◦. By
Stone’s representation theorem each BA is isomorphic to a BA of powerset, thus a1 t a2 = a
implies a1 ⊆ a and a2 ⊆ a. Suppose that a1 = a then a2 u a = 0 which is a contradiction
because 0 @ a2 @ a. As a result, a1 =6 a and thus a1 @ a. The proof that T is countable isachieved by enumerating T in the ascending order of tree height |τ | using the following total
strict order ≺:|τ1 | < |τ2 |◦≺•τ1 ≺ τ2

|

τ1

τ10

|=|

τ1

τ2

τ10

≺

τ20
τ2

| τ1 ≺ τ2
τ20

|τ

τ1

| = |τ

τ

τ1

τ2

≺τ

| τ1 ≺ τ2
τ2

It is known that there is a unique model for CABA up to isomorphism [28], so we canreason about the complexity of M in terms of CABA. Let STA(f (n), g(n), h(n)) be theX. Bach Le, Aquinas Hobor, and Anthony W. Lin

XX:5class of sets accepted by alternating Turing machines which use at most f (n) space, g(n)time and h(n) alternations between universal and existential states on a given input oflength n. Any field in the description can be replaced with symbol ∗ to indicate no bound isrequired. Kozen [17] proved that the elementary theory of infinite BAs is ≤log -complete for theS
Berman complexity class c<ω STA(∗, 2cn , n), which lies between the class of deterministic
exponential space and non-deterministic exponential space.
We now investigate the complexity of an important sub-theory of M, namely the existential
theory. Basically, this sub-theory includes all valid sentences whose prenex normal form
contains only existential quantifiers. Its counterpart is the universal theory in which all thequantifiers are universal. A result by Marriott et al. [24] showed that the existential theory
and universal theory for infinite BAs are in NP-complete and co-NP-complete respectively.

4

Decidability of general multiplication ./ over Tree Shares

In this section, we will prove the following results about S = (T, ./):I Theorem 2 (Complexity of S).
1. The existential theory of S is decidable in PSPACE.
2. The existential theory of S is NP-hard.
3. The general first-order theory over S is undecidable.
The proof of Theorem 2 largely rests on the identical conclusions for the key subtheory
S + , (T+ , ./), where T+ , T \ {◦} are the “positive trees” obtained by removing the “zeroelement” ◦ from T:
I Lemma 3 (Complexity of S + ).
1. The existential theory of S + is decidable in PSPACE.
2. The existential theory of S + is NP-hard.
3. The general first-order theory over S + is undecidable.
We will prove Lemma 3 shortly, but first let us use it to polish off Theorem 2:
Proof of Theorem 2. We take each part in turn as follows:
1. Represent the set of variables V = {x1 , . . . , xn } in a given formula F of S as a n-length
bitvector. We can enumerate through all possibilities P1 , . . . , P2n for this vector using
linear space and binary addition. For each possibility Pj , variable xi ’s bit is 0 to indicatethat xi must be ◦ and 1 when xi must be non-◦. For each xk that is marked as ◦, wesubstitute ◦ for xk in F to reach Fj and simplify using the rules
π1 ./ ◦ = π2

◦ ./ π1 = π2

π1 ./ π2 = ◦π2 = ◦

π2 = ◦

π1 = ◦ ∨ π2 = ◦π1 ./ ◦ =6 π2◦ ./ π1 6= π2

π1 ./ π2 6= ◦π2 6= ◦

π2 6= ◦

π1 6= ◦ ∧ π2 6= ◦We can then just check to make sure that the resulting “fresh” (in)equalities are consistent
with the current value of the bitvector Pj . If not, we have reached a contradiction andcan proceed to the next bitvector Pj+1 . If so, then after removing the trivial equalities(e.g. ◦ = ◦) from Fj we are left with an equivalent formula Fj+ which is in S + , so

FSTTCS 2016

XX:6

Decidability and Complexity of Tree Share Formulas

by Lemma 3.1 we can check if Fj is satisfiable in PSPACE. If so, we know that Fj issatisfiable, and thus that F is satisfiable. If not, we proceed to the next bitvector Pj+1 ;if all Fj are unsatisfiable then F is unsatisfiable.
++
2. By Lemma 3.2 it is sufficient to reduce a formulaF in S to S. Let V be the set ofVvariables in F + and define F , F + ∧x 6= ◦ ; note that we construct F in linearx∈Vtime from |F + |. F is satisfiable in S if and only if F + is satisfiable in S + , so we are done.
3. Any extension of an undecidable theory is also undecidable; by Lemma 3.3 we are done.
J

4.1

Word equations

To prove Lemma 3 we will show that S + is isomorphic to the theory of word equations. Let
us recall this theory. Let A = {a1 , a2 , . . .} be a finite set of letters and • be a concatenation
operator that combines letters into words. Let A∗ be the Kleene closure of A using •. We
define a model for the alphabet A, written WA as the pair (A∗ , •). Now let V = {v1 , v2 , . . .}be a finite set of variables, and w ∈ W , (A ∪ V )∗ a finitely generated word that includes
both letters and variables. We extend a word context ρ : V → A∗ to the domain A ∪ V bymapping constants to themselves, and further to the domain W by replacing each letter
within a word with its value in ρ. A word equation EW is a pair of words (w1 , w2 ) ∈ W × W.
We say that ρ is a solution of EW if ρ(w1 ) = ρ(w2 ).
The satisfiability of word equation asks whether a word equation EW has a solution ρ,
denoted SATW (EW ). Makanin proposed a complete treatment to this problem in a seriesof papers [20, 21, 22] but his method was highly intractable (quadruple-exponential nondeterministic time [16]). Substantial research since has improved this bound, e.g. [2, 13].
The best known complexity bound for this problem is PSPACE and NP-hard [25, 26] and it
is hypothesized to be NP-complete. Importantly for our present result, the existential theory
over word equations is known to be reducible to SATW in polynomial time [8]. Finally, thefirst order theory over W is known to be undecidable [23, 18].
Infinite alphabets. To define our isomorphism from T+ to A∗ it will be convenient if
the alphabet A can be countably infinite. Accordingly, we must reduce word equations
over an infinite alphabet to the standard finite case. Let σ : W → P(A) be the functionthat extracts the set of letters from a word w, e.g. σ(v1 a1 a3 v2 ) = {a1 , a3 } and extend σ to
W × W by σ(w1 , w2 ) = σ(w1 ) ∪ σ(w2 ). Let φ : W × P(A) → W be the projection functionthat takes a word w and a set of letters B ⊆ A and removes all letters in w that are notin B, e.g. φ(v1 a1 a3 v2 , {a1 , a2 }) = v1 a1 v2 . It is not hard to prove that φ with fixed B is anhomomorphism over WA . Now we are ready to state and prove the extension to infinite
alphabets:
I Lemma 4 (Infinite alphabet word equations). Let A be infinite and EW = (w1 , w2 ) a word
equation over A. EW is satisfiable in WA iff EW is satisfiable in Wσ(EW ) .
Proof. ⇐ is trivial. Let ρ : V → A∗ be a solution of EW over A and ρ0 = λv. φ(ρ(v), σ(EW )).
Notice ρ0 preserves all the letters in EW and ρ(w1 ) = ρ(w2 ) implies ρ0 (w1 ) = ρ0 (w2 ). Thus ρ0
is a new solution of EW that only contains letters from σ(EW ).
J

4.2

Finding an infinite alphabet inside T+

Since ./ is a kind of multiplication operation, and the fundamental building blocks of (N, ×)
are prime numbers, it is natural to wonder whether there is an analogue on trees. There is:X. Bach Le, Aquinas Hobor, and Anthony W. Lin

XX:7

I Definition 5 (Prime trees). τ ∈ T+ \{•} is prime if ∀τ1 , τ2 . τ = τ1 ./ τ2 ⇒ (τ1 = • ∨ τ2 = •).
Furthermore, let Prime(τ ) indicate τ is prime and Tp be the set of all prime trees.
Examples of tree primes are ◦• andis not prime since it can be factored as •. On the other hand, the tree•◦•

◦ ./ ◦◦◦•◦•. Prime trees have many nice properties:

I Lemma 6 (Properties of prime trees).
1. There are countably infinitely many prime trees.
2. Let τ1 , τ10 , τ2 , τ20 ∈ Tp , τ1 ./ τ2 = τ10 ./ τ20 iff τ1 = τ10 and τ2 = τ20 .
3. Given two prime tree sequences S1 = τ11 , . . . , τ1k1 and S2 = τ21 , . . . , τ2k2 , S1 = S2 iff their
Vk1 i
1
2
./ products are equal: ./ki=1
τ1i = ./ki=1
τ2i ⇔ (k1 = k2 i=1
τ1 = τ2i ).
To prove Lemma 6 we must define the notation |τ | to be the height of τ (with |◦| = |•| = 0
and counting up from there). Given this notation it is simple to define the set of all trees up
to height n, written Tn . We will also need the following technical lemma which allows us to
split an application of bowtie τ2 ./ τ3 to children of τ2 :I Lemma 7 (Split for ./). Let τ1 , τ2 , τ3 , τ1l , τ1r ∈ T+ and τ1 = τ2 ./ τ3 ∧ τ1 =either (1) τ2 = • ∧ τ1 = τ3 or (2) ∃τ2l , τ2r . τ2 =

τ2l

τ2r

τ1l

τ1r

then

∧ τ1l = τ2l ./ τ3 ∧ τ1r = τ2r ./ τ3 .

Proof. The case τ2 = • is trivial. Otherwise, there exists τ2l , τ2r ∈ T such that τ2 =

τ2l

τ2r

.

By definition of ./, τ1 = τ2 ./ τ3 is computed by replacing each leaf • in τ2 with τ3 ,which is equivalent to replace each leaf • in τ2l and τ2r with τ3 . Thus, τ1l = τ2l ./ τ3 andτ1r = τ2r ./ τ3 .
J
Proof of Lemma 6.
1. We construct an infinite sequence S of prime trees: let p1 , •

S

,





•




◦,

•

◦

•

,
•

◦

•

◦, pj , pj−1•

, i.e.





,...

•



It is immediate that p1 is prime. To prove that pi is prime for i > 1, we proceed asfollows. Suppose pi = τ1 ./ τ2 and neither τ1 nor τ2 is •. The right subtree of each pi
is just • and by the definition of ./ must contain a copy of τ2 , i.e. τ2 = •, so we have acontradiction and pi is prime.
2. We prove by induction on the height of τ1 , τ10 . The base case T0 is easy to verify. Assume0
it holds for Tk and τ1 , τ10 ∈ Tk+1 . Let τ1 = l
r , τ1 =l0
r 0 then by Lemma
τ1007, we derive τ1l ./ τ2 = τ1l ./ τ20 , τ1r ./ τ2 = τ1r00τ1l = τ1l , τ1r = τ1r , τ2 = τ20 . Consequently, τ1 = τ10 .

3. This is a simple generalization of property 2.

τ1./ τ20 .

τ1

τ1

By our induction hypothesis,J

Of course the real fun with prime numbers is the the unique factorization theorem.
Since ./ is not commutative we get a stronger version of the traditional theorem:
I Lemma 8 (Unique representation of S + ). For each τ ∈ T+ \{•}, there exists a uniquesequence τ1 , ..., τn ∈ Tp such that τ = ./ni=1 τi . Each τi is called a prime factor of τ .

FSTTCS 2016

XX:8

Decidability and Complexity of Tree Share Formulas

Proof. We prove by induction on the height of τ . The base case T1 is trivial. Assume it
holds for Tk and let τ ∈ Tk+1 . If τ is prime then we are done. Otherwise, let τ 1 , τ 2 ∈ Tk \{•}and τ = τ 1 ./ τ 2 . By our induction hypothesis, there are 2 sequences τ11 , ..., τk11 ∈ Tp and
12
12
τ12 , ..., τk22 ∈ Tp such that τ 1 = ./ki=1
τi1 and τ 2 = ./ki=1
τi2 and thus τ = (./ki=1
τi1 ) ./ (./ki=1
τi2 ).
The uniqueness is a consequence of property 3 from Lemma 6.
J
I Corollary 9 (Basis of S + ). Tp ∪ {•} is a basis of S + , i.e. the closure of Tp over ./ together
with • is T+ . Furthermore, it is the smallest basis: if B is a basis of S + then Tp ∪ {•} ⊆ B.
Accordingly, we will use Tp as our “infinite alphabet” in our isomorphism.

4.3

Connecting Tree Shares to Word Equations

We are ready to make the central connection needed for Lemma 3:
I Lemma 10. (T+ , ./) is isomorphic to (T∗p , •)Proof. Let f : T+ → T∗p be defined as follows. First, map the identity element • to the empty
word  and then for each prime tree τp ∈ T+ map τp to itself. Finally, for each compositeτ ∈ T+ map τ to exactly the concatenation of its (unique) prime factors.
We now wish to prove that for any τ1 and τ2 , f (τ1 ./ τ2 ) = f (τ1 ) • f (τ1 ). Let us consider
the easy cases first. If τ1 = • then f (τ1 ./ τ2 ) = f (τ2 ) =  • f (τ2 ) = f (τ1 ) • f (τ2 ). The
situation is symmetric when τ2 = •. Now let us consider the case when neither τ1 nor τ2 is •.
Let p1 , . . . , pi be the unique prime factors of τ1 and p01 , . . . , p0j be the unique prime factorsof τ2 . By Lemma 8, p1 , . . . , pi , p01 , . . . , p0j are exactly the unique prime factors of τ1 ./ τ2 , so:f (τ1 ./ τ2 ) = f (p1 ./ · · · ./ pi ./ p01 ./ · · · ./ p0j ) = p1 • · · · • pi • p01 • · · · • p0j =(p1 • · · · • pi ) • (p01 • · · · • p0j ) = f (τ1 ) • f (τ2 )To prove f is surjective, let w ∈ T∗p be the concatenation of primes p1 • · · · • pi ; then by
the definition f (p1 ./ · · · ./ pi ) = w. To prove f is injective, suppose f (τ1 ) = f (τ2 ). Let
p1 , . . . pi be the prime factors of τ1 and p01 , . . . p0j be the prime factors of τ2 . Accordingly weknow that p1 • · · · • pi = p01 • · · · • p0j , and since equality over words can only occur if the words
have the same length and have the same letters, we know i = j and pk = p0k for all k.
J
I Corollary 11 (Equations over Positive Tree Shares are Word Equations). Equations ET+ over
(T+ , ./) contain both tree constants τ ∈ T+ and variables v ∈ V ; we can map these to word
equations EW over (T∗p , •) by mapping variables to themselves, constants to the concatenationof their prime factors, and multiplication ./ to concatenation •. The resulting system is
equivalent, i.e. if ρ : V → T+ satisfies ET+ then f ◦ ρ satisfies EW , where ◦ in this casemeans functional composition and f is the isomorphism constructed in Lemma 10.
We are now ready to start tackling Lemma 3. We start with the simplest:
Proof of Lemma 3.3. As previously mentioned, the first order theory over word equations
is known to be undecidable [23, 18]. By Lemma 10 we know that this theory is isomorphic to
the first order theory over tree shares with ./, which accordingly must be undecidable. J
To show Lemma 3.1 we need to know that tree factorization can be done within PSPACE.
In fact we can do much better:
I Lemma 12 (Factorization). Factoring an arbitrary positive tree share τ is in P.

X. Bach Le, Aquinas Hobor, and Anthony W. Lin

XX:9

Proof. Let S(τ ) be the set of all subtrees of τ and Sn (τ ) ⊂ S(τ ) be the set of all subtreesof τ with height exactly n. S(τ ) can be computed recursively: S(◦) = {◦}, S(•) = {•},
S(
) = S(τ1 ) ∪ S(τ2 ) ∪ {}. If τ = τ1 ./ τ2 ({τ1 , τ2 } ⊂ T+ \{•}), then there exists
τ1

τ2

τ1

τ2

n ∈ N such that Sn (τ ) = {τ2 }, that is, S|τ2 | (τ ) is exactly the singleton set {τ2 }. Additionally,S|τ |S(τ ) = i=0 Si (τ ).
Thus we can find all the prime factors of τ (which is inspired from the well-known sieveof Eratosthenes) as follows: first we compute S(τ ) and partition it into S0 (τ ), . . . , S|τ | (τ ).
Let i ∈ N be the smallest number such that Si (τ ) is the singleton set {τ1 } for some τ1 ∈ T(note that i must be larger than 0 since S0 (τ ) = {◦, •}). If i = |τ | then τ itself is a prime,otherwise, we replace all subtrees τ1 of τ with • and call the new tree τ 0 . If all the “old” •leaves of τ are replaced and τ 0 is in canonical form then τ = τ 0 ./ τ1 , τ1 is a prime factorof τ , and we can repeat the process with τ 0 to find the next prime factor. Otherwise, we
consider the next singleton set Sj (τ ).
If τ has n leaves than its description requires O(n) bits and the time to compute S(τ ) isnO(n). Note that |Sk (τ )| ≤ k+1
because there are at least k + 1 leaves in a tree of height k.
nTherefore, the number of subtrees from height 1 to n is at most Σni=1 i+1≤ n2 . Computing0
the height of a subtree τ of τ requires O(n), thus the time to partition S(τ ) is O(n3 ). The
number of times we need to restart the process is O(n2 ). Consequently, the time for tree
factorization is O(n5 ), polynomial in the description of τ (more efficient solutions exist). J
Tree factorization is fundamentally simpler than integer factorization since the representationof a tree already contains the descriptions of all of its tree factors. In contrast, the connection
between the representation of a number and the representation of its prime factors is vague:e.g. among the 24 factors of 74,611,647 are 333 (which does not appear at all in the
representation of the original) and 8,290,183 (which only shares a single 1 with the original).
Proof of Lemma 3.1. We take the tree shares and factor them using Lemma 12 and thenconstruct the isomorphic system of word equations using the calculated prime factors as
the alphabet using Corollary 11. As mentioned, the best known complexity bound for the
existential word equation problem is PSPACE [25, 26].
J
For Lemma 3.2 we need one final fact:
I Lemma 13 (Existence of small primes). For any n (represented in unary) we can find alength-n sequence of tree primes S in polynomial time of n.
Proof. Consider the sequence S from Lemma 6: the description of pi is only a constant size
larger than the description of pi−1 so the description of S is quadratic in n.
J
Proof of Lemma 3.2. Suppose we have an arbitrary problem Q in NP. We can reduce Q
to word equations in polynomial time [25, 26]. We then use Lemma 13 to construct a setof primes the size of the number of alphabet letters that appear in the equations and map
each letter in the word alphabet to a distinct prime, creating a set of word equations overT∗p . Since the representation of the constants does not affect the computational properties of
the theory, we can conclude that T+ is NP-hard.
J

5

A reduction to Tree Automatic Structures

Theorem 2 shows that the first order theory (FO) over S is undecidable, so of course any
extension of S—e.g. with (u, t, )—also has an undecidable FO. However, if we restrict the

FSTTCS 2016

XX:10

Decidability and Complexity of Tree Share Formulas

form of ./-equations to be π1 ./ τ = π2 where τ ∈ T, then the FO of S is decidable because
the relation is tree-automatic. This type of restriction is inspired by Jain et al.’s concept ofsemi-automatic structures [14], in which relations are restricted so that all input arguments
are fixed constants except for one argument which is a variable. As a result, certain relations
become automatic, e.g. multiplication in unary language.
Let τ ./ : T → T and ./τ : T → T be the left and right restricted form of ./ with respectto τ ∈ T, i.e. τ ./(τ1 ) , τ ./ τ1 and ./τ (τ1 ) , τ1 ./ τ . We will show T , (T, u, t, , ./ ),where ./ denotes the family of all right-restricted forms of ./ indexed by tree constants, istree-automatic by constructing bottom-up tree automata that recognize the domain T andthe relations in T :I Theorem 14 (Decidability of (T, u, t, , ./ )). T is tree-automatic. As a result, thefirst-order theory of T is decidable.
As indicated by equation (7) (from §2), one use for ./ is to split/join ownership of maps-to
predicates in separation logic. Here the splitting/joining occurs on the right-hand side of
the ./. Moreover, many functions need to divide their ownership only a finite number oftimes before e.g. calling other functions or indeed themselves recursively. This is because
the program text of functions is finite. Accordingly, we believe that T is worthy of attention.

5.1

Tree automatic structures

Before proving Theorem 14, we recall the definition of tree automatic structures [27, 15].
Tree automaton. A bottom up tree automaton is a 4-tuple A = (Q, F, Qf , ∆) where Q is
the set of states, F is the ranked alphabet, Qf ⊂ Q is the set of accepting states and ∆ isthe set of transitions f (q1 (v1 ), ..., qn (vn )) → qn+1 (f (v1 , ..., vn )) where f ∈ F is a n-ary letter,vi ∈ V is a variable and qj ∈ Q. Let T be a tree constructed from F then A runs on T by
applying ∆ at each leaf of T spontaneously and proceeding upward. A accepts T if the state
associated with the root of T is in Qf . We will put a temporary superscript number (n)above each letter in the definition of F to indicate its arity, i.e. f (n) means f is n-ary. For
instance, the ranked alphabet for the tree domain T is F = {◦(0) , •(0) , Node(2) }.
Tree automatic structures. Let R ⊂ Dk be a k-ary tree relation on some tree domain
D, its convolution set is constructed by overlapping all k trees of each element in R toform a single tree. As trees can have different shapes and thus their convolution contains “holes”, we fill the holes with a special nullary character (0) that is not in F , e.g.
(Node(a1 , a2 ), b, Node(c1 , c2 )) 7→ [Node, b, Node]([a1 , , c1 ], [a2 , , c2 ]). As a result, if FD is theranked alphabet of D then (FD ∪ {})k is the ranked alphabet for Dk and the arity of eachconvolution letter is the maximal arity among its letter components. R is tree-automatic if
its convolution set is accepted by a tree automaton. Generally, a structure (D, R1 , . . . , Rn )is tree-automatic if its domain D and each of its relations Ri are tree-automatic. We restatea well-known decidability result for tree automatic structures:
I Lemma 15 ([5, 6]). The first-order theory of a tree automatic structures is decidable.

5.2

Tree automata construction for T

Construction of AT . For the domain T, it suffices to check the canonical form. Let
AT = (QT , F T , QTf , ∆T ) such that QT = {q, q◦ , q• }, F T = F, QTf = {q} and the transition
relation ∆T contains the following:◦ 7→ q(◦) and • 7→ q(•)
Node(q1 (v1 ), q2 (v2 )) 7→ q(Node(v1 , v2 )) where (q1 , q2 ) ∈ {(q◦ , q• ), (q• , q◦ ), (q, q)}X. Bach Le, Aquinas Hobor, and Anthony W. Lin

XX:11

Construction of A . From now on, we assume that the input trees are in domain T,
which will make other constructions more pleasant. The automaton A for complement  iseasy: we need to verify the opposite values leaf-wise between two trees . To be precise, let(Q , F  , Q= (F ∪ {})2 and ∆ is defined as:
f , ∆ ) such that Q = Qf = {q}, F[•, ◦] 7→ q([•, ◦]) and [◦, •] 7→ q([◦, •])[Node, Node](q(v1 ), q(v2 )) 7→ q([Node, Node](v1 , v2 ))}Construction of At and Au . At and Au are more sophisticated as trees can have different
shapes and thus are inapplicable for leaf-wise comparison. For instance, the convolution of
the relation ◦ • t • = • is [Node, •, •]([◦, , ], [•, , ]). When we proceed upward, the leafvalues of the second and third tree are initially unknown (denoted by ) but later recognizedas •. The trick to build the automaton is by guessing: when moving bottom-up, the statesof the automaton record the set of all possible values for the unknown leaves and later check
whether the observed values belong to the guessing set. When proceeding upward, if two
guessing sets meet at a certain step, they are unified into a single guessing set: first wecompute their intersection and then unify it with the observed values at the current node.
In details, we define F t = (F ∪ {})3 , Qt = {qS | S ⊆ {(τ1 , τ2 , τ3 ) | τi ∈ {◦, •, ?}}} andQt
f = {q{(?,?,?)} } where ? indicates the value was already seen. Let D = {◦, •, , Node, ?}and φ : D × D → {?, } be the unit unification:
φ(Node, ?) = φ(◦, ◦) = φ(•, •) = ?, φ(, ) = φ(τ1 , τ2 ) is undefined otherwise
We extend φ to φ0 : D3 × P(D3 ) → P(D3 ) to handle the convolution form of t:
V3
φ ((τ1 , τ2 , τ3 ), S) = {(τ10 , τ20 , τ30 ) | ∃k1 , k2 , k3 .((k1 , k2 , k3 ) ∈ S i=1 φ(τi , ki ) = τi0 )}. Finally,
the transition relation is defined to be ∆t = Sg ∪ Su where Sg contains all guessing rules atleaf level for t and Su is the transition part for unification that contains relations of the form
[τ1 , τ2 , τ3 ](qS1 (v1 ), qS2 (v2 )) 7→ qS ([τ1 , τ2 , τ3 ](v1 , v2 )) such that S = φ0 ((τ1 , τ2 , τ3 ), S1 ∩ S2 ).
Similarly, the automaton for u can be constructed by modifying Sg . For demonstration,
consider ◦ • t • = • whose convolution [Node, •, •]([◦, , ], [•, , ]) has the following run:0[◦, , ] 7→ qS1 ([◦, , ]) where S1 = {(?, •, •), (?, ◦, ◦)}[•, , ] 7→ qS2 ([•, , ]) where S2 = {(?, •, •), (?, ◦, •)}As S = S1 ∩ S2 = {(?, •, •)} and φ0 ((Node, •, •), S) = {(?, ?, ?)}, we have:[Node, •, •](qS1 ([◦, , ]), qS2 ([•, , ])) 7→ q{(?,?,?)} ([Node, •, •]([◦, , ], [•, , ]))Construction of A./τ . Next, we give the description of bottom-up tree automaton A./τthat recognizes ./τ . Let S : T → P(T) be the function that extracts all subtrees: S(•) = {•},S(◦) = {◦}, S()={} ∪ S(τ1 ) ∪ S(τ2 ). The ranked alphabet for A./τ is F ./τ =
τ1

τ2

τ1

τ2

τ
(F ∪ {})2 . The state space for A./τ is Q./τ = {qτ 0 | τ 0 ∈ S(τ )} ∪ {qf } and Q./= {qf }.
fW.l.o.g., we assume that τ 6∈ {◦, •} as those cases can be trivially reduced to equalities,
which is a special case of t: τ1 = τ2 ⇔ τ1 t ◦ = τ2 . The transition relation ∆./τ is defined asfollows:

a1 . [◦, ◦] 7→ qf ([◦, ◦])a2 . [, τ 0 ] 7→ qτ 0 ([, τ 0 ]) if τ 0 ∈ S(τ )a3 . [, Node](qτ1 (v1 ), qτ2 (v2 )) 7→ qτ3 ([, Node](v1 , v2 )) if τ3 =b1 . [•, Node](qτ1 (v1 ), qτ2 (v2 )) 7→ qf ([•, Node](v1 , v2 )) if τ =

τ1

τ1

τ2

∈ S(τ ) and τ3 6= τ

τ2b2 . [Node, Node](qf (v1 ), qf (v2 )) 7→ qf ([Node, Node](v1 , v2 ))FSTTCS 2016

XX:12

Decidability and Complexity of Tree Share Formulas

Briefly speaking, we traverse upward and check whether τ is a subtree of the second tree
(a1 − a3 ). When • is seen from the first tree (b1 ), we check whether the two trees have similar
shape (b2 ).
I Remark. As we are about to prove, the other relation τ ./ is not tree-automatic in thisrepresentation. We leave an open question whether there exists a representation in which
both ./τ and τ ./ are automatic i.e. whether ./ is semi-automatic.
I Proposition 16 (τ ./). In the current representation of tree shares, there exists infinitely
many τ such that τ ./ is not tree-automatic.
First, we recall the Pumping Lemma for tree automata:
I Definition 17 (Term, context and substitution [9]). Let A = (Q, F, Qf , ∆) be a tree
automaton and V the set of variables. We define T (F, V ) the set of all tree terms derived
from F ∪ V and T (F, ∅) is the set of ground terms. A term t is linear if each variable appears
at most once in t. A context C is a linear term of T (F, V ) and C(F) denotes the set of allcontexts with single variable. A context is trivial if it is reduced to a variable. Let C[t]be the substitution of C ∈ C(F) by replacing the variable in C with the term t. We define
C 0 [t] = v where v is the variable in C, C 1 [t] = C[t] and C n+1 [t] = C[C n [t]].
I Lemma 18 (Pumping Lemma for Tree Automata [9]). Let L be the set of all ground terms
recognizable by a tree automaton. There is a constant k ∈ N+ satisfying the following
condition: for all ground term t ∈ L and |t| > k, there exists a context C ∈ C(F), a nontrivial
context C 0 ∈ C(F) and a ground term t0 such that t = C[C 0 [t0 ]] and ∀n ∈ N. C[C 0n [t0 ]] ∈ L.
. For an input tree τ 0 ∈ T+ , theProof of Proposition 16. Let τ ./ where τ =
•

◦

•

◦

in which the left and right subtree are identical. If τ ./ is automatic

result tree is
τ0

◦

τ0

◦

then it satisfies the Pumping Lemma. However, the Pumping Lemma only allows us to pumpeither the left or the right subtree and thus they will be different after pumping, which is a
, τn+1 =thencontradiction. Now consider the following sequence: τ1 =•each of the τi ./ is not automatic.

6

◦

•

◦

τn

τn

J

Future Work

We identify several directions for future research. One obvious question is the decidability ofthe existential theory of the tree share model with ./, t, u, and , where ./ is unrestricted.
Our connection to word equations does not seem to provide an answer to decidability ofthis problem. Another question is the computational complexity of adding more general
constants (i.e., other than ◦ and •) to the first order theory of M. Although such constants
are in some way “definable” (e.g. in first-order logic over the vocabulary with ◦ and •), thedefinition in general requires a formula of superpolynomial size. For this reason, connections
to CABA do not immediately yield the same computational complexity. A final direction for
future work is to investigate the integration of ./ into a practical program logic.

7

Conclusion

We have demonstrated the decidability and complexity of a first-order theory over the
Boolean logic of tree shares by pinpointing the connection to countable atomless Boolean

X. Bach Le, Aquinas Hobor, and Anthony W. Lin

XX:13

algebras. We have provided the first serious look at the complexity of the tree multiplication./ operator and by way of an isomorphism to word equations prove that the existential
theory is in PSPACE while the general first-order theory is undecidable. We have identified
a restricted version of ./ that takes constants on the right-hand side ./ and have proventhat the system (T, t, u, , ./ ) has a decidable first-order theory via an embedding totree-automatic structures.
References
1

2
3

4
5
6
7

8

9

10

11

12

13
14

Parosh Aziz Abdulla, Yu-Fang Chen, Lukás Holík, Richard Mayr, and Tomás Vojnar. Whensimulation meets antichains. In Tools and Algorithms for the Construction and Analysis of
Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European
Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March
20-28, 2010. Proceedings, pages 158–174, 2010.
H. Abdulrab and J.P Pechuchet. Solving word equations. In Journal of Symbolic Computation, pages 499–521, 1989.
Andrew W. Appel, Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy. Program Logics for Certified Compilers.
Cambridge University Press, New York, NY, USA, 2014.
Leonard Berman. The complexity of logical theories. Theoretical Computer Science,
11(1):71–77, May 1980.
A. Blumensath. Automatic Structures. PhD thesis, RWTH Aachen, 1999.
A. Blumensath and E. Grade. Finite presentations of infinite structures: automata andinterpretations. In Theory of Computer Systems, pages 641–674, 2004.
John Boyland. Checking interference with fractional permissions. In Static Analysis, 10th
International Symposium, SAS 2003, San Diego, CA, USA, June 11-13, 2003, Proceedings,
pages 55–72, 2003.
J Richard Büchi and Steven Senger. Definability in the existential theory of concatenation
and undecidable extensions of this theory. In The Collected Works of J. Richard Büchi,pages 671–683. Springer, 1990.
H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard, D. Lugiez, S. Tison, andM. Tommasi. Tree automata techniques and applications. Available on: http://www.
grappa.univ-lille3.fr/tata, 2007. release October, 12th 2007.
Robert Dockins, Aquinas Hobor, and Andrew W. Appel. A fresh look at separation algebrasand share accounting. In Programming Languages and Systems, 7th Asian Symposium,
APLAS 2009, Seoul, Korea, December 14-16, 2009. Proceedings, pages 161–177, 2009.
Aquinas Hobor, Andrew W. Appel, and Francesco Zappa Nardelli. Oracle semantics forconcurrent separation logic. In 17th European Symposium of Programming (ESOP 2008),
pages 353–367, April 2008.
Aquinas Hobor and Cristian Gherghina. Barriers in concurrent separation logic. In Programming Languages and Systems - 20th European Symposium on Programming, ESOP2011, Held as Part of the Joint European Conferences on Theory and Practice of Software,
ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, pages 276–296,
2011.
Joxan Jaffar. Minimal and complete word unification. J. ACM, 37(1):47–85, 1990.
Sanjay Jain, Bakhadyr Khoussainov, Frank Stephan, Dan Teng, and Siyuan Zou. Semiautomatic structures. In Computer Science - Theory and Applications - 9th International
Computer Science Symposium in Russia, CSR 2014, Moscow, Russia, June 7-11, 2014.
Proceedings, pages 204–217, 2014.

FSTTCS 2016

XX:14

Decidability and Complexity of Tree Share Formulas

15

16
17
18
19

20
21
22
23
24
25
26
27
28
29

Bakhadyr Khoussainov and Mia Minnes. Three lectures on automatic structures. In Logic
Colloquium 2007 (F. Delon, U. Kohlenbach, P. Maddy, and F. Stephan, editors), Lecture
Notes in Logic, vol. 35, Association for Symbolic Logic, pages 132–176, 2007.
Antoni Koscielski and Leszek Pacholski. Complexity of Makanin’s algorithm. J. ACM,
43(4):670–684, 1996.
Dexter Kozen. Complexity of boolean algebras. In Theoretical Computer Science 10, pages
221–247, 1980.
D. Kuske. Theories of orders on the set of words. In Theoretical Informatics and Applications 40, pages 53–74, 2006.
Xuan Bach Le, Cristian Gherghina, and Aquinas Hobor. Decision procedures over sophisticated fractional permissions. In Programming Languages and Systems - 10th Asian Symposium, APLAS 2012, Kyoto, Japan, December 11-13, 2012. Proceedings, pages 368–385,
2012.
G. S Makanin. The problem of solvability of equations in a free semigroup. In Mat. Sbornik,
pages 147–236, 1977.
G. S Makanin. Equations in a free group. In Izvestiya AN SSSR, pages 1199–1273, 19821983.
G.S Makanin. Decidability of the universal and positive theories of a free group. In Izvestiya
AN SSSR, pages 735–749, 1984-1985.
S. Marchenkov. Unsolvability of positive ∀∃-theory of free semi-group. In Sibirsky mathmatichesky jurnal, pages 196–198, 1982.
Kim Marriott and Martin Odersky. Negative boolean constraints. In Theoretical Computer
Science 160, pages 365–380, 1996.
W. Plandowski. Satisfiability of word equations with constants is in PSPACE. In Journalof the Association for Computing Machinery, pages 483–496, 2004.
W. Plandowski. An efficient algorithm for solving word equations. In Proc 38th Annual
Symposium on Theory of Computing, pages 467–476, 2006.
M.O. Rabin. Decidability of second-order theories and automata on infinite trees. In Trans
AMS, pages 341–360, 1960.
Stijn Vermeeren. Embeddings into the countable atomless Boolean algebra. http://stijnvermeeren.be/download/mathematics/embeddings.pdf, 2010.
Jules Villard. Heaps and Hops. Ph.D. thesis, Laboratoire Spécification et Vérification,
École Normale Supérieure de Cachan, France, February 2011.