39
推薦論文● PPL 2019(特集●プログラミングおよびプログラミング言語)

Failure of Cut-Elimination in Cyclic Proofs of
Separation Logic
Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, andHiroshi Unno
This paper studies the role of the cut rule in cyclic proof systems for separation logic. A cyclic proof system is a sequent-calculus style proof system for proving properties involving inductively defined predicates.
Recently, there has been much interest in using cyclic proofs for proving properties described in separation
logic with inductively defined predicates. In particular, for program verification, several theorem provers
based on mechanical proof search procedures in cyclic proof systems for separation logic have been proposed.
This paper shows that the cut-elimination property fails in cyclic proof systems for separation logic in several settings. We present two systems, one for sequents with single-antecedent and single-conclusion, andanother for sequents with single-antecedent and multiple-conclusions. To show the cut-elimination failure,
we present concrete and reasonably simple counter-example sequents which the systems can prove with cuts
but not without cuts. This result suggests that the cut rule is important for a practical application of cyclic
proofs to separation logic, since a naı̈ve proof search procedure, which tries to find a cut-free proof, gives alimit to what one would be able to prove.

1 Introduction
Separation logic [15] is a popular program logic
for reasoning about programs that use pointer data
structures. In separation logic, reasoning about recursive data structures is made possible by augmenting the logic with inductively defined predicates. For example, a predicate which says thata pointer points to a list may be written as follows:
ls(x, y) := x 7→ y | x 7→ z ∗ ls(z, y).
Here, x 7→ y means that the memory cell at address
x contains the value y, and A ∗ B is a separating
conjunction which says that the memory is a unionof two memory regions hA and hB with disjoint domains such that hA satisfies A and hB satisfies B.
分離論理の循環証明系におけるカット除去不能性.
木村大輔, 東邦大学, Toho University.
中澤巧爾, 名古屋大学, Nagoya University.
寺内多智弘, 早稲田大学, Waseda University.
海野広志, 筑波大学, Tsukuba University.
コンピュータソフトウェア, Vol.37, No.1 (2020), pp.39–52.

[研究論文] 2019 年 6 月 14 日受付.

Therefore, ls(x, y) says that x points to a singlylinked list that ends in y. (We refer to Section 2 forthe formal definition for our fragment of separation
logic.)In the verification approach for heap-manipulating
programs based on Hoare-style logic, showing validity of entailments A |= B between formulas inseparation logic is necessary for the rule of consequence:{A1 }P {B1 }A2 |= A1 and B1 |= B2{A2 }P {B2 },where P is a program to be verified, and {A}P {B}is a Hoare-triple with a pre-condition A and a postcondition B. For this purpose, several proof systems that employ sequents of the form A ⊢ B
and automatic theorem provers based on proofsearch algorithms in that systems have been proposed [1][2][8]–[10][13][17][18].
In a sequent-calculus style proof system, it is customary to handle inductively defined predicates likels(x, y) by adding a set of rules that introduce them

コンピュータソフトウェア

40

to left and right sides of sequents. For ls(x, y), theright introduction rules are:A ⊢ x 7→ y
A ⊢ ls(x, y)

A ⊢ x 7→ z ∗ ls(z, y)A ⊢ ls(x, y),and the left introduction rule is:(ind case) A ∗ C[x, y] ⊢ B(Ind)A ∗ ls(x, y) ⊢ B,
where (base case) and (ind case) stand for A ∗ x 7→
y ⊢ C[x, y] and A ∗ x 7→ z ∗ C[z, y] ⊢ C[x, y] withfresh variable z, respectively. C[x, y] is a formulathat may have free variables x and y. The premise(base case) is the base case of the induction, that is,
it says that C holds in the base case. The premise(ind case) encodes the inductive case with the induction hypothesis C, that is, it roughly says that
if C holds for the smaller list from z to y then it
also holds for the larger list from x to y. The rule
is an obstacle to a mechanical proof search because
one needs to guess an appropriate C.
A cyclic proof system [5]–[7] oﬀers an alternative
approach to doing proofs about inductively definedpredicates in a sequent calculus. In this approach,the left introduction rule of an inductively definedpredicate is replaced by a rule that directly encodes
the inductive definition. For instance, the left introduction rule of ls(x, y) is given as(base case)A ∗ x 7→ y ⊢ B A ∗ x 7→ z ∗ ls(z, y) ⊢ B(UL)
A ∗ ls(x, y) ⊢ B.
A proof search in a cyclic proof system starts fromthe root goal sequent, mechanically building theproof tree upwards by applying an applicable ruleat each node. The search may stop by reaching a sequent (called a bud) that it has seen before (called acompanion), thereby forming a “cyclic” proof thathas an edge from a leaf bud node to an internal
companion node. To ensure correctness, a certain
condition, called global trace condition, is imposedon the cyclic structure (cf. Section 3 for details).
Importantly, in the absence of the cut rule, thepossible children of a node can be syntactically determined from the (finitely many) rules applicableat the node, which substantially expedites the mechanical proof search.†1 The property has been
†1 Technically, this is only true if structural rules
such as weakening, contraction, and substitution
are made implicit.

used to a great advantage by researchers of cyclic
proofs, and they have proposed automatic theorem
provers based on cyclic proofs [8][9]. Furthermore,
as we discuss below, some automatic inductionbased provers for separation logic [10][13][17][18] canalso be seen as cyclic proof systems with restricted
forms of cuts.
Meanwhile, cyclic proof systems are being intensively studied in the theoretical computer science community (for various logics, such as separation logic, first-order logic, and linear logic)[3]–[5][7]–[9][14][16]. The research has lead to some
remarkable results, such as showing that the cyclic
proof system (with cuts) is strictly more powerful than the standard inductive first-order logic sequent calculus (i.e., that with a rule analogous tothe (Ind) rule above) [3][7]. However, some fundamental proof-theoretic properties, such as cutelimination and completeness, still remain open.
As the main contribution of this paper, we showthat cut-elimination fails in cyclic proof systems
for separation logic. As remarked above, the result is not only of theoretical interest since thepresence of the cut rule substantially aﬀects a mechanical proof search process. We prove the result for two cyclic proof systems for separation
logic: CSL0 IDω which deduces sequents with single conclusions, and CSLM
0 IDω which deduces sequents with multiple conclusions. We show the cutelimination failure by presenting concrete counterexample sequents which the systems can prove withcuts but not without cuts. The counter-examples
are fairly simple formulas about singly-linked lists.
They contain three kinds of semantically equivalentpredicates ls(x, y), lsX(x, y) and sl(x, y) each describing a singly-linked list from x to y. The predicate ls(x, y) is the usual list definition shown above,
whereas lsX(x, y) defines a list to be either a listof an odd length or a list of an even length where
odd and even length lists are defined inductively
in a manner analogous to ls(x, y). The predicatesl(x, y) is a “backward” definition of a list whereby
a list is constructed by adding an element to thetail rather than to the head. We show that thesequent ls(x, y) ⊢ lsX(x, y) is a counter-example
to cut-elimination for CSL0 IDω, and the sequentls(x, y) ⊢ sl(x, y) is that for CSLM
0 IDω. Thus, apractical implication of our results is that (someform of) a cut rule is necessary for designing usefulVol. 37 No. 1 Feb. 2020
theorem provers based on cyclic proofs, at least for
separation logic.
The rest of the paper is organized as follows. We
discuss related work next. Section 2 introduces
SL0 , a simple fragment of separation logic used in
the rest of the paper. Section 3 presents CSL0 IDω
and shows our first main result which says that
cut-elimination fails for CSL0 IDω. CSL0 IDω isclosely related to the system proposed by Brotherston et al. [8], and the section also shows that
cut-elimination fails in their system as well. In
Section 3, we present CSLM
0 IDω, and show thatthe counter-example for CSL0 IDω (i.e. ls(x, y) ⊢lsX(x, y)) is cut-free provable in CSLM
0 IDω. Then,
we show that CSLM
0 IDω still fails to satisfy cutelimination by presenting the cut-free unprovability of the counter-example ls(x, y) ⊢ sl(x, y). Section 5 concludes the paper with a discussion on
future work.
Related Work: As remarked above, there has
been much work on meta-theoretic properties ofcyclic proof systems for various logics [3]–[5][7]–[9][11][12][14][16]. Among them, some papers discuss the cut-elimination property for cyclic proof
systems. The paper [12] considers a cyclic proof
system for µMALL (linear logic with least andgreatest fixed-point operators), and discusses nonpreservability of the cyclic structure by the ordinary cut-elimination procedure. It discusses the
behavior of cut-elimination procedure, but our paper considers admissibility of the cut rule. The paper [11] proposes a sequent-style system for Kleene
algebra, and shows the cut rule is not admissible inthe system.
In the context of (semi-)automated deduction,
several cyclic-proof-based theorem provers for separation logic have been proposed [8][10][13][17][18].
Some of them allow restricted forms of cut. For
instance, SLEEK [13] allows cuts, but only againstuser-provided lemmas. The theorem provers proposed in [10][17][18] synthesize induction hypotheses during the proof search by following a certain
set of rules. They can be seen as a kind of a cyclic
proof system in which the cuts are restricted to be
only against the synthesized induction hypotheses.
None of these papers investigate the eﬀect of having
or not having the cut rule nor clarify whether theirrestricted forms of cuts are enough or not enoughfor theorem proving purpose.

41

2 Simple separation logic SL0This section defines a simple fragment of separation logic (SL0 ), which has the minimum necessary connectives 7→ and ∗ to define our counterexamples.
2. 1 Syntax of SL0
We assume a finite set {P1 , . . . , PK } of inductive
predicates. Each inductive predicate P has its arity
ar(P ). Terms of SL0 (denoted by t, u, . . .) consist ofvariables (x, y, z · · · ) and nil. We sometimes write→→x∈−x if x appears in −x.
Formulas (denoted by A, B, C, . . .) of SL0 are defined as follows.
−→
A ::= t 7→ u | P ( t ) | A ∗ A,−→
where the length of t is ar(P ). We sometimes→
write A(−x ) to denote variables occurring in A explicitly. We implicitly suppose associativity andcommutativity of the separating conjunction ∗,that is, A ∗ B =B ∗ A and (A ∗ B) ∗ C =A ∗ (B ∗ C).
The set of free variables in A is written as FV(A).
The union of FV(A1 ), . . . , FV(An ) is written as
FV(A1 , . . . , An ).
A substitution (denoted by θ) has the form x1 :=t1 , . . . , xk := tk , where xi and xj are diﬀerent variables if i ̸= j. The formula obtained by replacing each xi by ti (i = 1, . . . , k) in A is written by
A[x1 := t1 , . . . , xk := tk ].
Each inductive predicate P has its own definition,
which is given as follows:→P (−x ) := A1 | . . . | As
Each Ai is called a definition clause of P . Intu→
itively, this means that P (−x ) is defined by the
disjunction of A1 , . . . , As . We note that variables→of Aj not appearing in −x are implicitly existen→tially quantified. Namely, P (−x ) is defined by
−
→
−
→
−
→
−
→
−
→
−
→
∃ y1 A1 ( x , y1 ) ∨ . . . ∨ ∃ ys As ( x , ys ).
In this paper we will consider several kinds of list
predicates ls, sl, lsO, lsE and lsX given below.
Definition 1. The definitions of ls, sl, lsO, lsE,
and lsX are given as follows.
ls(x, y) := x 7→ y | x 7→ z ∗ ls(z, y)sl(x, y) := x 7→ y | sl(x, z) ∗ z 7→ y
lsO(x, y) := x 7→ y | x 7→ z ∗ lsE(z, y)lsE(x, y) := x 7→ z ∗ lsO(z, y)lsX(x, y) := lsO(x, y) | lsE(x, y)Both ls(x, y) and sl(x, y) mean singly-linked list

42

コンピュータソフトウェア

segments of positive lengths from x to y. The former and the latter predicates represent list segments constructed by adding cells repeatedly to thehead position and the tail position, respectively.
lsO(x, y) and lsE(x, y) mean list segments with
odd and positive even lengths, respectively. They
are defined by a mutual induction. lsX(x, y) means
list segments with odd or positive even length, thatis, list segments of positive length. The formulas ls(x, y), sl(x, y), and lsX(x, y) are semanticallyequivalent (see Lemma 2).
2. 2 Semantics of SL0
Let N be the set of natural numbers. A store(denoted by s) is a function from variables to N .
It is extended to a function on terms by s(nil) = 0.
We define update s[x1 := a1 , . . . , xn := an ] of s by
the store s′ such that s′ (xi ) = ai and s′ (y) = s(y)if y ̸∈ {x1 , . . . , xn }. It is sometimes abbreviated→→by s[−
x := −a ]. A heap (denoted by h) is a finite partial function from N \ {0} to N . The domain of h is written by dom(h). We write h1 + h2
for disjoint union of h1 and h2 , namely, it is defined when dom(h1 ) and dom(h1 ) are disjoint, and(h1 + h2 )(a) = hi (a) if a ∈ dom(hi ) for i = 1, 2.
We sometimes write [a1 7→ b1 , . . . , am 7→ bm ] forthe heap h defined by dom(h) = {a1 , . . . , am } andh(aj ) = bj (1 ≤ j ≤ m).
A pair (s, h) is called a heap model.
Definition 2 (Interpretation of formulas). The interpretation of a formula A in (s, h) (denoted bys, h |= A) is inductively defined as follows.
• s, h |= t 7→ u
def⇐⇒ h = [s(t) 7→ s(u)],−→• s, h |= P (0) ( t )def⇐⇒ never,−→• s, h |= P (m+1) ( t )−−−→ −
−
→
→ −
→ →
def
→
⇐⇒ s[−
y := b ], h |= A[P (m) / P ]( t , −y)−→for some b and definition clause A of P ,−→• s, h |= P ( t )−→def⇐⇒ s, h |= P (m) ( t ) for some m,• s, h |= A1 ∗ A2
def⇐⇒ s, h1 |= A1 and s, h2 |= A2
for some h1 and h2 such that h = h1 + h2 ,where P (m) is an auxiliary notation for defining−−−→ −→−→s, h |= P ( t ) and A[P (m) / P ] is the formula ob(m)tained by replacing each Pi by Pi .
(m)
Intuitively P
corresponds the m-time un-→folding of P , that is, P (0) (−x ) means ⊥ and−−−→ −
∨s
→ → −
→
−
→
(m+1) −P( x ) means∃ y A [P (m) / P ](−
x,→
y ),
i=1

i

i

j

where A1 , . . . , As are the definition clauses of P .
The following lemma explains how the above definition for inductive predicates works. This result will be used in the proof of Theorem 2 andLemma 5.
Lemma 1. Let hn be [a0 7→ a1 , a1 7→
a2 , . . . , an−1 7→ an ] for n ≥ 1. That is, hn forms
a singly-linked list of length n. Take a store sthat satisfies s(x) = a0 and s(y) = an . Then we
have s, hn |= ls(n) (x, y) by induction on n. Hences, hn |= ls(x, y) holds for any n ≥ 1. We can also
show s, hn |= sl(x, y) and s, hn |= lsX(x, y).
We say A and B are logically equivalent if forany heap model (s, h), s, h |= A and s, h |= B are
equivalent. Then we have the following claim.
Lemma 2. ls(x, y), sl(x, y), and lsX(x, y) are logically equivalent.

3 Cyclic proof system CSL0 IDω
This subsection defines a cyclic proof system
CSL0 IDω for SL0 , which handles single-conclusion
sequents defined as follows.
Definition 3 (Single-conclusion sequents of SL0 ).
A sequent of SL0 has the form A ⊢ B. The formulaon the left-hand side and the right-hand side of asequent are called its antecedent and succedent (orconclusion), respectively. A sequent A ⊢ B is calledvalid if, for any heap model (s, h), s, h |= A impliess, h |= B.
The following subsections give several inferS1 · · · Snence rules of the form
with sequentsS
S, S1 , . . . , Sn . For each inference rule, sequents
above the horizontal line are called its premises,
and a sequent below the line is called its conclusion.
In order to avoid confusion, we will use
the word “conclusion” only for inference rules,
and the words “single-conclusion” and “multipleconclusion” (they are used for sequents) are nevershortened into the word “conclusion”.
3. 1 The proof system CSL0 IDω
The derivation rules of CSL0 IDω consist of thebasic rules and the unfolding rules. The basic rules
are the following three rules:

Vol. 37 No. 1 Feb. 2020A⊢A
A⊢C C⊢B
(Cut)
A⊢B

(Id)
A1 ⊢ B1 A2 ⊢ B2(∗)
A1 ∗ A2 ⊢ B1 ∗ B2

The rule (Id) is the identity rule, the rule (Cut) isthe cut-rule in the sequent calculus. The rule (∗)
combines two premises into one with the separating conjunction ∗, that is, it says if A1 implies B1
and A2 implies B2 , then B1 ∗ B2 is obtained fromA1 ∗ A2 , since A1 and A2 independently implies B1
and B2 , respectively.
The unfolding rules consist of (UL) and (UR). In→
the following, we assume P (−x ) := A1 | . . . | As isthe definition of P .
−→ →B ⊢ Aj ( t , −
u)
(UR)
−
→
B ⊢ P( t )−→ →B ∗ A1 ( t , −z1 ) ⊢ C−→ →· · · B ∗ As ( t , −zs ) ⊢ C(UL)−→
B ∗ P( t ) ⊢ C→→
where −
z1 , . . . , −zs are fresh.
Example 1. The unfolding rules for ls, sl, lsO,
lsE and lsX are as follows.
(1) Rules for ls:
B ⊢ t 7→ u(UR)B ⊢ ls(t, u)

B ⊢ t 7→ t1 ∗ ls(t1 , u)(UR)
B ⊢ ls(t, u)

B ∗ t 7→ u ⊢ C B ∗ t 7→ z ∗ ls(z, u) ⊢ C(UL)
B ∗ ls(t, u) ⊢ C(2) Rules for sl:
B ⊢ t 7→ u(UR)B ⊢ sl(t, u)

B ⊢ sl(t, u1 ) ∗ u1 7→ u(UR)B ⊢ sl(t, u)

B ∗ t 7→ u ⊢ C B ∗ sl(t, z) ∗ z 7→ u ⊢ C(UL)B ∗ sl(t, u) ⊢ C(3) Rules for lsO:
B ⊢ t 7→ t1 ∗ lsE(t1 , u)
B ⊢ t 7→ u
(UR)
(UR)
B ⊢ lsO(t, u)
B ⊢ lsO(t, u)
B ∗ t 7→ u ⊢ C B ∗ t 7→ z ∗ lsE(z, u) ⊢ C(UL)
B ∗ lsO(t, u) ⊢ C(4) Rules for lsE:
B ⊢ t 7→ t1 ∗ lsO(t1 , u)(UR)
B ⊢ lsE(t, u)

43

B ∗ t 7→ z ∗ lsO(z, u) ⊢ C(UL)
B ∗ lsE(t, u) ⊢ C(5) Rules for lsX:
B ⊢ lsO(t, u)(UR)
B ⊢ lsX(t, u)

B ⊢ lsE(t, u)(UR)
B ⊢ lsX(t, u)

B ∗ lsO(t, u) ⊢ C B ∗ lsE(t, u) ⊢ C(UL)
B ∗ lsX(t, u) ⊢ C
We define a cyclic proof of CSL0 IDω in a similar
way to [6][7].
Definition 4 (Derivation tree). A derivation tree
(denoted by D) of a sequent e is a finite tree structure whose nodes are labeled by sequents of SL0 ,the label of the root node is e, and a node labeledwith e′ has children labeled with e′1 , . . . , e′k when′′
there is an instance e1 . . . ek of an inference rulee′of CSL0 IDω. A leaf node which is the conclusion of
the rule (Id) is called closed. An open (not closed)
leaf is called a bud. A companion for a bud eb is an
occurrence of a sequent ec in D of which eb is an
substitution instance, namely, eb = ec [θ] for someθ.
In a derivation tree, if e appears as a conclusionof a rule instance and e′ is a premise of the rule,e′ is called a premise of e. In this case, e is calleda parent of e′ . Similarly we also use the usual terminology of the tree structure such as child anddescendant.
Definition 5 (Pre-proof). A pre-proof of e is givenby (D, R), where D is a derivation tree of e and R
is a function assigning a companion to every bud of
D. A proof-graph G(P) of a pre-proof P = (D, R)
is a graph structure D with additional edges frombuds to their companions assigned by R. A path in
P is a path in G(P).
Definition 6 (Trace). Let (ei )i∈ω be an infinite
path in P. A trace following (ei )i∈ω is a sequenceof (Ci )i∈ω such that each Ci is a subformula occur−→
rence of the form P ( t ) in the antecedent of ei , andsatisfies the following conditions:(a) if ei is the conclusion of (UL) in D, then either
Ci = Ci+1 or Ci is unfolded in the rule instanceand Ci+1 appears as a subformula of the unfolding
result. In the latter case, i is called a progressing
point of the trace;(b) if ei is the conclusion of a rule other than (UL),コンピュータソフトウェア

44

x 7→ z ∗ lsO(z, y) ⊢ x 7→ z ∗ lsO(z, y)
x 7→ z ∗ lsO(z, y) ⊢ lsE(x, y)
x 7→ z ∗ lsO(z, y) ⊢ lsX(x, y)
x 7→ y ⊢ x 7→ y(UR)x 7→ y ⊢ lsO(x, y)(UR)
x 7→ y ⊢ lsX(x, y)

(UR)

(UR)

x 7→ z ∗ lsE(z, y) ⊢ lsO(x, y)
x 7→ z ∗ lsE(z, y) ⊢ lsX(x, y)

x 7→ z ∗ lsX(z, y) ⊢ lsX(x, y)
x 7→ z ⊢ x 7→ z (†) ls(z, y) ⊢ lsX(z, y)
x 7→ z ∗ ls(z, y) ⊢ x 7→ z ∗ lsX(z, y)

(∗)

(UR)

(UR)
(UL)

(1)
x 7→ z ∗ lsX(z, y) ⊢ lsX(x, y)

x 7→ z ∗ ls(z, y) ⊢ lsX(x, y)(†) ls(x, y) ⊢ lsX(x, y)

Fig. 1x 7→ z ∗ lsE(z, y) ⊢ x 7→ z ∗ lsE(z, y)

(Cut)

(UL)

Cyclic proof of ls(x, y) ⊢ lsX(x, y) (for Proposition 1)

then Ci+1 is the corresponding subformula occurrence in ei+1 , which satisfies Ci+1 =Ci ;(c) if ei is a bud and ei+1 [θ] = ei for some substitution θ, then Ci+1 is the corresponding subformulaoccurrence in ei+1 , which satisfies Ci+1 [θ]=Ci .
Definition 7 (Cyclic proof). Let P be a pre-proofof e. P is called a cyclic proof of e if it satisfies theglobal trace condition: for any infinite path (ei )i∈ω
in P, there exists a trace (Ci )i∈ω following the paththat has infinitely many progressing points.
The global trace condition is a suﬃcient condition for soundness, that is, we have the following
theorem. This theorem is shown by the similar way
to [6]–[8].
Theorem 1 (Soundness of CSL0 IDω). If A ⊢ B
has a cyclic proof P of CSL0 IDω, then all sequentsin P are valid. In particular, A ⊢ B is valid.
In the following subsection we will prove thatls(x, y) ⊢ lsX(x, y) is a counter-example for the
cut-elimination property of CSL0 IDω. We firstshow that this example has a cyclic proof with(Cut).
Proposition 1. (1) x 7→ z ∗ lsX(z, y) ⊢ lsX(x, y)
is cut-free provable in CSL0 IDω.
(2) ls(x, y) ⊢ lsX(x, y) is provable in CSL0 IDω
with (Cut).
Proof. (1) is shown by the upper proof of Fig 1.
The lower one is a pre-proof by putting the upperproof at the node labeled by (1) and by connecting
the bud ls(z, y) ⊢ lsX(z, y) marked by (†) to theentailment with the same mark at the root position.
The pre-proof is a cyclic proof that shows (2), since
the only infinite path which is created from the budcompanion has an infinitely progressing trace (thesequence of the underlined predicates).

3. 2 Counter-example for cut-eliminationof CSL0 IDω
We define ♯7→ A by the number of 7→ in A. We
also define ♯7→ (A ⊢ B) by ♯7→ A.
Next theorem is our first main result, namely, thecut-elimination property fails in CSL0 IDω.
Theorem 2. The sequent ls(x, y) ⊢ lsX(x, y) is
not cut-free provable in CSL0 IDω.
Proof. Suppose that ls(x, y) ⊢ lsX(x, y) has a cutfree cyclic proof (D, R). We will show contradiction.
We construct a finite path e = (e0 , e1 , . . . , em ) ofD such that each ej has the form (up to permutation of ∗)z0 7→ z1 ∗ . . . ∗ zkj −1 7→ zkj ∗ ls(zkj , w) ⊢ lsX(z0 , w)
for some kj and pairwise distinct variables
z0 , . . . , zkj , w. Let e0 be ls(x, y) ⊢ lsX(x, y) at
the root position. Assume that e0 , . . . , ej are already defined. If ej is the conclusion of a (UL),
then define ej+1 by the unique premise of the ruleinstance that contains the ls-predicate in the antecedent. We note that ej+1 has the required formand ♯7→ ej < ♯7→ ej+1 . Otherwise finish constructing
the path e.
Claim 1. For any sequent e in D, if the antecedent of e contains the ls-predicate, then e ∈ e
or e is a descendant of em .
This claim is shown by induction on the heightht(e), namely the length of the path from the root
node to e, of e in D. If ht(e) = 0, then e = e0 ∈ e.
We show the case ht(e) > 0. Assume e ̸∈ e. We
show that e is a descendant of em . In this case, e isa premise of an instance of a rule (r), which is not(Cut). Let e′ be the parent of e, that is the conclusion of the rule instance. Then the antecedent ofe′ contains the ls-predicate. Hence e′ ∈ e or e′ isa descendant of em by the induction hypothesis. If

Vol. 37 No. 1 Feb. 2020the latter case holds, we have the expected result.
Otherwise, e′ must be em since e contains ls, e′ ∈ e
and e ̸∈ e. Thus e is a descendant of em . Hence wehave Claim 1.
Claim 2. em is not a bud.
We show this claim. Assume that em is a bud.
Then the antecedent of the companion e contains
the ls-predicate. By Claim 1, we have e ∈ esince em is a bud. Hence there is an infinite pathe, . . . , em , e, . . . of the cyclic proof (D, R). By the
global trace condition, there is a trace following thepath with infinitely many progressing points. Thismeans ♯7→ e < ♯7→ em ≤ ♯7→ e. Hence we have contradiction. Thus we obtain Claim 2.
By Claim 2, em is a conclusion of an instance ofa rule (r). Then (r) must be (UR) by case analysisof the inference rules. Let ẽ be the unique child of
em in D. The form of ẽ is either(a) z0 7→ z1 ∗ . . . ∗ zkm −1 7→ zkm ∗ ls(zkm , w) ⊢lsO(z0 , w), or(b) z0 7→ z1 ∗ . . . ∗ zkm −1 7→ zkm ∗ ls(zkm , w) ⊢lsE(z0 , w).
Consider the case (a). Take a store s1 such thats1 (zi ) = i + 1 and s1 (w) = 2 ∗ km + 1. Define h1 bydom(h1 ) = {1, 2, . . . , 2∗km } and h1 (i) = i+1. Thens1 , h1 |= z0 7→ z1 ∗ . . . ∗ zkm −1 7→ zkm ∗ ls(zkm , w)
and s1 , h1 ̸|= lsO(z0 , w). Hence (a) is invalid. We
can also show that (b) is invalid by taking s2 suchthat s2 (zi ) = i + 1 and s2 (w) = 2 ∗ km + 2, anddefining h2 by dom(h2 ) = {1, 2, . . . , 2 ∗ km + 1}
and h2 (i) = i + 1. Therefore ẽ is invalid. This
contradicts the soundness theorem. Hence we conclude that ls(x, y) ⊢ lsX(x, y) is not cut-free provable.
By combining proposition 1 and theorem 2, we
can obtain our first main result.
Corollary 1. The cyclic proof system CSL0 IDω
does not enjoy the cut-elimination property.
We note that our CSL0 IDω is designed as simple as possible in order to clarify the essence of our
discussion. The above corollary can be extended
easily to cyclic proof systems (of single-conclusion
sequents) that are extensions of CSL0 IDω withother connectives whose inference rules guarantee
the subformula property.

45

3. 3 Failure of Cut-elimination in Brotherston’s CADE2011-system
In this subsection we aim to demonstrate thatour proof technique in the previous subsection also
works for Brotherston’s CADE2011 paper [8]. The
readers may hope to extend our result in the previous subsection to Brotherston’s system as mentioned after Corollary 1. However we cannot doit, since Brotherston’s system contains the empty
predicate emp, which is the unit of ∗. It requires
the inference rules that do not guarantee the subformula property (see the rules (EmpL’) and (EmpR’)below). While the essence of the proof technique remains the same, a small modification is necessary
to handle these inference rules.
We first extend SL0 by adding emp, that is, theformulas of the extended system SL’0 are given as
follows:−→
A ::= t 7→ t | A ∗ A | P ( t ) | emp
The interpretation of the empty predicate is given
as follows:defs, h |= emp ⇐⇒ dom(h) = ∅Then we extend CSL0 IDω by adding the following derivation rules:
A⊢B(EmpR)A ⊢ B ∗ emp

A⊢B(EmpL)
emp ∗ A ⊢ B

A ⊢ B ∗ emp(EmpR’)
A⊢B

emp ∗ A ⊢ B(EmpL’)
A⊢B

x 7→ u ∗ x 7→ u′ ∗ A ⊢ B(Unsat7→)

We call this extended system CSL’0 IDω.
The definitions of pre-proofs, traces, and cyclic
proofs of CSL’0 IDω are given in the similar way tothose of CSL0 IDω. The soundness theorem for thisextended system also holds.
Then we can show the similar claim to Theorem 2.
Proposition 2. The sequent ls(x, y) ⊢ lsX(x, y)
is not cut-free provable in CSL’0 IDω.
Proof (sketch). Suppose that ls(x, y) ⊢ lsX(x, y)
has a cut-free cyclic proof (D, R). We construct afinite path e = (e0 , e1 , . . . , em ) of D such that eachej has the form
kj −1
−
−−
→
−
−−
→
i=0 zi 7→ zi+1 ∗ls(zkj , w)∗emp ⊢ lsX(z0 , w)∗emp
for some kj and pairwise distinct variables
z0 , . . . , zkj , w, and e0 is ls(x, y) ⊢ lsX(x, y) at theroot position. If ej is the conclusion of a (UL), de-∗コンピュータソフトウェア

46fine ej+1 by the unique premise of ej which contains
ls. If ej is the conclusion of EmpL, EmpR, EmpL’,
or EmpR’, define ej+1 by the unique premise. We
claim that ♯7→ ej ≤ ♯7→ ej+1 for any j < m, and, inparticular, ♯7→ ej < ♯7→ ej+1 if ej is the conclusionof a rule instance of (UL). Then we have the same
claims as Claim 1 and Claim 2 of Theorem 2. We
also have the following claim:
Claim 3 em is not the conclusion of a rule instance of (Unsat7→).
This claim is obtained by investigating that the antecedents of e are satisfiable. Hence em cannot be
the conclusion of (Unsat7→).
By using Claim 1, Claim 2, and Claim 3, we canshow the expected result in a similar way to theproof of Theorem 2.
We introduce an extended system CSLB IDω,which is a variant of Brotherston’s system [8]. The
diﬀerence between these two systems is not essential: terms of the system in [8] are only variables.
The formulas of CSLB IDω are given as follows:−→
A ::= t 7→ t | A ∗ A | P ( t ) | emp
2| t = t | t ̸= t | t 7→ (t, t) | ⊤ | ⊥ | A ∨ A
The derivation rules of CSLB IDω are those of
CSL’0 IDω with the following rules:
(⊤)

A⊢t=t

t = u ∗ t ̸= u ∗ A ⊢ B(Unsat=)

⊥∗A⊢B

(⊥)

A⊢⊤

(=R)

2

t 7→ (u1 , u2 ) ∗ t 7→ (u′1 , u′2 ) ∗ A ⊢ B
2

2(Unsat7→)

A1 ∗ B ⊢ C A2 ∗ B ⊢ C(∨L)(A1 ∨ A2 ) ∗ B ⊢ C
A ⊢ Bi ∗ C(∨R)
A ⊢ (B1 ∨ B2 ) ∗ C(i = 1, 2)
The following lemma shows that the above additional inference rules cannot be applied in proofsearch procedures of ls(x, y) ⊢ lsX(x, y).
Lemma 3. Let A and B be formulas of CSLB IDω
whose connectives and predicates are emp, ∗, 7→,ls, lsX, lsE, and lsO. Assume A ⊢ B has a cutfree derivation tree of CSLB IDω. Then all inference rules used in the derivation tree are those of
CSL’0 IDω.

This lemma can be shown by induction on thederivation tree.
As the result of this subsection, we can show the
failure of cut-elimination in CSLB IDω.
Theorem 3 (Failure of cut-elimination in
CSLB IDω). CSLB IDω does not enjoy the cutelimination property.
Proof. Note that ls(x, y) ⊢ lsX(x, y) can be shownin CSLB IDω with (Cut), since CSLB IDω is an extension of CSL0 IDω. Then we show ls(x, y) ⊢lsX(x, y) is not cut-free provable in CSLB IDω.
Assume that it has a cut-free cyclic proof of
CSLB IDω. Then the cyclic proof is also a proof
of CSL’0 IDω since all inference rules are those of
CSL’0 IDω by the previous lemma. Hence we havecontradiction by proposition 2.
Remark 1. In [8], an automated prover for sequents (that do not contain nil) in CSLB IDω,which is based on a proof-search procedure in
CSLB IDω, is proposed. Although the system contains (Cut), the tool uses the rule for managing
basic properties about ∗, such as associativity, commutativity, and unit of ∗. Hence the prover cannot
find non-trivial cut-formulas (e.g. the cut-formulax 7→ z ∗lsX(z, y) used in the proof of Proposition 1)
during its proof-search procedure.
Recall that each sequent considered in this section has a single-conclusion. It is the reason whyls(x, y) ⊢ lsX(x, y) works as a counter-example forthe cut-elimination, that is, we are forced to choose
either lsO(x, y) or lsE(x, y) in unfolding lsX(x, y)on the right-hand side of a sequent. This situation can be avoided if we consider sequents withmultiple-conclusions.

4 Cyclic proof system CSLM
0 IDω formultiple-conclusion SL0This section presents the second cyclic proof
system CSLM
0 IDω for sequents with multipleconclusions defined below.
Let ∆ be a multiset of formulas. We sometimes
write B1 , B2 , . . . , Bn instead of {B1 , B2 , . . . , Bn }.
We also write ∆, B for ∆ ∪ {B}. We define ∆ ∗ ∆′by {B ∗ B ′ | B ∈ ∆ and B ′ ∈ ∆′ }. We also define∨s, h |= ∆ by ∃B ∈ ∆(s, h |= B).
Definition 8 (Multiple-conclusion sequents of

Vol. 37 No. 1 Feb. 2020
SL0 ). The multiple-conclusion sequents of SL0 havethe form A ⊢ ∆. A sequent A ⊢ ∆ is valid if, for∨any (s, h), s, h |= A implies s, h |= ∆.
4. 1 Cyclic proof system CSLM
0 IDω formultiple-conclusion sequentsThe derivation rules of CSLM
0 IDω consists of thebasic rules and the unfolding rules. The basic rulesof CSLM
0 IDω are given as follows.
A⊢A

(Id)

A ⊢ ∆1 , C C ⊢ ∆2
(Cut)
A ⊢ ∆1 , ∆2

A1 ⊢ ∆1 A2 ⊢ ∆2(∗)
A1 ∗ A2 ⊢ ∆1 ∗ ∆2A⊢∆(Wk)
A ⊢ ∆, BA ⊢ ∆, B, B
(Ctr)
A ⊢ ∆, B

The unfolding rules (UL) and (UR) of CSLM
0 IDωare straightforward extension of those of CSL0 IDω.
→We assume that P (−x ) := A1 | . . . | As is the definition of P .
−→ →B ⊢ ∆, C ∗ Aj ( t , −
u)
(UR)
−
→
B ⊢ ∆, C ∗ P ( t )−→ →B ∗ A1 ( t , −z1 ) ⊢ ∆−→ →. . . B ∗ As ( t , −zs ) ⊢ ∆(UL)−→
B ∗ P( t ) ⊢ ∆→where −
z1 , . . . , −z→n are fresh.
The pre-proofs, traces, and cyclic proofs of
CSLM
0 IDω are defined similarly to those of
CSL0 IDω.
Remark 2. The main diﬀerence between CSL0 IDω
and CSLM
0 IDω is the structural rules, namely
the contraction rule (Ctr) and the weakening rule
(Wk). These rules allow to change whole proof
structure and strengthen the provability of theproof system. As we will see in the next proposition, the previous counter-example does not work in
the current system. Hence we need a new counterexample and a new proof technique that can capture the changed proof structure.
The soundness theorem of CSLM
0 IDω is also
shown in a similar way to that of CSL0 IDω:
Theorem 4 (Soundness of CSLM
0 IDω). If A ⊢ ∆M
has a cyclic proof P of CSL0 IDω, then all sequentsin P are valid. In particular, A ⊢ ∆ is valid.
The previous example ls(x, y) ⊢ lsX(x, y) is cutfree provable in the current system.
Proposition 3. ls(x, y) ⊢ lsX(x, y) is cut-free
provable in CSLM
0 IDω.

47

Proof. The proof figure given in Fig 2 is a cutfree pre-proof of ls(x, y) ⊢ lsX(x, y) in CSLM
0 IDω.
Note that the two entailments marked by (†) are ina bud-companion relation. The only infinite pathin this pre-proof contains an infinitely progressing
trace (the sequence of the underlined predicates).
Hence this pre-proof is a cyclic proof, since it satisfies the global trace condition.
This proposition shows that ls(x, y) ⊢ lsX(x, y)does not work as a counter-example for the cutelimination property of CSLM
However
0 IDω.
we still have another counter-example ls(x, y) ⊢sl(x, y). We first show that this sequent is provable in CSLM
0 IDω.
Proposition 4. (1) x 7→ z ∗ sl(z, y) ⊢ sl(x, y) is(cut-free) provable in CSLM
0 IDω.
(2) ls(x, y) ⊢ sl(x, y) is provable in CSLM
0 IDωwith (Cut).
Proof. The proof figures in Fig 3 show both (1) and(2). The first claim is obtained by the upper preproof, which is a cyclic proof since it satisfies theglobal trace condition. The lower figure becomes a
pre-proof by putting the upper one at the position
marked by (1). We can easily check the pre-proof
satisfies the global trace condition. Hence (2) isshown, since ls(x, y) ⊢ sl(x, y) has a cyclic proof
with (Cut).
4. 2 Counter-example for cut-eliminationof CSLM
0 IDω
This subsection shows that the cut-elimination
property fails in CSLM
0 IDω. The main result of
this section is the following theorem.
Theorem 5. The sequent ls(x, y) ⊢ sl(x, y) is not
cut-free provable in CSLM
0 IDω.
Remark 3. In the proof of Theorem 2, a contradiction appears at the point when (UR) is applied
to the unique succedent. In the current case, however, this idea does not work, since, at the pointthat (UR) is used, a formula before (UR) may remain in the succedent part because of contraction.
Our basic idea for proving Theorem 5 is as follows: focusing on the path of a cyclic proof that
contains both ls in the antecedent part and sl inthe succedent part; and analyzing the form of sequents on the path. To do this, we prepare somenotions and show their properties.
In the following we write n
i=0 Ai for A0 ∗· · ·∗An .

∗コンピュータソフトウェア

48
x 7→ y ⊢ x 7→ y(UR)x 7→ y ⊢ lsO(x, y)(Wk)
x 7→ y ⊢ lsO(x, y), lsE(x, y)(†)

x 7→ z ⊢ x 7→ z(†) ls(z, y) ⊢ lsE(z, y), lsO(z, y)

x 7→ z ∗ ls(z, y) ⊢ x 7→ z ∗ lsE(z, y), x 7→ z ∗ lsO(z, y)
x 7→ z ∗ ls(z, y) ⊢ lsO(x, y), lsE(x, y)ls(x, y) ⊢ lsO(x, y), lsE(x, y)(∗)(UR × 2)(UL)

(UR × 2)ls(x, y) ⊢ lsX(x, y), lsX(x, y)(Ctr)ls(x, y) ⊢ lsX(x, y)
Fig. 2Cut-free cyclic proof of ls(x, y) ⊢ lsX(x, y) (for Proposition 3)

x 7→ z ∗ z 7→ y ⊢ x 7→ z ∗ z 7→ y(UR)x 7→ z ∗ z 7→ y ⊢ sl(x, z) ∗ z 7→ y(UR)x 7→ z ∗ z 7→ y ⊢ sl(x, y)(†) x 7→ z ∗ sl(z, w) ⊢ sl(x, w)

w 7→ y ⊢ w 7→ y

x 7→ z ∗ sl(z, w) ∗ w 7→ y ⊢ sl(x, w) ∗ w 7→ y
x 7→ z ∗ sl(z, w) ∗ w 7→ y ⊢ sl(x, y)(†) x 7→ z ∗ sl(z, y) ⊢ sl(x, y)
x 7→ z ⊢ x 7→ z
x 7→ y ⊢ x 7→ y(UR)x 7→ y ⊢ sl(x, y)(‡) ls(z, y) ⊢ sl(z, y)

x 7→ z ∗ ls(z, y) ⊢ x 7→ z ∗ sl(z, y)

x 7→ z ∗ ls(z, y) ⊢ sl(x, y)

∗

(Cut)

(UL)

Cyclic proof of ls(x, y) ⊢ sl(x, y) (for Proposition 4)

Definition 9 (Ls-form). An SL0 formula is calleda connected Ls-form from x to y, if it has the form
n−1−→
i=0 zi 7→ zi+1 ∗ls(zn , y), z0 is x, and z , y are pairwise distinct variables. A formula is called an Lsform from x to y, if it is obtained by removing somepoints-to predicates from a connected Ls-form.
We sometimes omit “from x to y” if it is apparent
from the context.
Definition 10 (Sl-form). A formula is called aconnected Sl-form from x to y, if it has the form
sl(x, zn ) ∗ n−1
i=0 zi+1 7→ zi with z0 = y. A formulais called an Sl-form from x to y, if it is obtainedby removing some points-to predicates from a connected Sl-form. A formula is called a semi Sl-form,
if it is an Sl-form or contains only 7→.
A finite multiset ∆ of formulas is called a semi
Sl-form, if all elements of ∆ are semi Sl-form.
The following lemma is easily shown from thedefinition.
Lemma 4. If A is an Ls-form from x to y, thenA is satisfiable.
Lemma 5. Assume that A is an Ls-form from x
to y, ∆ is a semi Sl-form from x to y, and A ⊢ ∆is valid. Then we have the following claims.
(1) A is a connected Ls-form.

∗

(UR)

(UL)

(1)
x 7→ z ∗ sl(z, y) ⊢ sl(x, y)(∗)(‡) ls(x, y) ⊢ sl(x, y)
Fig. 3(∗)(2) sl(x, y) is in ∆.
Proof. Suppose the assumption. Since A is an Lsform from x to y, there is a connected Ls-formn−1−→
i=0 zi 7→ zi+1 ∗ ls(zn , y), where z0 = x and z , y
are pairwise distinct. Then A can be written asi∈I zi 7→ zi+1 ∗ ls(zn , y), where I ⊆ {0, . . . , n − 1}.
Let k = |FV(A, ∆)|. Define s and h by:s(zi ) = i + 1 for i ∈ {0, 1, . . . , n},s(y) = n + k + 2, and→s(w) = 0 if w ̸∈ −z , y.
dom(h) = {i + 1 | i ∈ I} ∪ {n + 1, . . . , n + k + 1},
and h(m) = m + 1 for m ∈ dom(h).
Then |dom(h)| = |I| + k + 1 and n + k + 2 ̸∈dom(h). We also have s, h |= A. Hence s, h |= B
for some B ∈ ∆ since A ⊢ ∆ is valid by the assumption.
We will now show that B is an Sl-form. Supposethat B is not an Sl-form. By the assumption, B
has the form j∈J xj 7→ x′j and s, h |= B. Then
we obtain contradiction, since |dom(h)| = |J| ≤|FV(∆)| ≤ k < |dom(h)|. Therefore B is an Slform.
(1) Suppose that A is not a connected Ls-form.
Then the set {0, 1, . . . , n − 1} \ I is not empty. Take
the smallest element i0 of this set. We will show

∗

∗

∗

Vol. 37 No. 1 Feb. 2020
contradiction by the case analysis of i0 .
We show the case i0 = 0. This case meansx = z0 ̸∈ FV(A) since A does not contain z0 7→ z1 .
Then 1 = s(z0 ) ̸∈ dom(h). Recall the above B.
It satisfies s, h |= B and contains sl(x, z ′ ) since B
is an Sl-form. Then we have 1 = s(x) ∈ dom(h).
Hence we have contradiction.
We show the case i0 > 0. This case we have
0 −1
zj 7→ zj+1 ∗ j∈I ′ zj 7→ zj+1 ∗ ls(zn , y),s, h |= ij=0′
where I = I \ {0, . . . , i0 − 1} and i0 ̸∈ I ′ . Hence
we have i0 + k + 1 ≤ |dom(h)|, since {1, . . . , i0 } ∪{n + 1, . . . , n + k + 1} ⊆ dom(h). Now the Sl-form′′
7→ zj′ . Thus
) ∗ j∈J zj+1
B has the form sl(x, zm
there exist h1 and h2 such that h = h1 +h2 , s, h1 |=′′7→ zj′ . By the defisl(x, zm) and s, h2 |= j∈J zj+1
nition of h and i0 , we have dom(h1 ) ⊆ {1, . . . , i0 }.
Hence we have |dom(h1 )| ≤ i0 . We also have|dom(h2 )| ≤ |FV(∆)| ≤ k. Therefore we obtaini0 + k + 1 ≤ |dom(h)| = |dom(h1 )| + |dom(h2 )| ≤i0 + k. Contradiction.
Finally we conclude that A is a connected Lsform. Hence (1) is shown.
(2) Since A is a connected Ls-form by (1), we
have I = {0, . . . , n − 1}. Hence we also havedom(h) = {1, . . . , n + k + 1}. Recall that s, h |= B
and B is an Sl-form. We show B is sl(x, y) by′contradiction. Then B has the form sl(x, zm
)∗
′
′
z
→
7
z
with
J
=
̸
∅.
Thus
there
exist
h1
j+1
j
j∈J
′
and h2 such that h = h1 + h2 , s, h1 |= sl(x, zm)′
7→ zj′ . Note that dom(h1 ) =and s, h2 |= j∈J zj+1′′
{1, . . . , s(zm) − 1} and dom(h2 ) = {s(zm), . . . , n +′k + 1}. Moreover s(zm ) < n + k + 2 = s(y) since J→′
is not empty. Hence zm∈−
z by the definition of s′′and zm ̸= y, We have |dom(h1 )| = s(zm)−1 ≤ nand |dom(h2 )| ≤ |FV(∆)| ≤ k. From this, we obtain n+k+1 = |dom(h)| = |dom(h1 )|+|dom(h2 )| ≤n + k. This is a contradiction. Therefore sl(x, y) =B ∈ ∆.

∗

∗

∗

∗

∗

∗

Definition 11 (L-form). A sequent A ⊢ ∆ is called
an L-form from x to y if A is an Ls-form from x toy and ∆ is a semi Sl-form from x to y.
We define ♯7→ (e) for a sequent e of CSLM
0 IDω inthe similar way to one of CSL0 IDω.
Lemma 6. Let P be a cut-free cyclic proof in
CSLM
0 IDω. Assume that an L-form e from x toy appears in P as the consequence of an inference rule (r). Then there is a unique premise e′of the rule such that e′ is an L-form. Moreover,49′♯7→ (e) < ♯7→ (e ) if (r) is (UL), and ♯7→ (e) = ♯7→ (e′ )otherwise.
Proof. This lemma is shown by case analysis of therule. Let A and ∆ be the antecedent and the succedent of e, respectively.
The rule (Id) is not the case since, by the definition of L-form, A contains the ls-predicate, and ∆does not contain the ls-predicate.
The rule (Cut) is not the case since P is cut-free.
The cases of (Wk) and (Ctr) are immediately
shown.
The case of (UR). By the premise e has the formA ⊢ ∆1 , B ∗ sl(x, z), and B ∗ sl(x, z) is an Sl-form.
The unique premise e′ of e is either A ⊢ ∆1 , B ∗x 7→w ∗ w 7→ z or A ⊢ ∆1 , B ∗ sl(x, w) ∗ w 7→ z. In eachcase, e′ is an L-form, since both B ∗ x 7→ w ∗ w 7→ z
and B ∗ sl(x, z) are semi Sl-forms. We also have♯7→ (e) = ♯7→ (e′ ).
The case of (UL). By the premise e has the form
A1 ∗ ls(z, y) ⊢ ∆, and A1 ∗ ls(z, y) is an Ls-form.
Thus e has a unique premise whose antecedent contains the ls-predicate. Let e′ be the premise. Thene′ has the form A1 ∗z 7→ z ′ ∗ls(z ′ , y) ⊢ ∆, where z ′ isa fresh variable. We note that A1 ∗ z 7→ z ′ ∗ ls(z ′ , y)is an Ls-form since A1 ∗ ls(z, y) is an Ls-form andz ′ is fresh. Therefore e′ is an L-form. We also have♯7→ (e) < ♯7→ (e′ ).
The case of (∗). Recall that e contains only one
ls-predicate. Hence there is a unique premise ofe that contains the ls-predicate. Let e′ be thepremise. Let A′ and ∆′ be the antecedent andsuccedent of e′ . Then A′ is an Ls-form. Since ∆ isa semi Sl-form, ∆′ is also a semi Sl-form. Therefore e′ is an L-form. Note that all 7→ of A must
be contained in A′ . Otherwise A′ is not a connected Ls-form. This contradicts Lemma 5. Hence
we have ♯7→ (e) = ♯7→ (e′ ).
Lemma 7. Suppose that there is a cut-free cyclic
proof P of ls(x, y) ⊢ sl(x, y) in CSLM
0 IDω. Then its
graph G(P) contains an infinite path (ei )i∈ω suchthat (a) e0 is ls(x, y) ⊢ sl(x, y), and (b) each ei isan L-form.
Proof. Let D be the underlying derivation tree of
P. We inductively define a finite path e0 , e1 , . . . , enof D. Let e0 be ls(x, y) ⊢ sl(x, y) at the root position of D. Suppose that e0 , . . . , ek are alreadydefined. If ek is a bud, then finish making theコンピュータソフトウェア

50(eq−1 ) :..
.

(em+1 ) :∗q−2
i=0 xi 7→ xi+1 ∗ ls(xq−1 , y) ⊢ sl(x, y)

..
..
m−1
x
→
7
x
∗
x
i
i+1
m 7→ xm+1 ∗ ls(xm+1 , y) ⊢ sl(x, y)i=0∗(em ) :∗

m−1
i=0 xi 7→ xi+1 ∗ ls(xm , y) ⊢ sl(x, y)

(UL)

..
..
p−1
(ep ) = (eq ) :i=0 xi 7→ xi+1 ∗ ls(xp , y) ⊢ sl(x, y)..
..
(e1 ) : x0 7→ x1 ∗ ls(x1 , y) ⊢ sl(x, y)(UL)(e0 ) : ls(x, y) ⊢ sl(x, y)

∗

..
.

In the above proof figure, x = x0 and each ei is the name of the corresponding sequent, the sequence (ei )i∈ω is apath, the sequence of the underlined list predicates forms an infinite progress trace that follows the path, and eq isthe companion of the bud eq−1 .
Fig. 4

Proof of Theorem 5

path with n = k. Otherwise there exists a uniquepremise e′ of ek by Lemma 6 such that e′ is an
L-form. Then we define ek+1 by e′ . Note that
this construction successfully terminates, since any
L-form cannot be the conclusion of (Id) and thenumber of sequents in D is finite.
We claim that all L-forms of D are on the path,since the premise e′′ of ek (k < n) other than ek+1
does not contain the ls-predicate and all sequentsof the subtree of D starting from e′′ do not containthe ls-predicate. Hence the companion of the bud
en appears in the path (ei )i≤n .
Finally we obtain the required infinite path(ei )i∈ω of G(P) by defining en+1 = ep , where ep
is the companion of en .
Finally we show Theorem 5. The proof is doneby combining Lemmas 6 and 7. The proof figure
given in Fig 4 explains the situation of the following
proof.
Proof of Theorem 5. Suppose that there is a cutfree cyclic proof P of ls(x, y) ⊢ sl(x, y) in
CSLM
We will show a contradiction. By
0 IDω.
Lemma 7, there is an infinite path (ei )i∈ω of G(P)such that e0 is ls(x, y) ⊢ sl(x, y) and each ei is an
L-form. By the global trace condition, there exist m ∈ ω and an infinite progressing trace (τi )i≥mthat follows the infinite path (ei )i≥m . By the construction of the path, the bud appears infinitely
many times in the path. Let ep and eq be the first
and the second occurrences of the bud in the path.
Then there is at least one progressing point be-

tween τp and τq . Hence, we have contradiction since♯7→ (ep ) < ♯7→ (eq ) = ♯7→ (ep ) by Lemma 6. Therefore
there is no cut-free cyclic proof of ls(x, y) ⊢ sl(x, y)
in CSLM
0 IDω.
By combining Proposition 4 and Theorem 5, we
can obtain our second main result.
Corollary 2. The cyclic proof system CSLM
0 IDωdoes not enjoy the cut-elimination property.

5 Conclusion and future work
In this paper, we have proved that cutelimination fails in cyclic proof systems for separation logic. We have shown the failure by presenting
counter-example sequents that can be proven withcuts but not without cuts. The counter-example sequents are reasonably simple formulas about singlylinked lists, therefore leading one to believe thatsome form of cuts is necessary for practical uses ofcyclic proofs in separation logic. Because it is nontrivial to infer arbitrary cut formulas in general,
we envisage automatic provers to include restricted
forms of cuts that are suitable for practical proof
searches. For instance, the induction hypothesis
synthesis pattern employed in Chu et al. [10] may
be a reasonable approach to this.
As future work, we plan to investigate the powerof various strategies used in cyclic-proof-based
provers that can be characterized as restricted
forms of cuts. For instance, the approach by Chu
et al. [10] can be seen as a cyclic proof system withcuts restricted to only those against buds. An openVol. 37 No. 1 Feb. 2020
question that seems worth investigating is whether
all sequents provable in cyclic proof systems areprovable with cuts only against buds.
As another line of future work, we would liketo investigate whether the cut-elimination property can be recovered by restricting the usage of
inductive definitions. Recall that our counterexamples contain multiple inductive definitions of
the same singly-linked list data structure. Perhaps
cut-elimination can be recovered if such a situation
is avoided.
Finally, we would like to investigate whether cutelimination fails or not in cyclic proof systems forlogics diﬀerent from separation logic, such as firstorder logic and bunched implication logic [6][7]. An
important diﬀerence between the cyclic proof systems for separation logic in this paper and thosein [6][7] is the existence of contraction and weakening on antecedents, which precludes a direct application of the proof technique of this paper.
Acknowledgments. We wish to thank James
Brotherston for valuable discussions about cyclic
proofs.
We also thank the anonymous referees for their helpful comments. This work is
partially supported by JSPS KAKENHI Grant
Numbers JP16H05856, JP17H01720, JP18K11161,
JP17H01723, JP18K19787, and by JSPS Core-toCore Program (A. Advanced Research Networks).
References[ 1 ] Berdine, J., Calcagno, C., O’Hearn, P. W. : A
Decidable Fragment of Separation Logic, in 24th International Conference of Foundations of Software
Technology and Theoretical Computer Science, Lodaya, K. and Mahajan, M. (eds.), Lecture Notes
in Computer Science 3328, Springer-Verlag, 2004,
pp. 97–109.
[ 2 ] Berdine, J., Calcagno, C., and O’Hearn, P. W. :Symbolic Execution with Separation Logic, in Third
Asian Symposium of Programming Languages andSystems (APLAS ’05), Yi, K. (eds.), Lecture Notes
in Computer Science 3780, Springer-Verlag, 2005,
pp. 52–68.
[ 3 ] Berardi, S. and Tatsuta, M. : Classical System of Martin-Löf’s Inductive definitions is not
equivalent to cyclic proof system, in 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS ’17),
EsparzaAndrzej, J. and Murawski, S. (eds.), Lecture
Notes in Computer Science 10203, Springer-Verlag,
2017, pp. 301–317.

51[ 4 ] Berardi, S. and Tatsuta, M. : Equivalence of
inductive definitions and cyclic proofs under arithmetic, in 32nd Annual IEEE Symposium on Logicin Computer Science (LICS ’17), Dawar, A. andGrädel, E. (eds.), ACM Press, 2017, pp. 1–12.
[ 5 ] Brotherston, J. : Sequent calculus proof systems
for inductive definitions, Ph.D thesis, Edinburgh
University, 2006.
[ 6 ] Brotherston, J. : Formalised Inductive Reasoning in the Logic of Bunched Implications, in 14th
International Symposium of Static Analysis (SAS’07), Nielson, H. R. and Filé, G. (eds.), Lecture
Notes in Computer Science 4634, Springer-Verlag,
2007, pp. 87–103.
[ 7 ] Brotherston, J.and Simpson, A. : Sequent calculi
for induction and infinite descent, Journal of Logic
and Computation, Vol. 21, No. 6 (2011), pp. 1177–
1216.
[ 8 ] Brotherston, J., Distefano, D., and Petersen,
R. L. : Automated cyclic entailment proofs inseparation logic, in 23rd International Conference
on Automated Deduction (CADE-23), Bjørner, N.
and Sofronie-Stokkermans, V. (eds.), Lecture Notes
in Computer Science 6803, Springer-Verlag, 2011,
pp. 131–146.
[ 9 ] Brotherston, J., Gorogiannis, N., and Petersen, R. L. : A Generic Cyclic Theorem Prover,in 10th Asian Symposium of Programming Languages and Systems (APLAS ’12), Jhala. R. andIgarashi, A. (eds.), Lecture Notes in Computer Science 7705, Springer-Verlag, 2012, pp. 350–367.
[10] Chu, D. H., Jaﬀar, J., and Trinh, M. T. : Automatic induction proofs of data-structures in imperative programs, in 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’15), Grove, D. and Blackburn, S.
(eds.), ACM Press, 2015, pp. 457–466.
[11] Das, A. and Pous, D. : Non-wellfounded proof
theory for (Kleene+action)(algebras+lattices), in
27th EACSL Annual Conference on Computer Science Logic (CSL ’18), Ghica, D. R. and Jung, A.
(eds.), LIPIcs, Vol. 119, Schloss Dagstuhl - LeibnizZentrum fuer Informatik, 2018, pp. 19:01–19:18.
[12] Doumane, A.: On the infinitary proof theory oflogics with fixed points, PhD thesis, Paris 7, 2017.
[13] Nguyen, H. H. and Chin, W. N. : Enhancing
Program Verification with Lemmas, in 20th International Conference of Computer Aided Verification(CAV ’08), Gupta, A. and Malik, S. (eds.), Lecture
Notes in Computer Science 5123, Springer-Verlag,
2008, pp. 355–369.
[14] Nollet, R., Saurin, A., and Tasson, C. : Local Validity for Circular Proofs in Linear Logic with Fixed
Points in 27th EACSL Annual Conference on Computer Science Logic (CSL ’18), Ghica, D. R. andJung, A. (eds.), LIPIcs, Vol. 119, Schloss Dagstuhl- Leibniz-Zentrum fuer Informatik, 2018, pp. 35:01–
35:23.

コンピュータソフトウェア

52[15] Reynolds, J. C. : Separation Logic: A Logic for
Shared Mutable Data Structures, in 17th AnnualIEEE Symposium on Logic in Computer Science(LICS ’02), Plotkin, G. (ed.), ACM Press, 2002,
pp. 55–74.
[16] Simpson, A. : Cyclic Arithmetic Is Equivalent toPeano Arithmetic, in 20th International Conference
on Foundations of Software Science and Computation Structures (FoSSaCS ’17), EsparzaAndrzej, J.
and Murawski, S. (eds.), Lecture Notes in Computer
Science 10203, Springer-Verlag, 2017, pp. 283–300.
[17] Ta, Q. T., Le, T. C., Khoo, S. C., andChin, W. N. : Automated Mutual Explicit Induction Proof in Separation Logic, in 21st International Symposium of Formal Methods (FM ’16),
Fitzgerald, J. S., Heitmeyer, C. L., Gnesi, S., andPhilippou, A. (eds.), Lecture Notes in Computer
Science 9995, Springer-Verlag, 2016, pp. 659–676.
[18] Ta, Q. T., Le, T. C., Khoo, S. C., andChin, W. N. : Automated lemma synthesis insymbolic-heap separation logic, in 45th ACM SIGPLAN Symposium on Principles of Programming
Languages (POPL ’18), Vol. 2, ACM Press, 2018,
Article No.9.

中澤巧爾

2002 年京都大学大学院理学研究科博士後期課程修了．同年，京都大学大学院情報学研究科助手．2007 年，同研究科助教．2015 年より名古屋大学
大学院情報科学研究科准教授．京都大学博士 (理学)．プログラミング言語理論，型システ
ムや，それらの論理学との関連に興味を持つ．日本ソフトウェア科学会，日本数学会，EATCS 各会員．第32 回日本ソフトウェア科学会大会高橋奨励賞を受賞．
寺内多智弘

2006 年 カ リ フ ォ ル ニ ア 大 学
バークレー校博士課程後期課程
修 了 ．Ph.D.(Computer Science)．
2007 年，東北大学大学院情報科学研究科助教．2011 年，名古屋大学大学院情報科学研究科准教授．2014 年，北陸先端科学
技術大学院大学情報科学研究科教授．2017 年より早稲田大学情報理工学科教授．プログラミング言語研
究に興味を持つ．ACM，情報処理学会各会員．

木村大輔

2007 年総合研究大学院大学複合科学
研究科情報学専攻修了．博士 (情報学)．国立情報学研究所特任研究員を経て 2016 年 4 月より東邦大学理学部情報科学科講師．プログラミング
言語理論，型理論，数理論理学に興味を持つ．現在は分離論理に基づくプログラム解析器の理論構築およびその実装を行っている．情報処理学会会員．

海野広志

2009 年東京大学大学院情報理工学系
研究科コンピュータ科学専攻博士課
程修了．博士 (情報理工学)．東北大学大学院情報科学研究科研究支援者，
東京大学大学院情報理工学系研究科
特任研究員を経て 2012 年，筑波大学システム情報系
情報工学域助教．2017 年，同准教授．プログラミン
グ言語理論．形式手法に興味を持つ．ACM，日本ソフトウェア科学会各会員．