Contents
Overview
CO3 is a tool for proving confluence of conditional term
rewriting systems (CTRS) by using a transformational approach.
The tool is based on the results in [GNG13iwc]
and [NYG14iwc]:
the tool first transforms a given normal 1CTRS into an unconditional
term rewriting system (TRS) by using
the simultaneous unraveling [GNG13iwc]
or the SR transformation [Serbanuta & Rosu, RTA 2006],
and then verify confluence of the transformed TRS.
CO3 is using syntactic analyses only:
a syntactic transformation, syntactic criteria for checking properties, etc.,
except for the normalization for checking joinability of critical pairs.
For this reason, CO3 is very efficient.
To make the confluence checking more powerful, we should implement more powerful
methods for proving confluence of TRSs, e.g., the critical pair theorem with using
powerful termination proving methods. However, this tool is focusing on converting
a CTRS to a TRS which help us to analyse the CTRS, and thus, we won't strengthen
an internal termination prover, or any confluence proving technique.
We want to use CO3 with other confluence provers.
History
 Ver. 2.0 (March 11th, 2019)

An infeasibility analysis based on narrowing trees has been implemented.
 Ver. 1.1 (August 1st, 2014)

the improved version for participating in CoCo 2014.
 Ver. 1.0 (June 27th, 2014)

the first version for participating in CoCo 2014.
 Ver. 0 (June 26th, 2014)

a prototype version.
Supported Classes
Oriented CTRSs
Examples
 [NYG14iwc, Example 2]

(CONDITIONTYPE ORIENTED)
(VAR x)
(RULES
e(0) > true
e(s(x)) > true  e(x) == false
e(s(x)) > false  e(x) == true
)
 [NYG14iwc, Example 8]

(CONDITIONTYPE ORIENTED)
(VAR x)
(RULES
e(0) > true
e(s(x)) > true  o(x) == true
e(s(x)) > false  e(x) == true
o(0) > true
o(s(x)) > true  e(x) == true
o(s(x)) > false  o(x) == true
)
 [NYG14iwc, Example 9]

(CONDITIONTYPE ORIENTED)
(VAR x y l)
(RULES
dot(x,dot(y,l)) > dot(y,dot(x,l))  les(x,y) == true
les(0,0) > false
les(0,s(0)) > true
les(0,s(s(x))) > les(0,s(x))
les(s(0),0) > false
les(s(s(x)),0) > les(s(x),0)
les(s(x),s(y)) > les(x,y)
)
co3test1.trs
for testing the critical pair theorem

(RULES
f(a) > b
f(a) > c
b > d
c > d
)
co3test2.trs
for testing the critical pair theorem

(RULES
f(a) > b
f(a) > c
b > d(e)
c > d(e)
)
 Other normal 1CTRSs
 See Cops.
 Other TRSs
 See Cops.
Implemented Procedure (Ver. 1.1)
The tool takes a CTRS R as input, and then starts the following process:
 If R is a normal 1CTRS, then go to the next step;
otherwise, return
UNSUPPORTED
.
 If R satisfies one of the following, then return
NO
, and
otherwise, go to the next step:

there exists an unconditional critical pair (s, t) of R such that
cap(s) and cap(s) are not unifiable, where cap replaces any term rooted by a defined symbol by a fresh variable,
,
or
 there exists an unconditional critical pair (s, t) of R such that
s and t are different strongly irreducible ground terms of R.
 If R is a TRS, then let R_{1} be R;
if SR is sound for R (i.e., R is weak leftlinear),
then let R_{1} be a TRS obtained by
applying the optimized simultaneous unraveling [GNG13iwc] to
R,
and let R_{2} be a TRS obtained by
applying the optimized SR transformation [Serbanuta & Rosu, RTA 2006] to
R, while the special bracket symbol and its rewrite
rules are not introduced whenever R is a constructor system;
otherwise, return
MAYBE
.
 If R_{1} or R_{2} satisfies one of the following (i.e., R_{1} or R_{2} is confluent), then
return
YES
,
and otherwise, return MAYBE
:
 R_{i} is orthogonal,
or
 R_{i} satisfies one of the following (i.e., R_{i} is terminating),
 R_{i} has no dependency pair in the union of the SCCs in the simple estimated dependency graph,
or
 R_{i} ⊆ ≥ and DP(R_{i}) ⊆ > where
 s ≥ t iff s ≥ t
and ∀x∈V. s_{x} ≥ t_{x}
and
 s > t iff s > t
and ∀x∈V. s_{x} ≥ t_{x}
(see [Baader & Nipkow, 92, Example 5.2.2]),
and
all the critical pairs of R_{i} are joinable.
Procedures in the old versions can be seen here.
Participation in Competition since 2014
See CoCo webpage, and
results.
References
 [NYG14iwc]
 Naoki Nishida, Makishi Yanagisawa, and Karl Gmeiner,
On Proving Confluence of Conditional Term Rewriting Systems via the Computationally Equivalent Transformation,
In Proceedings of the 3rd International Workshop on Confluence (IWC 2014),
pp. 2428, Vienna, July 2014.
[PDF]
[PDF (preprint)]
 [NYG14wpte]
 Naoki Nishida, Makishi Yanagisawa, and Karl Gmeiner,
On Proving Soundness of the Computationally Equivalent Transformation for Normal Conditional Term Rewriting Systems by Using Unravelings,
In Proceedings of the first International Workshop on ewriting Techniques for Program Transformations and Evaluation (WPTE 2014),
OpenAccess Series in Informatics (OASIcs), Vol. 40, pp. 3950, Vienna, July 2014.
[Link (OASIcs)]
[Link (local with a full version)]
 [GNG13iwc]
 Karl Gmeiner, Naoki Nishida, and Bernhard Gramlich,
Proving Confluence of Conditional Term Rewriting Systems via Unravelings,
In Proceedings of the 2nd International Workshop on Confluence (IWC 2013),
pp. 3539, Eindhoven, June 2013.
[PDF]
[PDF (preprint)]
System Description
 [NKYG15v1.2]
 Naoki Nishida, Takayuki Kuroda, Makishi Yanagisawa, and Karl Gmeiner,
CO3: a COnverter for proving COfluence of COnditional TRSs (Version 1.2),
In Proceedings of the 4th International Workshop on Confluence (IWC 2015),
to appear, Berlin, August 2015.
[PDF (full version)]
Past Contributors
 Karl Gmeiner (UAS Technikum Wien)
 Makishi Yanagisawa (Nagoya University)
 Yoshiaki Kanazawa (Nagoya University)
 Takayuki Kuroda (Nagoya University)
 Yuta Tsuruta (Nagoya University)
Acknowledgement
The research in this paper was partly supported by the Austrian Science
Fund (FWF) international project I963 and the Japan Society for the
Promotion of Science (JSPS).
Contact
 ML for CO3 developers
co3 @ trs.css.i.nagoyau.ac.jp