Updated: Jul 27, 2015

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

Ver. 1.1 (August 1st, 2014)

Developed by Naoki Nishida (Nagoya University), Karl Gmeiner (UAS Technikum Wien), and Makishi Yanagisawa (Nagoya University)


News

July 27th, 2015
Added System Description.
August 4th, 2014
Updated the list of developers, Overview, Experiments for Ver. 1.1, Web Interface, and Implemented Procedure, and added Participation in Competition to this page.
August 1st, 2014

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. 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

The tool supports normal 1-CTRSs without any strategy and theory (specified by STRATEGY and THEORY, resp.), the class of which includes TRSs. The implemented techniques for TRSs are very poor since the tool is focusing on CTRSs. Due to a technical reason as shown later, indeed the tool is working for weakly left-linear CTRSs which has at least one condition.

NOTE: the current version (Ver. 1.0) accepts oriented 1-CTRSs, and returns NO if the disproving criterion below is satisfied, and otherwise, returns MAYBE whenever the input is not normal 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
        • st iff |s| ≥ |t| and ∀xV. |s|x ≥ |t|x and
        • s > t iff |s| > |t| and ∀xV. |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.


Experiments

July 3rd, 2014 (for Ver. 1.1)

Benchmarks
1.trs-402.trs in Cops
Environment
StarExec
Results
Categories Yes No Maybe Others
oriented 1-CTRSs (48) 15 13 20 0
TRSs (262) 23 5 234 0

July 2nd, 2014 (for Ver. 1.0)

Benchmarks
1.trs-402.trs in Cops
Environment
StarExec
Results
Categories Yes No Maybe Others
oriented 1-CTRSs (48) 13 13 22 0
TRSs (262) 15 3 244 0

Participation in Competition

CoCo 2014


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)]


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