On Generalized Records and
Spatial Conjunction in Role Logic

arXiv:cs/0408019v1 [] 5 Aug 2004

Viktor Kuncak and Martin Rinard
MIT Computer Science and Artificial Intelligence Laboratory
{vkuncak, rinard}@csail.mit.edu
MIT CSAIL Technical Report No 942 VK0104
Abstract. We have previously introduced role logic as a notation for
describing properties of relational structures in shape analysis, databases
and knowledge bases. A natural fragment of role logic corresponds to
two-variable logic with counting and is therefore decidable.
We show how to use role logic to describe open and closed records, as
well the dual of records, inverse records. We observe that the spatial
conjunction operation of separation logic naturally models record concatenation. Moreover, we show how to eliminate the spatial conjunction
of formulas of quantifier depth one in first-order logic with counting. As
a result, allowing spatial conjunction of formulas of quantifier depth one
preserves the decidability of two-variable logic with counting. This result
applies to two-variable role logic fragment as well.
The resulting logic smoothly integrates type system and predicate calculus notation and can be viewed as a natural generalization of the notation for constraints arising in role analysis and similar shape analysis
approaches.

Keywords:. Records, Shape Analysis, Static Analysis, Program Verification,
Two-Variable Logic with Counting, Description Logic, Types

Table of Contents
1
2
3
4
5
6
7

Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
A Decidable Two-Variable Role Logic RL2 . . . . . . . . . . . . . . . . . . . . . . . . .
Spatial Conjunction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Field Complement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Records and Inverse Records . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Role Constraints . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Eliminating Spatial Conjunction in RL2 . . . . . . . . . . . . . . . . . . . . . . . . . . .
7.1 Atomic Type Formulas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7.2 Spatial Conjunction of Stars . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
8 Further Remarks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
8.1 Extracting Subformulas in the Presence of ⊛ . . . . . . . . . . . . . . . . . .
8.2 Representing ⊛ in Second-Order Logic . . . . . . . . . . . . . . . . . . . . . . .
9 Further Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
10 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
A Appendix: Correctness of Spatial Conjunction Elimination . . . . . . . . . .
Version of September 29, 2017, 8:40pm.

2
4
5
6
8
9
10
11
13
18
18
18
20
21
24

1

Introduction

In [36] we have introduced role logic, a notation for describing properties of
relational structures in shape analysis, databases and knowledge bases. Role
logic notation aims to combine the simplicity of role declarations [33] and the
well-established first-order logic. Role logic is closed under all boolean operations
and generalizes boolean shape analysis constraints [37]. Role logic formulas easily
translate into the traditional first-order logic notation. Despite this generality,
role logic enables the concise expression of common properties of data structures
in imperative programs that manipulate complex data structures with mutable
references. In [36, Section 4] we have established the decidability of the fragment
RL2 of role logic by exhibiting a correspondence with two-variable logic with
counting C 2 [22, 45].
Generalized records in role logic. In this paper we give a systematic
account of field and slot declarations of role analysis [33] by introducing a set of
role logic shorthands that allows concise description of records. Our basic idea
is to generalize types to unary predicates on objects. Some of the aspects of our
notion of records that indicate its generality are:
1. We allow building new records by taking the conjunction, disjunction, or
negation of records.
2. In our notation, a record indicates a property of an object at a particular
program point; objects can satisfy different record specifications at different program points. As a result, our records can express typestate changes
such as object initialization [16–18, 55, 56] and more general changes in relationships between objects such as movements of objects between data structures [32, 33, 54].
3. We allow inverse records as a dual of records that specify incoming edges of
an object in the graph of objects representing program heap. Inverse records
allow the specification of aliasing properties of objects, generalizing unique
pointers. Inverse records enable the convenient specification of movements
of objects that participate in multiple data structures.
4. We allow the specification of both open and closed records. Closed records
specify a complete set of outgoing and incoming edges of an object. Open
records leave certain edges unspecified, which allows orthogonal data structures to be specified independently and then combined using logical conjunction.
5. We allow the concatenation of generalized records using a form of spatial
conjunction of separation logic, while remaining within the decidable fragment of two-variable role logic.
Separation logic. Separation logic [28, 43, 51, 52] is a promising approach for
specifying properties of programs in the presence of mutable data structures. One
of the main uses of separation logic in previous approaches is dealing with frame
conditions [5, 28]. In contrast, our paper identifies another use of spatial logic:
expressing record concatenation. Although our approach is based on essentially
2

same logical operation of spatial conjunction, our use of spatial conjunction for
records is more local, because it applies to the descriptions of the neighborhood
of an object.
To remain within the decidable fragment of role logic, we give in Section 7
a construction that eliminates spatial conjunction when it connects formulas of
quantifier depth one. This construction also illustrates that spatial conjunction
is useful for reasoning about counting stars [22] of the two-variable logic with
counting C 2 . To our knowledge, this is the first result that combines two-variable
logic with counting and a form of spatial conjunction.
Using the resulting logic. We can use specifications written in our notation to
describe properties and relations between objects in programs with dynamically
allocated data structures. These specifications can act as assertions, preconditions, postconditions, loop invariants or data structure invariants [33, 36, 39].
By selecting a finite-height lattice of properties for a given program fragment,
abstract interpretation [15] can be used to synthesize properties of objects at intermediate program points [2, 3, 24, 33, 49, 50, 54, 58, 59]. Decidability and closure
properties of our notation are essential for the completeness and predictability
of the resulting static analysis [38].
Contributions. We summarize the main contributions of this paper as follows:
1. We present a logic which generalizes the concept of records in several directions (Section 5). These generalizations are useful for expressing properties
of objects and memory cells in imperative programs, and go beyond standard
type systems.
2. We identify a novel use of separation logic: modelling the concatenation of
generalized records.
3. We show how to translate role constraints from role analysis [33] to role logic
(Section 6).
4. We show that, under certain syntactic restrictions, we can translate spatial
conjunction into other constructs of the decidable logic RL2 (Section 7).
We therefore obtain a notation that extends RL2 with a convenient way of
describing record concatenation, and remains decidable.
5. We present a translation of first-order logic with spatial conjunction and
inductive definitions into second-order logic (Section 8.2).
Outline. Section 2 reviews the syntax and semantics of role logic. Section 3
defines spatial conjunction in role logic and motivates its use for describing record
concatenation. Section 4 and Section 5 show how to use spatial conjunction in
role logic to describe a generalization of records. Section 6 demonstrates that our
notation is a generalization of the local constraints arising in role analysis [33]
by giving a natural embedding of role constraints into our notation. Section 7
shows how to eliminate the spatial conjunction connective ⊛ from a spatial
conjunction F1 ⊛ F2 of two formulas F1 and F2 when F1 and F2 have no nested
counting quantifiers; this is the core technical result of this paper. A consequence
of this is result is that we may allow certain uses of spatial conjunction in RL2
fragment of role logic while preserving the decidability property of RL2 . Our
3

extension of role logic with spatial conjunction is therefore justified: it allows
record-like specifications to be expressed in a more natural way, and it does not
lead outside the decidable fragment. Section 8 contains remarks on preserving the
satisfiability of formulas in the presence of spatial conjunction and shows how to
encode the spatial conjunction (with inductive definitions) in second-order logic.
Section 9 presents related work, and Section 10 concludes. Appendix contains
the details of the correctness proof for the elimination of spatial conjunction
from Section 7.

2

A Decidable Two-Variable Role Logic RL2

F ::= A | f | EQ | F1 ∧ F2 | ¬F | F ′ | ∼F | card≥k F
e :: {1, 2} → D
[[A]]e = [[A]](e 1)

[[f ]]e = [[f ]](e 2, e 1)

[[EQ]]e = (e 2) = (e 1)
[[F1 ∧ F2 ]]e = ([[F1 ]]e) ∧ ([[F2 ]]e)

[[¬F ]]e = ¬([[F ]]e)

[[F ′ ]]e = [[F ]](e[1 7→ (e 2)])

[[∼F ]]e = [[F ]](e[1 7→ (e 2), 2 7→ (e 1)])

[[card≥k F ]]e = |{d ∈ D | [[F ]](e[1 7→ o, 2 7→ (e 1)])}| ≥ k
F1 ∨ F2 ≡ ¬(¬F1 ∧ ¬F2 )
F1 ⇒ F2 ≡ ¬F1 ∨ F2
Fig. 1. The Syntax and the Semantics of RL2

Figure 1 presents the two-variable role logic RL2 [36]. We have proved in [36]
that RL2 has the same expressive power as two-variable logic with counting
C 2 . The logic C 2 is a first-order logic 1) extended with counting quantifiers
∃≥k x.F (x), saying that there are at least k elements x satisfying formula F (x)
for some constant k, and 2) restricted to allow only two variable names x, y in
formulas. An example formula in two-variable logic with counting is
∀x.A(x) ⇒ (∀y.f (x, y) ⇒ ∃=1 x. g(x, y))

(1)

The formula (1) means that all nodes that satisfy A(x) point along the field f
to nodes that have exactly one incoming g edge. Note that the variables x and y
may be reused via quantifier nesting, and that formulas of the form ∃=k x. F (x)
and ∃≤k x. F (x) are expressible as boolean combination of formulas of the form
∃≥k x. F (x). The logic C 2 was shown decidable in [22] and the complexity for
the C12 fragment of C 2 (with counting up to one) was established in [45]. We can
view role logic as a variable-free version of C 2 . Variable-free logical notations are
attractive as generalizations of type systems because traditional type systems
4

are often variable-free. The formula (1) can be written in role logic as [A ⇒
[f ⇒ card≥1 ∼g]] where the construct [F ] is a shorthand for ¬card≥1 ¬F and
corresponds to the universal quantifier. The expression ∼g denotes the inverse
of relation g. This paper focuses on the use of role logic to describe generalized
records, see [36] for further examples of using role logic and [6] for advantages
of variable-free notation in general.

3

Spatial Conjunction

[[F1 ⊛ F2 ]]e = ∃e1 , e2 . split e [e1 e2 ] ∧ [[F1 ]]e1 ∧ [[F2 ]]e2
split e [e1 e2 ] =
∀A ∈ A. ∀d ∈ D. (e A) d ⇐⇒ (e1 A) d ∨ (e2 A) d ∧ ¬((e1 A) d ∧ (e2 A) d) ∧
∀f ∈ F. ∀d1 , d2 ∈ D.
(e f ) d1 d2 ⇐⇒ (e1 f ) d1 d2 ∨ (e2 f ) d1 d2 ∧ ¬((e1 f ) d1 d2 ∧ (e2 f ) d1 d2 )
V
V
¬f ]]
¬A ∧
emp ≡ [[
A∈A

f ∈F

priority: ∧ binds strongest, then ⊛, then ∨
F ∼ G means ∀e. [[F ]]e = [[G]]e
(F1 ⊛ F2 ) ⊛ F3 ∼ F1 ⊛(F2 ⊛ F3 )
F ⊛ emp ∼ emp ⊛ F ∼ F
F1 ⊛ F2 ∼ F2 ⊛ F1
F1 ⊛(F2 ∨ F3 ) ∼ F1 ⊛ F2 ∨ F1 ⊛ F3
Fig. 2. Semantics and Properties of Spatial Conjunction ⊛.

Figure 2 shows our semantics of spatial conjunction ⊛. To motivate our use of
spatial conjunction, we first illustrate how role logic supports the description of
simple properties of objects in a concise way. Indeed, one of the design goals of
role logic is to have a logic-based specification language where simple properties
of objects are as convenient to write as type declarations in a language like Java.
Example 1. The formula [f ⇒ A] is true for an object whose every f -fields points
to an A object, [g ⇒ B] means that every g-field points to a B object, so
[f ⇒ A] ∧ [g ⇒ B]
denotes the objects that has both f pointing to an A object and g pointing to a
B object. Such specification is as concise as the following Java class declaration
class C { A f; B g; }
5

Example 1 illustrates how the presence of conjunction ∧ in role logic enables
combination of orthogonal properties such as constraints on distinct fields. However, not all properties naturally compose using conjunction.
Example 2. Consider a program that contains three fields, modelled as binary
relations f , g, h. The formula Pf ≡ (card=1 f ) ∧ (card=0 (g ∨ h)) means that
the object has only one outgoing f -edge and no other edges. The formula Pg ≡
(card=1 g) ∧ (card=0 (f ∨ h)) means that the object has only one outgoing g-edge
and no other edges. If we “physically join” two records, each of which has one
field, we obtain a record that has two fields, and is described by the formula
Pf g ≡ (card=1 f ) ∧ (card=1 g) ∧ (card=0 h)
Note that it is not the case that Pf g ∼ Pf ∧ Pg . More generally, no boolean
combination of Pf and Pg yields Pf g .
Example 2 prompts the question: is there an operation that allows joining specifications that will allow us to combine Pf and Pg into Pf g ? Moreover, can we
define such an operation on records viewed as arbitrary formulas in role logic?
It turns out that there is a natural way to describe the set of models of formula
Pf g in Example 2 as the result of “physically merging” the edges (relations) of
the models of Pf and models of Pg . The merging of disjoint models of formulas is
the idea behind the definition of spatial conjunction ⊛ in Figure 2. The predicate
(split e [e1 e2 ]) is true iff the relations of the model (environment) e can be split
into e1 and e2 and the notation generalizes to splitting into any number of
environments.
Example 3. For Pf , Pg , and Pf g of Example 2, we have Pf g = Pf ⊛ Pg .
Note that the operation ⊛ is associative and commutative. The formula emp,
which asserts that all predicates are false, is the unit for ⊛. Moreover, ⊛ distributes over ∨.
A note on relationship with [28]. The semantics of spatial conjunction in
Figure 2 match the semantics of [28], with two differences.
A small technical difference is that Figure 2 splits the edges of the model
(the tuples of the relations), whereas [28] splits the domain. The difference arises
because the elements of the domain in [28] are locations, whereas the elements
of our models are objects. To represent a location in our view, we would use a
tuple ho, f i where o is an element of the domain and f is a field name.
A higher-level difference is that the use of spatial logic we propose in this
paper is the notation for records (Section 5), as opposed to the description of
global heap properties. When used for formulas of quantifier depth one (Section 7), spatial conjunction does not even change the set of definable relations
of two-variable logic with counting.

4

Field Complement

As a step towards record calculus in role logic, this section introduces the notion
of a field complement, which makes it easier to describe records in role logic.
6

Example 4. Consider the formula Pf ≡ (card=1 f ) ∧ (card=0 (g ∨ h)) from Example 2, stating the property that an object has only one outgoing f -edge and no
other edges. Property Pf has little to do with g or h, yet g and h explicitly occur
in Pf . Moreover, we need to know the entire set of relations in the language to
write Pf ; if the language contains an additional field i, the property Pf would
become Pf ≡ (card=1 f ) ∧ (card=0 (g ∨ h ∨ i)). Note also that ¬f is not the same
as g ∨ h ∨ i, because ¬f computes the complement of the value of the relation f
with respect to the universal set, whereas g ∨ h ∨ i is the union of all relations
other than f .
To address the notational problem illustrated in Example 4, we introduce the
symbol edges, which denotes the union of all binary relations, and the notation
−f (field complement of f ), which denotes the union of all relations other than
f.
W
W
edges ≡

−f ≡

g

g

g

g6=f

This additional notation allows us to avoid explicitly listing all fields in the
language when stating properties like Pf .
Example 5. Formula Pf from Example 4 can be written as Pf ≡ (card=1 f ) ∧
(card=0 −f ), which mentions only f . Even when the language is extended with
additional relations, Pf still denotes the intended property. Similarly, to denote
the property of an object that has outgoing fields given by Pf and has no incoming fields, we use the predicate Pf ∧ card=0 ∼edges.
We use the notation edges and −f to build the notation for records and inverse
records in Section 5 below.
A note on ternary relation interpretation. It is possible to provide a
notation for relations that generalizes the notation edges and −f . The idea of
this generalization is to change the definition of the model (environment). Instead
of a model that specifies a binary relation for each field, the model specifies the
value of one ternary relation H and a unary tag-predicate for each field name.
For example, instead of the model that provides interpretations fI and gI for two
binary relations f and g, we could use the model that provides interpretation of
[[H]], where
[[H]]o1 o2 n = (n=f0 ∧ fI o1 o2 ) ∨
(n=g0 ∧ fI o1 o2 )
and the interpretation of unary tag-predicates f and g. Here f0 is an element
of the domain that tags tuples coming from [[f ]], whereas g0 tags tuples coming
from [[g]]. We interpret f as a predicate that is true only on the element f0 , and
similarly g as a predicate true only on the element g0 . We then introduce the
following dereferencing shorthand:
↑F ≡ {H ∧ F }

(2)

The expression ↑f now denotes the original interpretation of f , that is, [[↑f ]] = fI .
Moreover, ↑¬f corresponds to field complement −f , and ↑True corresponds to
7

edges. Note that the expressions of the form ↑(¬f ∧ ¬g) are now also available. Let B be a boolean combination of unary predicates denoting fields. These
unary predicates are disjoint, so transforming B into disjunctive normal form
and applying the property
↑(B1 ∨ B2 ) = ↑B1 ∨ ↑B2
which follows from (2), allows transforming ↑B into a boolean combination of
expressions of the form ↑f and ↑g. This means that we obtain no additional
expressive power using expressions of the form ↑B where B is a boolean combination of unary predicates denoting fields, so for simplicity we do not consider
such “ternary relation interpretation” further in this paper.

5

Records and Inverse Records

In this section we use role logic with spatial conjunction and field complement
from Section 4 to introduce a notation for records. We also introduce inverse
records, which are dual to records, and correspond to slot constraints in role
analysis [33].

∗

multifield: f → A ≡ card=0 (−f ∨ (f ∧ ¬A))
∗

s

field: f → A ≡ cards (A ∧ f ) ∧ f → A
s of the form =k, ≤k, or ≥k, for k ∈ {0, 1, 2, . . .}
=1

f →A ≡ f →A
∗

multislot: A ← f ≡ card=0 (∼−f ∨ (∼f ∧ ¬A))
∗

s

slot: A ← f ≡ cards (A ∧ ∼f ) ∧ A ← f
s of the form =k, ≤k, or ≥k, for k ∈ {0, 1, 2, . . .}
=1

A←f ≡ A←f
fm ::= field | multifield
closedRecord ::= fm | closedRecord ⊛ fm
openRecord ::= closedRecord ⊛ True
sm ::= slot | multislot
closedInvRecord ::= sm | closedInvRecord ⊛ sm
openInvRecord ::= closedInvRecord ⊛ True
Fig. 3. Record Notation

8

Figure 3 presents the notation for records and inverse records. A field predicate f → A is true for an object whose only outgoing edge in the graph (model) is
an f -edge terminating at A. Dually, a slot predicate A ← f is true for an object
whose only incoming edge in the graph is an f -edge originating at A. A multifield
∗
predicate f → A is true iff the object has any number of outgoing f -edges termi∗
nating at A, and no other edges. Dually, a multislot predicate A ← f is true iff
the object has any number of incoming f -edges originating from A, and no other
s
edges. We also allow notation f → A where s is an expression of the form =k,
≤k, or ≥k. This notation gives a bound on the number of outgoing edges, and
s
implies that there are no other outgoing edges. We similarly introduce A ← f . A
closed record is a spatial conjunction of fields and multifields. An open record is
a spatial conjunction of a closed record with True. While a closed record allows
only the listed fields, an open record allows any number of additional fields. Inverse records are dual to records, and we similarly distinguish open and closed
inverse records.
Example 6. To describe a closed record whose only fields are f and g where
f -fields point to objects in the set A and g-fields point to objects in the set
B, we use the predicate P1 ≡ f → A ⊛ g → B. The definition of P1 lists all
fields of the object. To specify an open record which certainly has fields f and g
but may or may not have other fields, we write P2 ≡ f → A ⊛ g → B ⊛ True.
Neither P1 nor P2 restrict incoming references of an object. To specify that
the only incoming references of an object are from the field h, we conjoin P2
∗
with the closed inverse record consisting of a single multislot True ← h, yielding
∗
the predicate P3 ≡ P2 ∧ True ← h. To specify that an object has exactly
one incoming reference, and that the incoming reference is from the h field and
originates from an object belonging to the set C, we use P4 ≡ P2 ∧ C ← h.
Note that specifications P3 and P4 go beyond most standard type systems in
their ability to specify the incoming (in addition to the outgoing) references of
objects.

6

Role Constraints

Role constraints were introduced in [30, 31, 33]. In this section we show that role
logic is a natural generalization of role constraints by giving a translation from
role constraints to role logic. A logical view of role constraints is also suggested
in [35, 35]. A role is a set of objects that satisfy a conjunction of the following
four kinds of constraints: field constraints, slot constraints, identities, acyclicities.
In this paper we show that role logic naturally models field constraints, slot
constraints, and identities. 1
Roles describing complete sets of fields and slots. Figure 4 shows the
translation of role constraints [33, Section 3] into role logic formulas. The simplicity of the translation is a consequence of the notation for records that we
have developed in this paper.
1

Acyclicities go beyond first-order logic because they involve non-local transitive closure
properties.

9

C[[fields F ; slots S; identities I; acyclic A]] = C[[fields F ]] ∧ C[[slots S]] ∧
[[identities I]] ∧ [[acyclic A]]
C[[fields f1 : S1 , . . . , fn : Sn ]] = f1 → S1 ⊛ . . . ⊛ fn → Sn
C[[slots S1 .f1 , . . . , Sn .fn ]] = S1 ← f1 ⊛ . . . ⊛ Sn ← fn
V
[[identities f1 .g1 , . . . , fn .gn ]] = n
i=1 [fi ⇒ ∼gi ]
W
[[acyclic f1 , . . . , fn ]] = acyclic ( n
i=1 fi )
Fig. 4. Translation of Role Constraints [33] into Role Logic Formulas

O[[fields F ; slots S; identities I; acyclic A]] = O[[fields F ]] ∧ O[[slots S]] ∧
[[identities I]] ∧ [[acyclic A]]
W
O[[fields f1 : S1 , . . . , fn : Sn ]] = C[[fields f1 : S1 , . . . , fn : Sn ]] ⊛ card=0 ( n
i=1 fi )
=0 Wm
O[[g1 , . . . , gm slots S1 .f1 , . . . , Sn .fn ]] = C[[slots S1 .f1 , . . . , Sn .fn ]] ⊛ card ( i=1 ∼gi )
Fig. 5. Translation of Simultaneous Role Constraints [33, Section 7.2] into Role Logic
Formulas. See also Figure 4.

Simultaneous Roles. In object-oriented programs, objects may participate
in multiple data structures. The idea of simultaneous roles [33, Section 7.2] is
to associate one role for the participation of an object in one data structure.
When the object participates in multiple data structures, the object plays multiple roles. Role logic naturally models simultaneous roles: each role is a unary
predicate, and if an object satisfies multiple roles, the the object satisfies the
conjunction of predicates. Figure 5 presents the translation of field and slot constraints of simultaneous roles into role logic. Whereas the roles of [33, Section
3] translate to closed records and closed inverse records, the simultaneous roles
of [33, Section 7.2] translate specifications that are closer to open records and
open inverse records.

7

Eliminating Spatial Conjunction in RL2

Preserving the decidability. Previous sections have demonstrated the usefulness of adding record concatenation in the form of spatial conjunction to our
notation for generalized records. However, a key question remains: is the resulting extended notation decidable? In this section we give an affirmative answer
to this question by showing how to compute the spatial conjunction using the
remaining logical operations for a large class of record specifications.
10

Approach. Consider two formulas F1 and F2 in first-order logic with counting,
where both F1 and F2 have quantifier depth one. An equivalent way of stating
the condition on F1 and F2 is that there are no nested occurrences of quantifiers.
(Note that we count one application of ∃≥k x. P as one quantifier, regardless of
the value k.) We show that, under these conditions, the spatial conjunction
F1 ⊛ F2 can be written as an equivalent formula F3 where F3 does not contain
the spatial conjunction operation ⊛. The proof proceeds by writing formulas F1 ,
F2 in a normal form, as a disjunction of counting stars [22], and showing that the
spatial conjunction of counting stars is equivalent to a disjunction of counting
stars.
As a consequence of the results in this section, adding the operation ⊛ to
logic with counting does not change its expressive power provided that both F1
and F2 have quantifier depth at most one. Here we allow F1 and F2 themselves
to contain spatial conjunction, because we may eliminate spatial conjunction in
F1 and F2 recursively. Applying these results to two-variable logic with counting
C 2 , we conclude that introducing into C 2 the spatial conjunction of formulas
of quantifier depth one preserves the decidability of C 2 . Furthermore, thanks to
the translations between C 2 and RL2 in [36], if we allow the spatial conjunction
of RL2 formulas with no nested card occurrences, we preserve the decidability of
the logic RL2 . The formulas of the resulting logic are given by
F ::= A | f | EQ | F1 ∧ F2 | ¬F | F ′ | ∼F | card≥k F
| F1 ⊛ F2 , if F1 and F2 have no nested card occurrences

Note that record specifications in Figure 3 contain no nested card occurrences,
so joining them using ⊛ yields formulas in the decidable fragment. Hence, in
addition to quantifiers and boolean operations, the resulting logic supports a
generalization of record concatenation, and is still decidable; this decidability
property is what we show in the sequel. We present the sketch of the proof, see
Appendix for proof details..
7.1

Atomic Type Formulas

In this section we introduce classes of formulas that correspond to the modeltheoretic notion of atomic type [44, Page 20] (see [25, Page 42] and [12, Page 78]
for the notion of type in general). We then introduce formulas that describe the
notion of counting stars [22, 45]. We conclude this section with Proposition 12,
which gives the normal form for formulas of quantifier depth one.
If C = C1 , . . . , Cm is a finite set of formulas, then a cube over C is a conjuncαm
tion of the form C1α1 ∧ . . . Cm
where αi ∈ {0, 1}, C 1 = C and C 0 = ¬C. For
simplicity, fix a finite language L = A ∪ F with A a finite set of unary predicate
symbols and F a finite set of binary predicate symbols. We work in predicate calculus with equality, and assume that the equality “=”, where = ∈
/ F , is present
as a binary relation symbol, unless explicitly stated otherwise. We use D to
denote a finite domain of interpretation and e to denote a model with variable
assignment; e maps A to 2D , maps F to 2D×D and maps variables to elements
of D. Let x1 , . . . , xn be a finite list of distinct variables. Let C be the set of all
11

atomic formulas F such that FV(F ) ⊆ {x1 , . . . , xn }. The set C is finite (in our
case it has |A|n + (|F | + 1)n2 elements). We call a cube over C a complete atomic
type (CAT) formula.
Example 7. If A = {A} and F = {f }, then
A(x1 ) ∧ ¬A(x2 ) ∧
¬f (x1 , x1 ) ∧ ¬f (x2 , x2 ) ∧ f (x1 , x2 ) ∧ ¬f (x2 , x1 ) ∧
x1 = x1 ∧ x2 = x2 ∧ x1 6= x2 ∧ x2 6= x1

is a CAT formula.
We may treat conjunction of literals as the set of literals, so we say that “a literal
belongs to the conjunction” and apply set-theoretic operations on conjunctions
of literals.
From the disjunctive normal form theorem for propositional logic, we obtain
the following Proposition 8.
Proposition 8. Every quantifier-free formula F such that FV(F ) ⊆
{x1 , . . . , xn } is equivalent to a disjunction of CAT formulas C such that FV(C) =
{x1 , . . . , xn }.
A CAT formula may be contradictory if, for example, it contains the literal
xi 6= xi as a conjunct. We next define classes of CAT formulas that are satisfiable
in the presence of equality. Let x1 , . . . , xn be distinct variables. A general-case
CAT (GCCAT) formula is a CAT formula F such that the following two conditions hold: 1) FV(F ) = {x1 , . . . , xn }; 2) for all 1 ≤ i, j ≤ n, the conjunct xi = xj
is in F iff i ≡ j. Let x1 , . . . , xn and y1 , . . . , ym be distinct
Vm variables. An equality
CAT (EQCAT) formula is a formula of the form j=1 yj = xij ∧ F, where
1 ≤ i1 , . . . , im ≤ n and F is a GCCAT formula such that FV(F ) = {x1 , . . . , xn }.
Lemma 9. Every CAT formula F is either contradictory, or is equivalent to an
EQCAT formula F ′ such that FV(F ′ ) = FV(F ).
From Proposition 8 and Lemma 9, we obtain the following Proposition 10.
Proposition 10. Every quantifier-free formula F such that FV(F ) ⊆
{x1 , . . . , xn } can be written as a disjunction of EQCAT formulas C such that
FV(C) = {x1 , . . . , xn }.
We next introduce the notion of an extension of a GCCAT formula. Let
x, x1 , . . . , xn be distinct variables and F be a GCCAT formula such that
FV(F ) = {x1 , . . . , xn }. We say that F ′ is an x-extension of F , and write
F ′ ∈ exts(F, x) iff all of the following conditions hold: 1) F ∧ F ′ is a GCCAT
formula; 2) FV(F ∧ F ′ ) = {x, x1 , . . . , xn }; 3) F and F ′ have no common atomic
formulas. Note that if FV(F1 ) = FV(F2 ), then exts(F1 , x) = exts(F2 , x) i.e. the
set of extensions of a GCCAT formula depends only on the free variables of the
formula; we introduce additional notation exts(x1 , . . . , xn , x) to denote exts(F, x)
for FV(F ) = {x1 , . . . , xn }.
12

To define a normal form for formulas of quantifier depth one, we introduce
the notion of k-counting star. If p ≥ 2 is a non-negative integer, let p+ be
a new symbol which represents the co-finite set of integers {p, p + 1, . . .}. Let
Cp = {0, 1, . . . , p−1, p+ }. If c ∈ Cp , by ∃i x. P we mean ∃=i x. P if i is an integer,
and ∃≥p x. P if i = p+ . We say that a formula F has a counting degree of at most
p iff the only counting quantifiers in F are of the form ∃c x. G for some c ∈ Cp+1 .
Definition 11 (Counting Star Formula). Let x, x1 , . . . , xn , and y1 , . . . , ym
be distinct variables, k ≥ 1 a positive integer, and F a GCCAT formula such
that FV(F ) = {x1 , . . . , xn }. A k-counting star function for F is a function γ :
exts(F, x) → Ck+1 . A k-counting-star formula for γ is a formula of the form
m
^

^

yj = xij ∧ F ∧

j=1

′

∃γ(F ) x. F ′

F ′ ∈exts(F,x)

where 1 ≤ i1 , . . . , im ≤ n.

V
Note that in Definition 11, formula m
j=1 yj = xij ∧F is an EQCAT formula, and
Vm
′
formula j=1 yj = xij ∧ F ∧ F is an EQCAT formula for each F ′ ∈ exts(F, x).
The following Proposition 12 shows that formulas of quantifier depth at most
one are equivalent to disjunctions of counting stars.
Proposition 12 (Depth-One Normal Form). Let F be a formula of such
that F has quantifier depth at most one, F has counting degree at most k, and
FV(F ) ⊆ {x1 , . . . , xn }. Then F is equivalent to a disjunction of k-counting-star
formulas FC where FV(FC ) = {x1 , . . . , xn }.
7.2

Spatial Conjunction of Stars

Sketch of the construction. Let F1 and F2 be two formulas of quantifier depth
at most one, and not containing the logical operation ⊛. By Proposition
12, let
Wn1
C
and
let
F1 be equivalent to the disjunction of counting star formulas i=1
1,i
Wn2
C2,j . By
F2 be equivalent to the disjunction of counting star formulas j=1
distributivity of law of ⊛ with respect to ∨, we have
F1 ⊛ F2 ∼ (

n1
_
i=1

C1,i ) ⊛(

n2
_

C2,j ) ∼

j=1

n1 n2
_
_

C1,i ⊛ C2,j

i=1 j=1

In the sequel we show that a spatial conjunction of counting-star formulas is
either contradictory or is equivalent to a disjunction of counting star formulas.
This suffices to eliminate spatial conjunction of formulas of quantifier depth at
most one. Moreover, if F is any formula of quantifier depth at most one, possibly
containing ⊛, by repeated elimination of the innermost ⊛ we obtain a formula
without ⊛.
To compute the spatial conjunction of counting stars we establish an alternative syntactic form for counting star formulas. The idea of this alternative
form is roughly to replace a counting quantifier such as ∃=k x. F ′ with a spatial
conjunction of k formulas each of which has the meaning similar to ∃=1 x. F ′ , and
13

then combine a formula ∃=1 x. F1′ resulting from one counting star with a formula
∃=1 x. F2′ resulting from another counting star into the formula ∃=1 x. (F1′ ⊙ F2′ )
where ⊙ denotes merging of GCCAT formulas by taking the union of their positive literals. We next develop this idea in greater detail.
Notation for spatial representation of stars. Let GE (x1 , . . . , xn ) be the
unique GCCAT formula F with FV(F ) = {x1 , . . . , xn } such that the only positive
literals in F are literals xi = xi for 1 ≤ i ≤ n. Similarly, there is a unique formula
F ′ ∈ exts(x1 , . . . , xn , x) such that every atomic formula in F ′ distinct from for
x = x occurs in a negated literal. We call F ′ an empty extension and denote it
empEx(x1 , . . . , xn , x).
To compute a spatial conjunction of formulas C1 and C2 in the language L,
we temporarily consider formulas in an extended language L′ = L ∪ {B1 , B2 }
where B1 and B2 are two new unary predicates used to mark formulas. We use
B1 to mark formulas derived from C1 , and use B2 to mark formulas derived from
C2 . For m ∈ {∅, {1}, {2}, {1, 2}}, define
Mark∅ (x) = ¬B1 (x) ∧ ¬B2 (x)
Mark2 (x) = ¬B1 (x) ∧ B2 (x)

Mark1 (x) = B1 (x) ∧ ¬B2 (x)
Mark1,2 (x) = B1 (x) ∧ B2 (x)

Note that, when we say that F is a GCCAT formula, we mean that F is GCCAT
formula in language L (and thus F mentions symbols only from L), even when
we use F as a subformula of a larger formula in language L′ . Similarly, expressions exts(x1 , . . . , xn , x), empEx(F, x), and GE (x1 , . . . , xn ) all denote formulas in
language L.
On the other hand, empEx∅ (F, x) and empe are formulas in language L′ .
Formula empEx∅ (F, x) is an empty extension of F in language L′ . Formula empe
asserts that x1 , . . . , xn have an empty GCCAT formula and that the remaining
elements have empty extension in L′ . Formula empe does not constrain the values
B1 (xi ) and B2 (xi ), these values turn out to be irrelevant.
Let F ′ ∈ exts(x1 , . . . , xn , x). Define
empEx∅ (x1 , . . . , xn , x) ≡ empEx(x1 , . . . , xn , x) ∧ Mark∅ (x)
V
empe(x1 , . . . , xn ) ≡ GE (x1 , . . . , xn ) ∧ ∀x. ( n
i=1 x 6= xi ) ⇒ empEx∅ (x1 , . . . , xn , x)

We write empEx∅ (F, x) for empEx∅ (x1 , . . . , xn , x) if FV(F ) = {x1 , . . . , xn }, and
similarly for empe(F, x). We write simply empe if F and x are understood.
We next introduce formulas LF ′ M∗m and LF ′ Mm , which are the building blocks
for representing counting star formulas. Formula LF ′ M∗m means that F ′ marked
with m and empEx∅ (F, x) are the only extensions of F that hold in the neighborhood of x1 , . . . , xn (F ′ may hold for any number of neighbors). Formula
LF ′ Mm means that F ′ holds for exactly one element in the neighborhood of
x1 , . . . , xn , and all other neighbors have empty extensions. More precisely, let
F ′ ∈ exts(x1 , . . . , xn , x). Define
V
′
LF ′ M∗m ≡ GE (x1 , . . . , xn ) ∧ ∀x. ( n
i=1 x 6= xi ) ⇒ (F ∧ Markm (x)) ∨ empEx∅ (F, x)
Vn
′
LF ′ Mm ≡ LF ′ M∗m ∧ ∃=1 x.
i=1 x 6= xi ∧ F ∧ Markm (x)

where m ∈ {∅, {1}, {2}, {1, 2}}. Observe that G ⊛ empe ∼ G if G ≡ LF ′ M∗m or
G ≡ LF ′ Mm for some F ′ and m. Also note that LF ′ M∗m ⊛LF ′ M∗m ∼ LF ′ M∗m .
14

E ∧ F − EQCAT formula
F − GCCAT formula
Sm [[E ∧ F ∧ ∃s1 x.F1′ ∧ . . . ∧ ∃sk x.Fk′ ]] =
= E ∧ K[[F ]] ⊛ Xm [[∃s1 x.F1′ ]] ⊛ . . . ⊛ Xm [[∃sk x.Fk′ ]]
V
K[[F ]] = F ∧ (∀x. ( n
i=1 x 6= xi ) ⇒ empEx∅ (F, x))
Xm [[∃0 x. F ′ ]]
Xm [[∃

i+1

= empe
′

x. F ]] = LF ′ Mm ⊛ Xm [[∃i x. F ′ ]]

+

Xm [[∃i x. F ′ ]] = Xm [[∃i x. F ′ ]] ⊛LF ′ M∗m
Fig. 6. Translation of Counting Stars to Spatial Notation

Translation of counting stars. Figure 6 presents the translation of counting
stars to spatial notation. The idea of the translation is to replace ∃=k x. F ′ with
the spatial conjunction of k formulas LF ′ Mm ⊛ . . . ⊛LF ′ Mm where m ∈ {{1}, {2}}.
The purpose of the marker m is to ensure that each of the k witnesses for x that
are guaranteed to exist by LF ′ Mm ⊛ . . . ⊛LF ′ Mm are distinct. The reason that the
witnesses are distinct for m 6= ∅ is that no two of them can satisfy Bi (x) at the
same time for i ∈ m.
To show the correctness of the translation in Figure 6, define em to be the
L -environment obtained by extending L-environment e according to marking
m, and e1 to be the restriction of an L′ environment e1 to language L. More
precisely, if e is an environment in language L, for m ∈ {∅, {1}, {2}, {1, 2}},
define environment em in language L′ by 1) em r = e r for r ∈ L and 2) for
q ∈ {1, 2}, let (e Bq ) d = True ⇐⇒ q ∈ m ∧ d ∈
/ {e x1 , . . . , e xn }. Conversely,
if e1 is an environment in language L′ , define environment e1 in language L by
e1 r = e1 r for all r ∈ L. Lemma 13 below gives the correctness criterion for
translation in Figure 6.
′

Lemma 13. If e is an environment for language L, C a counting star formula
in language L, and m ∈ {{1}, {2}, {1, 2}}, then [[C]]e = Sm [[C]]em .

(1)
(2)
(3)
(4)
(5)
(6)

LT1 M1 ⊛LT2 M2 ; LT1 ⊙ T2 M1,2
LT1 M1 ⊛LT2 M∗2 ; LT1 ⊙ T2 M1,2 ⊛LT2 M∗2
LT1 M∗1 ⊛LT2 M2 ; LT1 M∗1 ⊛LT1 ⊙ T2 M1,2
LT1 M∗1 ⊛LT2 M∗2 ; LT1 M∗1 ⊛LT2 M∗2 ⊛LT1 ⊙ T2 M∗1,2
LT M∗1 ; empe
LT M∗2 ; empe

Fig. 7. Transformation Rules for Combining Spatial Conjuncts

15

Combining quantifier-free formulas. Let C1 ⊛ C2 be a spatial conjunction
of two counting-star formulas
′
′
C1 ≡ E ∧ F1 ∧ ∃s1,1 x.F1,1
∧ . . . ∧ ∃s1,k x.F1,k
′
′
C2 ≡ E ∧ F2 ∧ ∃s2,1 x.F2,1
∧ . . . ∧ ∃s2,k x.F2,l

where F1 and F2 are GCCAT formulas with FV(F1V
) = FV(F2 ) = {x1 , . . . , xn },
E ∧ F1 and E ∧ F2 are EQCAT formulas, and E ≡ m
j=1 yj = xij .
Note that we assume that the two GCCAT formulas F1 and F2 have same
free variables and that the equalities E in the two EQCAT formulas are the
same. This assumption is justified because either 1) C1 ⊛ C2 make inconsistent
assumptions about equalities among x1 , . . . , xn , and therefore C1 ⊛ C2 is equivalent to False, or 2) C1 ⊛ C2 make same assumptions about equalities among
x1 , . . . , xn , so we can rewrite C1 and C2 to satisfy the our assumption by exchanging variables xi and yj in the definition of an EQCAT formula.
To show how to transform formula S1 [[C1 ]] ⊛ S2 [[C2 ]] into a disjunction of
formulas of the form S1,2 [[C3 ]], we introduce the following notation. If T is a
formula, let S(T ) denote the set of positive literals in T1 that do not contain
equality. Let T1 ∈ exts(F1 , x) and T2 ∈ exts(F2 , x). (Note that exts(F1 , x) =
exts(F2 , x).) We define the partial operation T1 ⊙ T2 as follows. The result of
T1 ⊙ T2 is defined iff S(T1 ) ∩ S(T2 ) = ∅. If S(T1 ) ∩ S(T2 ) = ∅, then T1 ⊙ T2 = T
where T is the unique element of exts(F1 , x) such that S(T ) = S(T1 ) ∪ S(T2 ).
Similarly to ⊙, we define the partial operation F1 ⊕ F2 for F1 and F2 GCCAT
formulas with FV(F1 ) = FV(F2 ) = {x1 , . . . , xn }. The result of F1 ⊕ F2 is defined
iff S(F1 ) ∩ S(F2 ) = ∅. If S(F1 ) ∩ S(F2 ) = ∅, then F1 ⊕ F2 is the unique GCCAT
formula F such that FV(F ) = {x1 , . . . , xn } and S(F ) = S(F1 ) ∪ S(F2 ). The
following Lemma 14 notes that ⊙ and ⊕ are sound rules for computing spatial
conjunction of certain quantifier-free formulas.
Lemma 14. If T1 , T2 ∈ exts(x1 , . . . , xn , x) then T1 ⊛ T2 ∼ T1 ⊙ T2 . If F1 and
F2 are GCCAT formulas with FV(F1 ) = FV(F2 ) = {x1 , . . . , xn }, then F1 ⊛ F2 ∼
F1 ⊕ F2 .
Rules for transforming spatial conjuncts.
We transform formula
S1 [[C1 ]] ⊛ S2 [[C2 ]] into a disjunction of formulas of the form S1,2 [[C3 ]] as follows.
The first step in transforming C1 ⊛ C2 is to replace K[[F1 ]] ⊛ K[[F2 ]] with
K[[F1 ⊕ F2 ]] if F1 ⊕ F2 is defined, or False if F1 ⊕ F2 is not defined.
The second step is summarized in Figure 7, which presents rules for combining conjuncts resulting from X1 [[∃s1 .F1 ]] and X2 [[∃s2 x.F2 ]] into conjuncts of
the form X1,2 [[∃s x.F ]]. The intuition is that LT M∗m and LT Mm represent a finite
abstraction of all possible neighborhoods of x1 , . . . , xn , and the rules in Figure 7
represent the ways in which different portions of the neighborhoods combine using spatial conjunction. We apply the rules in Figure 7 modulo commutativity
and associativity of ⊛, the fact that emp is a unit for ⊛, as well as the idempotence of LT M∗m . Rules (1)−(4) are applicable only when the occurrence of T1 ⊙ T2
on the right-hand side of the rule is defined. We apply rules (1)−(4) as long as
possible, and then apply rules (5), (6). Moreover, we only allow the sequences of
16

rule applications that eliminate all occurrences of LT M1 , LT M∗1 , LT M2 , LT M∗2 , leaving
only LT M1,2 and LT M∗1,2 . Note also that the are only finitely many non-equivalent
expressions that can be obtained by sequences of applications of rules in Figure 7. Namely, an application of rules (1)–(3) decreases the total number of
spatial conjuncts of the form LT M1 and LT M2 , multiple applications of rule (4) to
the same pair of spatial conjuncts are unnecessary because of the idempotence
of LT1 ⊙ T2 M∗1,2 (so we never perform them), and rules (5), (6) reduce the total
number of spatial conjuncts. The following Lemma 15 gives partial correctness
of rules in Figure 7.
Lemma 15. If G1 ; G2 , then G2 ⇒ G1 is valid.
C

Define G1 =⇒ G2 to hold iff both of the following two conditions hold: 1)
G2 results from G1 by replacing K[[F1 ]] ⊛ K[[F2 ]] with K[[F1 ⊕ F2 ]] if F1 ⊕ F2 is
defined, or False if F1 ⊕ F2 is not defined, and then applying some sequence of
rules in Figure 7 such that rules (5), (6) are applied only when rules (1)−(4)
are not applicable; 2) G2 contains only spatial conjuncts of the form LT M1,2 and
LT M∗1,2 . From Lemma 15 and Lemma 14 we immediately obtain Lemma 16.
C

Lemma 16. If G1 =⇒ G2 , then G2 ⇒ G1 is valid.
The rule for computing the spatial conjunction of counting star formulas is the
following. If C1 , C2 , and C3 are counting star formulas, define R(C1 , C2 , C3 ) to
C

hold iff S1 [[C1 ]] ⊛ SW
2 [[C2 ]] =⇒ S1,2 [[C3 ]]. We compute spatial conjunction by replacing C1 ⊛ C2 with R(C1 ,C2 ,C3 ) C3 . Our goal is therefore to show the equivalence
C1 ⊛ C2

_

∼

C3

(3)

R(C1 ,C2 ,C3 )

W
The validity of R(C1 ,C2 ,C3 ) C3 ⇒ (C1 ⊛ C2 ) follows from Lemma 16 and
Lemma 13.
W
Lemma 17. ( R(C1 ,C2 ,C3 ) C3 ) ⇒ (C1 ⊛ C2 ) is a valid formula for every pair of
counting star formulas C1 and C2 .
We next consider the converse claim. If [[C1 ⊛ C2 ]]e, then there are e1 and e2 such
that split e e1 e2 , [[C1 ]]e1 , and [[C2 ]]e2 . By considering the atomic types induced
in e, e1 and e2 by elements in D \ {e x1 , . . . , e xn }, we construct a sequence
of ; transformations in Figure 7 that convert S1 [[C1 ]] ⊛ S2 [[C2 ]] into a formula
S1,2 [[C3 ]] such that [[C3 ]]e = True.
W
Lemma 18. C1 ⊛ C2 ⇒ R(C1 ,C2 ,C3 ) C3 is a valid formula for every pair of
counting star formulas C1 and C2 .
From Lemma 17 and Lemma 18 we obtain the desired Theorem 19, which
shows the correctness of our rules for computing spatial conjunction of formulas
of quantifier depth at most one.
Theorem 19. The equivalence (3) holds for every pair of counting star formulas
C1 and C2 .
17

8

Further Remarks

In this section we present two additional remarks regarding spatial conjunction.
The first remark notes that we must be careful when extracting a subformula
from a formula and labelling it with a new predicate. The second remark shows
how to encode spatial conjunction in second-order logic, thus providing some
insight into the expressive power of spatial conjunction.
8.1

Extracting Subformulas in the Presence of ⊛

In two-variable logic with counting C 2 we may efficiently transform formula into
an unnested form by introducing new predicate names and naming subformulas
using these predicates. This transformations is a standard step in decidability
proofs for two-variable logic with counting [22, 45].
The satisfiability of the resulting formula is equivalent to the satisfiability of
the original formula. An extraction of a subformula G and its replacement with
a new predicate P can be justified by a substitution lemma of the form:
[[F [P := G]]]e = [[F ]](e[P := [[G]]e])
where e is the environment (model). This substitution lemma does not hold in
the presence of spatial conjunction that splits the values of newly introduced
predicates. Namely,
[[(F1 ⊛ F2 )[P := G]]]e ⇒ [[F1 ⊛ F2 ]](e[P := [[G]]e])
holds, but the converse implication does not hold because the value [[G]]e of the
relation P might be split on the right-hand side.
It is therefore interesting to divide predicates into splittable and non-splittable
predicates, and have spatial conjunction split only the interpretations of splittable predicates. The substitution lemma then holds when P is a non-splittable
predicate.
Note, however, that in the presence of non-splittable predicates we cannot
translate counting stars into spatial notation and thus use unnested form to
eliminate all spatial conjunctions from first-order formulas. As a result, adding
spatial conjunction of formulas of large quantifier depth to two-variable logic
with counting may increase the expressive power of the resulting logic.
We also remark that if the language contains only one splittable unary predicate AS , then it is easy to simulate the splitting of objects of the universe, which
is the semantics of spatial conjunction in [28]. Namely, we use some fixed unary
predicate A0 to denote all “live” objects, and make all quantifiers range only
over the objects that satisfy A0 .
8.2

Representing ⊛ in Second-Order Logic

In this section we give a simple translation from the first-order logic with spatial
conjunction and inductive definitions [27, Chapter 4] to second-order logic. This
18

gives an upper bound on the expressive power of first-order logic with spatial
conjunction and inductive definitions.
Consider first-order logic extended with the spatial conjunction ⊛ and the
least-fixpoint operator. The syntax of the least-fixpoint operator is
(lfp P, x1 , . . . , xn .F )(y1 , . . . , yn )
where F is a formula that may contain new free variables P, x1 , . . . , xn . The
meaning of the least-fixpoint operator is that the relation which is the least
fixpoint of the monotonic transformation on predicates
(λx1 , . . . , xn .P (x1 , . . . , xn )) 7→ (λx1 , . . . , xn .F )
holds for y1 , . . . , yn . To ensure the monotonicity of the transformation on predicates, we require that P occurs only positively in F .

A = {A1 , . . . , An }
F = {f1 , . . . , fm }
′
[[F ′ ⊛ F ′′ ]] = ∃ A′1 , . . . , A′n , f1′ , . . . , fm
,

′

′′

′′
A′′1 , . . . , A′′n , f1′′ , . . . , fm
. B[[F ′ ⊛ F ′′ ]]

B[[F ⊛ F ]] =
n
m
V
V
(split1 Ai A′i A′′i ) ∧
(split2 fi fi′ fi′′ ) ∧
i=1
′

i=1

′ m
[[F ]][Ai := A′i ]n
i=1 [fi := fi ]i=1 ∧

′′ m
[[F ′′ ]][Ai := A′′i ]n
i=1 [fi := fi ]i=1

split1 A A′ A′′ ≡ ∀x. (A(x) ⇔ (A′ (x) ∨ A′′ (x))) ∧
¬(A′ (x) ∧ A′′ (x))
split2 f f ′ f ′′ ≡ ∀x y. (f (x, y) ⇔ (f ′ (x, y) ∨ f ′′ (x, y))) ∧
¬(f ′ (x, y) ∧ f ′′ (x, y))
[[(lfp P, x1 , . . . , xn .F )(y1 , . . . , yn )]] =
∀P. (∀x1 , . . . , xn . (F ⇔ P (x1 , . . . , xn ))) ⇒ P (y1 , . . . , yn )
Fig. 8. Translation of Spatial Conjunction and Inductive Definitions into Second-Order
Logic

Figure 8 presents the translation from first-order logic extended with spatial
conjunction and least-fixpoint operator to second-order logic. The translation
directly mimics the semantics of ⊛ and lfp.
In second-order logic, the relations in L = A ∪ F become free variables.
19

To translate ⊛, use second-order quantification to assert the existence of
new unary and binary relations that partition the relations in L into relations
in L′ and L′′ . Then perform a syntactic replacement of relations in L with the
corresponding relations in L′ for the first formula, and with the corresponding
relations in L′′ for the second formula.
Translating lfp is also straightforward. The property that P is a fixpoint of
F is easily expressible. To encode that y1 , . . . , yn hold for the least fixpoint of F ,
we state that y1 , . . . , yn hold for all fixpoints of F , using universal second-order
quantification over P .
We also note that the translation of ⊛ in Figure 8 uses only existential
second-order quantification, which points to another class of formulas where
spatial conjunction can be eliminated if we are only concerned with satisfiability.
Namely, if F ′ and F ′′ are first-order formulas (without ⊛ or lfp), then F ′ ⊛ F ′′
is satisfiable iff the first-order formula B[[F ′ ⊛ F ′′ ]] in the extended language is
satisfiable. As a slight generalization, define the following class of “interesting”
formulas:
1. a first-order formula F is an interesting formula;
2. if F1 and F2 are interesting formulas, so is F1 ⊛ F2 ;
3. if F1 and F2 are interesting formulas, so is F1 ∨ F2
The satisfiability of each interesting formula is equivalent to the satisfiability of
the corresponding first-order formula in an extended vocabulary. In particular,
the satisfiability of the class of formulas formed starting from formulas in twovariable logic with counting and applying only ∨ and ⊛ is decidable.

9

Further Related Work

Records have been studied in the context of functional and object-oriented programming languages [11, 14, 23, 29, 42, 46–48, 57]. The main difference between
existing record notations and our system is that the interpretation of a record in
our system is a predicate on an object, where an object is linked to other objects
forming a graph, as opposed to being a type that denotes a value (with values
typically representable as finite trees). Our view is appropriate for programming
languages such as Java and ML that can manipulate structures using destructive updates. Our generalizations allow the developers to express both incoming
and outgoing references of objects, and allow the developers to express typestate
changes.
We have developed role logic to provide a foundation for role analysis [30–33].
We have subsequently studied a simplification of role analysis constraints and
showed a characterization of such constraints using formulas [34, 35]. Multifields
and multislots are present already in [32, Section 8.1]. In this section we have
shown that role logic provides a unifying framework for all these constraints
and goes beyond them in 1) being closed under the fundamental boolean logical
operations, and, 2) being closed under spatial conjunction for an interesting class
20

of formulas. The view of roles as predicates is equivalent to the view of roles as
sets and works well in the presence of data abstraction [39, 40].
The parametric analysis based on there-valued logic was introduced in [53,
54]. Other approaches to verifying shape invariants include [13, 19–21, 26, 41]. A
decidable logic for expressing connectivity properties of the heap was presented
in [4]. We use spatial conjunction from separation logic that has been used for
reasoning about the heap [7, 8, 28, 51, 52]. Description logics [1, 6] share many
of the properties of role logic and have been traditionally applied to knowledge
bases. [9, 10] present doubly-exponential deterministic algorithms for reasoning
about the satisfiability of expressive description logics over all structures and
over finite structures. The decidability of two-variable logic with counting C 2
was shown in [22], whereas [45] establishes the NEXPTIME-complexity of the
satisfiability problem for the fragment C12 with counting up to one.

10

Conclusions

We have shown how to add notation for records to two-variable role logic while
preserving its decidability. The resulting notation supports a generalization of
traditional records with record specifications that are closed under all boolean
operations as well as record concatenation, allow the description of typestate
properties, support inverse records, and capture the distinction between open
and closed records. We believe that such an expressive and decidable notation is
useful as an annotation language used with program analyses and type systems.
Acknowledgements. We thank the participants of the Dagstuhl Seminar
03101 “Reasoning about Shape” for useful discussions on separation logic and
shape analysis.

References
1. Franz Baader, Diego Calvanese, Deborah McGuinness, Daniele Nardi, and Peter PatelSchneider, editors. The Description Logic Handbook: Theory, Implementation and Applications. Cambridge University Press, 2003.
2. Thomas Ball, Rupak Majumdar, Todd Millstein, and Sriram K. Rajamani. Automatic
predicate abstraction of C programs. In Proc. ACM PLDI, 2001.
3. Thomas Ball, Andreas Podelski, and Sriram K. Rajamani. Relative completeness of abstraction refinement for software model checking. In TACAS’02, volume 2280 of LNCS,
page 158, 2002.
4. Michael Benedikt, Thomas Reps, and Mooly Sagiv. A decidable logic for linked data
structures. In Proc. 8th ESOP, 1999.
5. Lars Birkedal, Noah Torp-Smith, and John C. Reynolds. Local reasoning about a copying
garbage collector. In 31st ACM POPL, pages 220–231. ACM Press, 2004.
6. Alexander Borgida. Description logics in data management. IEEE Trans. on Knowledge
and Data Engineering, 7(5):671–682, 1995.
7. Cristiano Calcagno, Luca Cardelli, and Andrew D. Gordon. Deciding validity in a spatial
logic for trees. In ACM TLDI’02, 2002.
8. Cristiano Calcagno, Samin Ishtiaq, and Peter W. O’Hearn. Semantic analysis of pointer
aliasing, allocation and disposal in hoare logic. In Proc. 2nd International Conference on
Principles and Practice of Declarative Programming, 2000.

21

9. Diego Calvanese. Finite model reasoning in description logics. In Proc. of the 5th Int. Conf.
on the Principles of Knowledge Representation and Reasoning (KR’96), pages 292–303.
Morgan Kaufmann, 1996.
10. Diego Calvanese. Unrestricted and Finite Model Reasoning in Class-Based Representation
Formalisms. PhD thesis, Dipartimento di Informatica e Sistemistica, Universita di Roma
”La Sapienza”, 1996.
11. Luca Cardelli and John C. Mitchell. Operations on records. In Theoretical Aspects of
Object-Oriented Programming. The MIT Press, Cambridge, Mass., 1994.
12. C. C. Chang and H. J. Keisler. Model Theory. North Holland, 1990.
13. David R. Chase, Mark Wegman, and F. Kenneth Zadeck. Analysis of pointers and structures. In Proc. ACM PLDI, 1990.
14. David R. Cheriton and Michael E. Wolf. Extensions for multi-module records in conventional programming languages. In Proceedings of the 14th ACM SIGACT-SIGPLAN
symposium on Principles of programming languages, pages 296–306. ACM Press, 1987.
15. Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for
static analysis of programs by construction or approximation of fixpoints. In Proc. 4th
POPL, 1977.
16. Robert DeLine and Manuel Fähndrich. Enforcing high-level protocols in low-level software.
In Proc. ACM PLDI, 2001.
17. Robert DeLine and Manuel Fähndrich. Typestates for objects. In Proc. 18th ECOOP,
June 2004.
18. Manuel Fähndrich and K. Rustan M. Leino. Declaring and checking non-null types in an
object-oriented language. In OOPSLA’03, 2003.
19. Pascal Fradet and Daniel Le Métayer. Shape types. In Proc. 24th ACM POPL, 1997.
20. Pascal Fradet and Daniel Le Métayer. Structured gamma. Science of Computer Programming, SCP, 31(2-3), pp. 263-289, 1998.
21. Rakesh Ghiya and Laurie J. Hendren. Putting pointer analysis to work. In Proc. 25th
ACM POPL, 1998.
22. Erich Grädel, Martin Otto, and Eric Rosen. Two-variable logic with counting is decidable. In Proceedings of 12th IEEE Symposium on Logic in Computer Science LICS ‘97,
Warschau, 1997.
23. Robert Harper and Benjamin Pierce. A record calculus based on symmetric concatenation.
In 18th ACM POPL, pages 131–142, Orlando, Florida, 1991.
24. Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Kenneth L. McMillan. Abstractions from proofs. In 31st POPL, 2004.
25. Wilfrid Hodges. Model Theory, volume 42 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1993.
26. Joseph Hummel, Laurie J. Hendren, and Alexandru Nicolau. A general data dependence
test for dynamic, pointer-based data structures. In Proc. ACM PLDI, 1994.
27. Neil Immerman. Descriptive Complexity. Springer-Verlag, 1998.
28. Samin Ishtiaq and Peter W. O’Hearn. BI as an assertion language for mutable data
structures. In Proc. 28th ACM POPL, 2001.
29. Mark Jones and Simon Peyton Jones. Lightweight extensible records for Haskell. In
Haskell Workshop, 1999.
30. Viktor Kuncak. Designing an algorithm for role analysis. Master’s thesis, MIT Laboratory
for Computer Science, 2001.
31. Viktor Kuncak, Patrick Lam, and Martin Rinard. A language for role specifications. In
Proceedings of the 14th Workshop on Languages and Compilers for Parallel Computing,
volume 2624 of Lecture Notes in Computer Science, Springer, 2001.
32. Viktor Kuncak, Patrick Lam, and Martin Rinard. Roles are really great! Technical Report
822, Laboratory for Computer Science, Massachusetts Institute of Technology, 2001.
33. Viktor Kuncak, Patrick Lam, and Martin Rinard. Role analysis. In Proc. 29th POPL,
2002.
34. Viktor Kuncak and Martin Rinard. Typestate checking and regular graph constraints.
Technical Report 863, MIT Laboratory for Computer Science, 2002.

22

35. Viktor Kuncak and Martin Rinard. Existential heap abstraction entailment is undecidable. In 10th Annual International Static Analysis Symposium (SAS 2003), San Diego,
California, June 11-13 2003.
36. Viktor Kuncak and Martin Rinard. On role logic. Technical Report 925, MIT CSAIL,
2003.
37. Viktor Kuncak and Martin Rinard. On the boolean algebra of shape analysis constraints.
Technical report, MIT CSAIL, August 2003.
38. Viktor Kuncak and Martin Rinard. Boolean algebra of shape analysis constraints. In
Proc. 5th International Conference on Verification, Model Checking and Abstract Interpretation, 2004.
39. Patrick Lam, Viktor Kuncak, and Martin Rinard. On modular pluggable analyses using
set interfaces. Technical Report 933, MIT CSAIL, December 2003.
40. Patrick Lam, Viktor Kuncak, and Martin Rinard. Generalized typestate checking using
set interfaces and pluggable analyses. SIGPLAN Notices, 39:46–55, March 2004.
41. Anders Møller and Michael I. Schwartzbach. The Pointer Assertion Logic Engine. In Proc.
ACM PLDI, 2001.
42. Wolfgang Naraschewski and Markus Wenzel. Object-oriented verification based on record
subtyping in higher-order logic. In 11th TPHOLs, volume 1479 of LNCS, pages 349–366,
1998.
43. Peter O’Hearn, John Reynolds, and Hongseok Yang. Local reasoning about programs that
alter data structures. In Proc. CSL, Paris 2001, volume 2142 of LNCS, 2001.
44. Martin Otto. Bounded Variable Logics and Counting: A Study in Finite Models. Lecture
Notes in Logic 9. Springer, 1997.
45. Leszek Pacholski, Wieslaw Szwast, and Lidia Tendera. Complexity results for first-order
two-variable logic with counting. SIAM J. on Computing, 29(4):1083–1117, 2000.
46. Francois Pottier. A constraint-based presentation and generalization of rows. In 18th
IEEE LICS, June 2003.
47. Didier Remy. Typechecking records and variants in a natural extension of ml. In POPL,
pages 77–88, 1989.
48. Didier Remy. Typing record concatenation for free. In POPL, pages 166–176, 1992.
49. Thomas Reps, Mooly Sagiv, and Alexey Loginov. Finite differencing of logical formulas
for static analysis. In Proc. 12th ESOP, 2003.
50. Thomas Reps, Mooly Sagiv, and Greta Yorsh. Symbolic implementation of the best transformer. In Proc. 5th International Conference on Verification, Model Checking and Abstract Interpretation, 2004.
51. John C. Reynolds. Intuitionistic reasoning about shared mutable data structure. In
Proceedings of the Symposium in Celebration of the Work of C.A.R. Hoare, 2000.
52. John C. Reynolds. Separation logic: a logic for shared mutable data structures. In 17th
LICS, pages 55–74, 2002.
53. Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Parametric shape analysis via 3valued logic. In Proc. 26th ACM POPL, 1999.
54. Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Parametric shape analysis via 3valued logic. ACM TOPLAS, 24(3):217–298, 2002.
55. Robert E. Strom and Daniel M. Yellin. Extending typestate checking using conditional
liveness analysis. IEEE Transactions on Software Engineering, May 1993.
56. Robert E. Strom and Shaula Yemini. Typestate: A programming language concept for
enhancing software reliability. IEEE TSE, January 1986.
57. Mitchell Wand. Type inference for record concatenation and multiple inheritance. Information and Computation, 93(1):1–15, 1991.
58. Eran Yahav and Ganesan Ramalingam. Verifying safety properties using separation and
heterogeneous abstractions. In PLDI, 2004.
59. Greta Yorsh, Thomas Reps, and Mooly Sagiv. Symbolically computing most-precise abstract operations for shape analysis. In 10th TACAS, 2004.

23

A

Appendix: Correctness of Spatial Conjunction
Elimination

Proposition 8. Every quantifier-free formula F such that FV(F ) ⊆ {x1 , . . . , xn }
is equivalent to a disjunction of CAT formulas C such that FV(C) = {x1 , . . . , xn }.
Proof. Let F be a quantifier-free formula and FV(F ) ⊆ {x1 , . . . , xn }. Transform
F to disjunctive normal form F ′ . Let C be a conjunction in F ′ . If C contains
a literal and its negation, then C is contradictory and we eliminate C from F ′ .
Assume all conjunctions are non-contradictory, and let C be one conjunction. If
there exists an atomic formula FA in variables {x1 , . . . , xn } such that FA ∈
/ C
and (¬FA ) ∈
/ C, then replace C with the disjunction
(C ∧ FA ) ∨ (C ∧ ¬FA )

By repeating this process, we obtain a disjunction of CAT formulas.
Lemma 9. Every CAT formula F is either contradictory, or is equivalent to an
EQCAT formula F ′ such that FV(F ′ ) = FV(F ).
Proof. Let F be a CAT formula. If xi 6= xi occurs in F , then F is contradictory.
If xi = xj occurs in F for i 6≡ j, then in all conjuncts other than xi = xj
replace all occurrences of xi with xj . Repeat this process as long as it is possible.
Suppose that the resulting formula was not established to be contradictory. Let
y1 , . . . , ym be variables that occur only on the left-hand side of some equality
yj = xij . Removing all equalities of the form yj = yj yields an EQCAT formula.
Proposition 10.
Every quantifier-free formula F such that FV(F ) ⊆
{x1 , . . . , xn } can be written as a disjunction of EQCAT formulas C such that
FV(C) = {x1 , . . . , xn }.
Proof. Let F be a quantifier-free formula such that FV(F ) ⊆ {x1 , . . . , xn }. Using
Proposition 8, transform F to disjunction of CAT formulas F1 . Then, for each
conjunct C of F1 apply Lemma 9 to transform C to an EQCAT formula.
Proposition 12. Let F be a formula of such that F has quantifier depth
at most one, F has counting degree at most k, and FV(F ) ⊆ {x1 , . . . , xn }.
Then F is equivalent to a disjunction of k-counting-star formulas FC where
FV(FC ) = {x1 , . . . , xn }.
Proof. Let F be a formula of such that F has quantifier depth at most one, F
has counting degree at most k, and FV(F ) ⊆ {x1 , . . . , xn }. Then F is a boolean
combination of 1) atomic formulas and 2) formulas of the form ∃s z. F ′ where F ′
is quantifier-free and FV(F ′ ) = {z, x1 , . . . , xn }. Because z is a bound variable,
rename it to x in each formula F ′ . Let F1 be the result of transforming this
boolean combination to disjunctive normal form. Consider a disjunct C of F1 .
As in the proof of Proposition 10, and treating quantified formulas as atomic
syntactic entities, transform C into disjunction of formulas of the form
m
^
j=1

yj = wij ∧ F ∧

^
F ′ ∈S

24

′

(∃β(F ) x. F ′ )α(F

′

)

V
where β(F ′ ) ∈ Ck+1 , α(F ′ ) ∈ {0, 1} for F ′ ∈ S, and where m
j=1 yj = wij ∧ F
is an EQCAT formula with y1 , . . . , ym , w1 , . . . , wp distinct variables such that
{y1 , . . . , ym , w1 , . . . , wp } = {x1 , . . . , xn }, and FV(F ′ ) ⊆ {x, x1 , . . . , xn } for F ′ ∈
′
S. Here S is the set of formulas of the form ∃β(F ) x. F ′ that end up conjoined
with the EQCAT formula as the result of transformation to normal form. By
replacing each yj with wij in each F ′ , enforce that FV(F ′ ) ⊆ {x, w1 , . . . , wp }.
Using Proposition 10, transform each F ′ to a disjunction of EQCAT formulas.
By applying the equivalences
∃≥k1 x.

q
W

Bi ∼

i=1

∃=k1 x.

q
W

q
P

j=1

Bi ∼

i=1

q
P

W
lj =k1

W
lj =k1

q
V

∃≥li x. Bi

q
V

∃=li x. Bi

i=1

i=1

j=1

for B1 , . . . , Bq mutually exclusive, and propagating the disjunction to the top
level, ensure that every F ′ is an EQCAT formula. Then transform each term
′
′
(∃β(F ) x. F ′ )α(F ) into positive boolean combination of formulas of one of the
forms ∃=i x. F ′ for 0 ≤ i ≤ k and ∃≥k+1 x. F ′ , using the properties
¬∃≥k1 x. F ′ ∼
¬∃=k1 x. F ′ ∼

k1W
−1
i=0

∃=i x. F ′
W

∃=i x. F ′ ∨ ∃≥k+1 x. F ′

i∈{0,...,k}\{k1 }

Next ensure that each F ′ is not merely an EQCAT, but in fact a GCCAT such
that F ′ ∈ exts(F, x), as follows.
Suppose that F ′ contains a literal L1 complementary to some literal occurring
in GCCAT formula F . If L1 occurs in ∃=i x. F ′ for i > 0 or in ∃≥k+1 x. F ′ , then
the entire conjunct is contradictory and we eliminate it. If L1 occurs in ∃=0 x. F ′ ,
then ∃=0 x. F ′ is implied by F , so eliminate it. Assume that F ′ has no literals
complementary to literals in F . Then F ′ contains wi 6= wj for all i 6≡ j. Next
ensure that x 6= wi is a conjunct for 1 ≤ i ≤ p, as follows. Suppose that F ′
contains the conjunct x = wi for some 1 ≤ i ≤ p.
There is clearly at most one interpretation of x that is equal to interpretation
+
of wi , so if β(F ′ ) ∈ {2, 3, . . . , k, (k + 1) } then F and F ′ are contradictory and
the entire conjunction is False, so assume β(F ′ ) ∈ {0, 1}. For the same reason,
∃=1 x. F ′ is equivalent to ∃x.F ′ , so if β(F ′ ) = 1, then replace x with wi in
F ′ giving a GCCAT formula F ′′ such that FV(F ′′ ) = FV(F ). By definition of
GCCAT formulas, either F and F ′′ are equivalent, so F ∧ (∃x.F ′′ ) ∼ F , or F
and F ′′ are contradictory, and the entire conjunction is False.
Assume therefore that x 6= wi occurs in F ′ for all 1 ≤ i ≤ p. This means that
′
F is a GCCAT formula. Because FV(F ′ ) = {x, w1 , . . . , wp } and F ′ does not
contain a literal complementary to a literal from F , eliminating from F ′ atomic
formulas that occur in F yields an element of exts(F, x).
25

To ensure that there exists exactly one conjunct of the form ∃s x. F ′ for each
F ∈ exts(F, x), use the fact that the k + 1 formulas ∃=i x. F ′ , for 0 ≤ i ≤ k, and
∃≥k+1 x. F ′ form a partition (they are mutually exclusive and their disjunction
is True).
′

Lemma 13. If e is an environment for language L, C a counting star formula
in language L, and m ∈ {{1}, {2}, {1, 2}}, then [[C]]e = Sm [[C]]em .
Proof. Formula E contains only equalities, so [[E]]e iff [[E]]em . It therefore suffices
to show that
[[K[[F ]] ⊛ Xm [[∃s1 x.F1′ ]] ⊛ . . . ⊛ Xm [[∃sk x.Fk′ ]]]]em = True

(4)

iff [[F ]]e = True and for all i, [[∃si x.Fi′ ]]e = True.
⇒): Let (4) hold. Then there exist e0 , e1 , . . . , ek such that split em [e0 e1 . . . ek ],
[[K[[F ]]]]e0 = True, and [[Xm [[∃si x.Fi′ ]]]]ei = True for 1 ≤ i ≤ k.
We first show [[F ]]e = True. Note first that [[GE ]]ei = True for 1 ≤ i ≤ k.
Namely, because both LF ′ M∗m and LF ′ Mm entail GE , so does Xm [[∃si x.Fi′ ]], by
definition of Xm [[]] and split. Therefore, e0 is the only environment among
e0 , e1 , . . . , ek that may have non-empty relations between the elements interpreting x1 , . . . , xn . As a result, [[F ]]em = [[F ]]e0 . But [[F ]]e0 = True because
[[K[[F ]]]]e0 = True. Therefore [[F ]]em = True, and F contains no symbols from
L′ \ L, so [[F ]]e = True.
We next show [[∃si x.Fi′ ]]e = True for 1 ≤ i ≤ k. For si = p+ , from
[[Xm [[∃si x.Fi′ ]]]]ei = True we have that there exist ei,0 , ei,1 , . . . , ei,p such that
1) split ei [ei,0 , ei,1 , . . . , ei,p ], 2) [[LF ′ M∗m ]]ei,0 = True, and 3) [[LF ′ Mm ]]ei,j = True
for 1 ≤ j ≤ p. Similarly, for si < p, we have that there exist ei,1 , . . . , ei,si
such that 1) split ei [ei,1 , . . . , ei,si ], and 2) [[LF ′ Mm ]]ei,j = True for 1 ≤ j ≤ si .
Note that whenever [[LF ′ M∗m ]]ei,j or [[LF ′ Mm ]]ei,j holds, we can split elements of
the domain D into two disjoint sets: elements Ei,j for which empEx∅ (F, x)
holds, and elements Ni,j for which F ′ ∧ Markm (x) holds. If [[LF ′ Mm ]]ei,j , then
|Ni,j | = 1, by definition of [[LF ′ Mm ]]ei,j . Moreover, by definition of split and
6 hi2 , j2 i. Observe
because m 6= ∅, we have Ni1 ,j1 ∩ Ni2 ,j2 = ∅ for hi1 , j1 i =
that, for a given domain element d ∈ D, the atomic type extension corresponding to em with x 7→ d is the union of atomic type extensions corresponding
to each ei,j . The atomic type extension for d in ei,j is either F ′ ∧ Markm (x),
or empEx∅ (F, x). Therefore, the atomic type extension for d in em is either
F ′ ∧ Markm (x) if d ∈ Ni,j for some i, j, or empEx∅ (F,
/ Ni,j .
U x) if for all i, j, d ∈
If Ni = {d | [[Fi′ ]]em [x 7→ d] = True}, then Ni = j Ni,j . If si = k < p then
Psi
Psi
1 = si , so [[∃=k x. Fi′ ]]em = True. Because ∃=k x. Fi′
|Ni,j | = i=j
|Ni | = j=1
=k
′
is formula in language
if si = p+ ,
PpL, we have [[∃ x. Fi ]]e = True.≥kSimilarly,
′ m
then |Ni | = |Ni,0 | + j=1 |Ni,j | = |Ni,0 | + p ≥ p, so [[∃ x. Fi ]]e = True and
therefore [[∃≥p x. Fi′ ]]e = True. In both cases, [[∃si x. Fi′ ]]e = True.
This completes one direction of the implication, we next show the converse
direction.
⇐): Let [[F ]]e = True and for all i where 1 ≤ i ≤ k, [[∃si x.Fi′ ]]e = True.
We construct environments e0 , e1 , . . . , ek such that 1) split em [e0 , e1 , . . . , ek ] 2)
26

[[K[[F ]]]]e0 = True, and 3) [[Xm [[∃si x.Fi′ ]]]]ei = True for all i where 1 ≤ i ≤ k.
We construct e0 , e1 , . . . , ek by assigning the tuples of relations in e to one of
the environments e0 , e1 , . . . , ek , as follows. We only need to decide on splitting
the tuples hd1 , . . . , dq i where all but one value d1 , . . . , dq are from the set DX =
{ex1 , . . . , exn }, the values of relations on other tuples do not affect the truth
value of formulas in question and can be split arbitrarily. If {d1 , . . . , dq } ⊆ DX ,
then we assign the tuple to e0 , as a result, [[K[[F ]]]]e0 = True. If {d1 , . . . , dq }\DX =
{d}, then let i be such that Fi′ is the unique extension of F with the property
[[Fi′ ]]e[x 7→ d] = True. Then assign the tuple hd1 , . . . , dq i to the environment ei
and also assign the values (e Bl ) d for all l ∈ m to ei . Because we assign each
relevant tuple to exactly one ei , we ensure split em [e0 , e1 , . . . , ek ]. Let DE = {d |
[[Fi′ ]]e[x 7→ d] = True}, then also DE = {d | [[Fi′ ]]ei [x 7→ d] = True}. Because
[[∃si x.Fi′ ]]e = True, |DE | = si for si < p and |DE | ≥ p for si = p+ . Let si < p.
Then split ei into ei,1 , . . . , ei,si by assigning exactly one element d ∈ DE to one
ei,j . When assigning an element we assign the values of all relations from L, as
well as the relations B1 and B2 . This ensures that [[LFi′ Mm ]]ei,j = True for all
1 ≤ i ≤ si . For si = p+ , we split ei into ei,0 , ei,1 , . . . , ei,p by assigning exactly
one element to each of ei,1 , . . . , ei,p and assigning the remaining elements to ei,0 .
In both cases, we obtain [[Xm [[∃si x.Fi′ ]]]]ei = True.
Lemma 15. If G1 ; G2 , then G2 ⇒ G1 is valid.
Proof. We show the claim for each of the rules (1)–(6).
Rule (1): Let T1 ⊙ T2 be defined and let [[LT1 ⊙ T2 M1,2 ]]e = True for an L′ environment e. Let d ∈ D be the unique domain element such that [[T1 ⊙T2 ]]e[x 7→
d] = True. Let e1 and e2 be such that split e [e1 , e2 ], [[T1 ]]e1 [x 7→ d] = True and
[[T2 ]]e2 [x 7→ d] = True, and ep Bq d = True iff p = q for p, q ∈ {1, 2}. In other
words, e1 and e2 split e by assigning tuples validating T1 to e1 , tuples validating
T2 to e2 , and by assigning B1 to e1 and B2 to e2 on the element d. The values
of relations e r containing tuples with an element d′ ∈
/ {ex1 , . . . , exn , d} are all
False, because [[LT1 ⊙ T2 M1,2 ]]e = True, so we let the values of e1 r and e2 r for those
tuples also be empty. Then d is the only element outside {ex1 , . . . , exn } such that
[[T1 ]]e1 [x 7→ d] = True, and d is also the only element outside {ex1 , . . . , exn } such
that [[T2 ]]e2 [x 7→ d] = True. As a result, [[LT1 M1 ]]e1 = True and [[LT2 M2 ]]e2 = True,
so [[LT1 M1 ⊛LT2 M2 ]]e = True.
To show the claim for rules (2), (3), (4), we proceed similarly as for rule (1).
Rule (2): Let T1 ⊙ T2 be defined and let [[LT1 ⊙ T2 M1,2 ⊛LT2 M∗2 ]]e = True.
Then there are e′ and e′′ such that split e [e′ , e′′ ], [[LT1 ⊙ T2 M1,2 ]]e′ = True and
[[LT2 M∗2 ]]e′′ = True. Let d be the unique element such that [[T1 ⊙ T2 ]]e′ [x 7→
d] = True, and let d1 , . . . , dk be the list of all (distinct) elements such that
/ {d1 , . . . , dk }, because e′ B2 d = True,
[[LT2 M∗2 ]]e′′ [x 7→ di ] = True. Note that d ∈
′′
e B2 di = True for all 1 ≤ i ≤ k, and split e [e′ , e′′ ]. We construct e1 and e2 such
that split e [e1 , e2 ] as follows. We assign B1 , as well as the values of relations that
hold according to T1 on element d to e1 , and we assign B2 , as well as the values
of relations that hold according to T2 on element d to e2 . We assign B2 as well as
the values of relations that hold according to T2 on d1 , . . . , dk to e2 . The values
27

of B1 and the relations on d1 , . . . , dk for e1 are empty. For such e1 and e2 we
have [[LT1 M1 ]]e1 = True and [[LT2 M∗2 ]]e2 = True, so [[LT1 M1 ⊛LT2 M∗2 ]]e = True.
Rule (3) is analogous to rule (2).
Rule (4): Let T1 ⊙ T2 be defined and let [[LT1 M∗1 ⊛LT2 M∗2 ⊛LT1 ⊙ T2 M∗1,2 ]] = True.
Then there are e′ ,e′′ , e′′′ such that split e [e′ , e′′ , e′′′ ], [[LT1 M∗1 ]]e′ = True, [[LT2 M∗2 ]]e′′ =
True, and [[LT1 ⊙ T2 M∗1,2 ]]e′′′ = True. Then there are three sets of elements N ′ , N ′′ ,
N ′′′ , where N ′ contains elements that validate T1 in e′ , N ′′ contains elements
that validate T2 in e′′ , and N ′′′ contains elements that validate T1 ⊙ T2 in e′′′ .
We have N ′ ∩ N ′′′ = ∅ and N ′′ ∩ N ′′′ = ∅, whereas N ′ ∩ N ′′ need not be
empty. Each element d ∈
/ {ex1 , . . . , exn } validates in e either 1) empEx∅ (F, x), if
d∈
/ N ′ ∪N ′′ ∪N ′′′ , or 2) T1 , if d ∈ N ′ \ N ′′ , or 3) T2 , if d ∈ N ′′ \ N ′ , or 4) T1 ⊙ T2 ,
if d ∈ (N ′ ∩ N ′′ ) ∪ N ′′′ . We construct environments e1 ,e2 ,e3 by assigning B1 and
relations from T1 to elements in N ′ \ N ′′ to e1 , assigning B2 and elements in
N ′ \ N ′′ to e2 , and splitting relations on elements in (N ′ ∩ N ′′ ) ∪ N ′′′ into those
for T1 , which we assign to e1 , and those for T2 , which we assign to e2 . We then
have [[LT1 M∗1 ]]e1 = True and [[LT2 M∗2 ]]e2 = True, so [[LT1 M∗1 ⊛LT2 M∗2 ]] = True.
Rules (5), (6): Directly from the definitions of empe and LF ′ M∗m it follows that
empe ⇒ LF ′ M∗m .
W
Lemma 17. ( R(C1 ,C2 ,C3 ) C3 ) ⇒ (C1 ⊛ C2 ) is a valid formula for every pair of
counting star formulas C1 and C2 .
W
Proof. Let [[ R(C1 ,C2 ,C3 ) C3 ]]e hold for some L-environment e. Then [[C3 ]]e =
C

True for some C3 such that S1 [[C1 ]] ⊛ S2 [[C2 ]] =⇒ S1,2 [[C3 ]]. By Lemma 16,
S1,2 [[C3 ]] ⇒ S1 [[C1 ]] ⊛ S2 [[C2 ]] is valid. By Lemma 13 and [[C3 ]]e = True, we have
[[S1,2 [[C3 ]]]]e1,2 = True. Therefore, [[S1 [[C1 ]] ⊛ S2 [[C2 ]]]]e1,2 = True. This means
that there are e1 and e2 such that split e1,2 [e1 , e2 ], [[S1 [[C1 ]]]]e1 = True, and
[[S2 [[C2 ]]]]e2 = True. From Lemma 13 we have [[C1 ]]e1 = True, and [[C2 ]]e2 = True.
From split e1,2 [e1 , e2 ] it follows that split e [e1 , e2 ], so [[C1 ⊛ C2 ]]e = True.
W
Lemma 18. C1 ⊛ C2 ⇒ R(C1 ,C2 ,C3 ) C3 is a valid formula for every pair of
counting star formulas C1 and C2 .
Proof. Let [[C1 ⊛ C2 ]]e = True for some L-environment e. Then there are e1 and
e2 such that split e [e1 , e2 ], [[C1 ]]e1 = True and [[C2 ]]e2 = True. By Lemma 13,
S1 [[C1 ]]e11 = True and S2 [[C2 ]]e22 = True. We construct S1,2 [[C3 ]] such that
C

S1 [[C1 ]] ⊛ S2 [[C2 ]] =⇒ S1,2 [[C3 ]] and [[C3 ]]e = True, as follows.
Let K1 be the GCCAT part of C1 and let K2 be the GCCAT part of C2 . Let
DX = D\{e x1, . . . , e xn }. For each d ∈ DX , let T1d be the type extension induced
by d in e1 , that is, let T1d ∈ exts(K1 , x) be the formula such that [[T1d ]]e11 [x 7→ d] =
True. Similarly, let T2d ∈ exts(K2 , x) be the formula such that [[T2d ]]e22 [x 7→ d] =
True. Because split e [e1 , e2 ], the operation T1 ⊙T2 is defined and [[T1 ⊙T2 ]]e1,2 [x 7→
d] = True. Because S1 [[C1 ]]e11 = True, with each d we can associate an occurrence
µ1 (d) in S1 [[C1 ]] of a formula Fµ1 (d) where Fµ1 (d) is of the form LT1d M1 or of the
form LT1d M∗1 , and an environment e1,µ1 (d) such that split e11 [e1,0 , (e1,µ1 (d) )µ(d) ],
such that K[[K1 ]]e1,0 = True, and such that for every d, [[Fµ1 (d) ]]e1,µ1 (d) = True.
28

Analogously, for each d we can associate an occurrence µ2 (d) in S2 [[C2 ]] of a
formula Fµ2 (d) of the form LT2d M2 or of the form LT2d M∗2 , and an environment
e2,µ2 (d) such that split e22 [e2,0 , (e2,µ2 (d) )µ2 (d) ], such that K[[K2 ]]e2,0 = True, and
such that for every d, [[Fµ2 (d) ]]e2,µ2 (d) = True.
We compute C3 by first combining K[[K1 ]] and K[[K2 ]] into K[[K1 ⊕ K2 ]].
From split e [e1 , e2 ] we conclude that the operation F1 ⊕ F2 is well-defined and
1,2
1,2
that [[K[[F1 ⊕ F2 ]]]]e1,2
0 = True where e0 is given by split e0 [e1,0 , e2,0 ].
We next apply rules (1)–(4) in Figure 7, as follows:
1. apply rule (1) once to each pair of occurrences µ1 (d) and µ2 (d) if they are
of the form LT1d M1 and LT2d M2 , respectively; let µ(d) be the occurrence of the
resulting formula Fµ(d) ≡ LT1d ⊙ T2d M1,2 ;
2. apply rule (2) once to each pair of occurrences µ1 (d) and µ2 (d) if µ1 (d) is an
occurrence of the form LT1d M1 and µ2 (d) is an occurrence of the form LT2d M∗2 ;
let µ(d) be the occurrence of the formula Fµ(d) ≡ LT1d ⊙ T2d M1,2 obtained as
one of the results;
3. apply rule (3) once to each pair of occurrences µ1 (d) and µ2 (d) if µ1 (d) is an
occurrence of the form LT1d M∗1 and µ2 (d) is an occurrence of the form LT2d M2 ;
let µ(d) be the occurrence of the formula Fµ(d) ≡ LT1d ⊙ T2d M1,2 obtained as
one of the results;
4. apply rule (4) once for each pair of occurrences of formulas of the form LT1d M∗1
and LT2d M∗2 ; for each d such that µ1 (d) is an occurrence of LT1d M∗1 and µ2 (d) is
an occurrence of LT2d M∗2 , let µ(d) be the occurrence of the resulting formula
Fµ(d) ≡ LT1d ⊙ T2d M∗1,2 .
Note that no rule is applied twice to a distinct pair of occurrences of formulas.
This means that the number of applications of rules is uniformly bounded, despite the fact that there is no bound on the size of the model e. In particular,
there is no bound on the number of elements d covered by a single application
of rule (4). Each formula of the form LT M1 is Fµ1 (d) for some d and each formula
of the form LT M2 is Fµ2 (d) for some d, and all such formulas are consumed by
applications of rules (1)–(3), so the resulting formula has no subformulas of the
form LT M1 or LT M2 . After applying rules (1)–(4), apply rules (5) and (6) to all
applicable formulas. The resulting formula FR has no occurrences of LT M∗1 or
LT M∗2 either, it contains only occurrences of formulas of forms LT M1,2 and LT M∗1,2 .
1,2
For each of the finitely many occurrences µ(d) in FR we construct eµ(d)
,
splitting e1,2 into the environment e1,2
defined above, and the environments
0
e1,2
,
by
assigning
the
type
extension
of
d in e1,2 to e1,2
µ(d)
µ(d) . By construction,
1,2
1,2
split e1,2 [e1,2
= True, it suffices to show
0 , (eµ(d) )µ(d) ]. To show [[FR ]]e

[[Fc ]]e1,2
c = True

(5)

for every occurrence c = µ(d0 ). Fix an occurrence c, and let δ = {d | µ(d) = c}.
1,2
d
d
By definition of e1,2
c , the type extension induced by each d ∈ δ in ec is T1 ⊙ T2 ,
and the type extension of each d ∈ DX \ δ is an empty extension. Therefore,
[[LT1d ⊙ T2d M∗1,2 ]]e1,2
= True. If Fc ≡ LT1d ⊙ T2d M∗1,2 then the equation (5) already
c
29

holds. If Fc ≡ LT1d ⊙ T2d M1,2 , then Fc was generated by one of the rules (1)–(3),
which means that δ is a singleton set. Namely, if Fc was generated by rules (1) or
(2), then there is exactly one d such that µ1 (d) = c, namely d0 , and similarly if Fc
was generated by rule (3), then there is exactly one d such that µ2 (d) = c, again
d0 . In both cases, δ = {d0 }, so d0 is the unique d with type extension T1d ⊙ T2d ,
which means that [[LT1d ⊙ T2d M1,2 ]]e1,2
c = True and the equation (5) holds.
We finally apply idempotence to ensure that no LT M∗m occurs more than
once. The resulting formula FR′ is equivalent to FR , so [[FR′ ]]e1,2 = True, FR′
C

is of the form S1,2 [[C3 ]], and S1 [[C1 ]] ⊛ S2 [[C2 ]] =⇒ S1,2 [[C3 ]]. From S1,2 [[C3 ]] we
recover C3 using the inverse of the translation in Figure 6. By Lemma 13 we
have [[C3 ]]e = True, completing the proof.

30

