Updated: Mar 11, 2019

CO3: a COnverter for proving COnfluence of COnditional term rewriting systems

Ver. 2.0 (March 11th, 2019)

Currently developed by Naoki Nishida (Nagoya University), and Yuya Maeda (Nagoya University)

News

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 1-CTRS 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

Web Interface

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)
)
co3-test-1.trs for testing the critical pair theorem
(RULES
  f(a) -> b
  f(a) -> c
  b -> d
  c -> d
)
co3-test-2.trs for testing the critical pair theorem
(RULES
  f(a) -> b
  f(a) -> c
  b -> d(e)
  c -> d(e)
)
Other normal 1-CTRSs
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:

  1. If R is a normal 1-CTRS, then go to the next step; otherwise, return UNSUPPORTED.
  2. 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.
  3. If R is a TRS, then let R1 be R; if SR is sound for R (i.e., R is weak left-linear), then let R1 be a TRS obtained by applying the optimized simultaneous unraveling [GNG13iwc] to R, and let R2 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.
  4. If R1 or R2 satisfies one of the following (i.e., R1 or R2 is confluent), then return YES, and otherwise, return MAYBE:
    • Ri is orthogonal, or
    • Ri satisfies one of the following (i.e., Ri is terminating),
      • Ri has no dependency pair in the union of the SCCs in the simple estimated dependency graph, or
      • Ri ⊆ ≥ and DP(Ri) ⊆ > 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 Ri 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. 24-28, 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. 39-50, 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. 35-39, 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

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.nagoya-u.ac.jp