Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Termination of Context-Sensitive Rewriting
[go: Go Back, main page]

Termination of Context-Sensitive Rewriting

A collection of examples


Contents:
    Introduction to context-sensitive rewriting
Termination of context-sensitive rewriting
The collection of examples
Contributions
References
Contact

Introduction to context-sensitive rewriting

Context-sensitive rewriting (CSR [Luc98,Luc02a]) is a simple restriction of rewriting which is formalized by imposing fixed restrictions on replacements. In CSR, a replacement map, i.e., a mapping µ (from symbols into subsets of their argument positions) is used to discriminate the argument positions on which replacements are allowed. This is inductively extended to arbitrary positions of terms built from those symbols. In this way, a restriction of rewriting is obtained.

Example 1: Consider the rules:

if(True,x,y)  -> x
if(False,x,y) -> y
defining the conditional function if. It is natural to avoid rewritings on the second and third argument of if. This is easily achieved with CSR by defining µ(if)={1}.
Context-sensitive rewriting has been proved useful for describing semantic aspects of programming languages (e.g., Maude, OBJ2, OBJ3, or CafeOBJ) and analyzing the computational properties (e.g., termination or completeness) of the corresponding programs [AEL03, Luc01a, Luc01b, Luc03b ].

Termination of context-sensitive rewriting

Restrictions of rewriting can eventually achieve termination by pruning all infinite rewrite sequences issued from every term.

Example 2: Consider the TRS:

first(0,X)            -> nil
first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
from(X)               -> cons(X,from(s(X)))
In order to avoid infinite rewritings with expressions involving calls to from, it is natural to forbid rewritings on the second argument of the list constructor cons. It is possible to prove that such context-sensitive computations are terminating (see Example number 11 below).

Fortunately, a number of methods have been developed for proving the µ-termination of a TRS R (i.e., termination of CSR for R and the replacement map µ). Basically, we have:

  • Direct methods, i.e., orderings > on terms which can be used to directly compare the left-hand sides and right-hand sides of the rules in order to conclude the µ-termination of the TRS, see [BLR02, Bor03, GL02b, Luc04, Zan97].
  • Transformations from TRSs R and replacement maps µ that obtain a TRS R'. If we are able to prove termination of R' (using the standard methods), then the µ-termination of R is ensured, see [FR99, GM04, Luc96a, Zan97].

There is a tool, MU-TERM, which implements many of these techniques for proving termination of CSR.

The collection of examples

The following table collects examples of non-terminating TRSs which become terminating after imposing some replacement restrictions by using a replacement map µ, i.e., they all are (supposed to be) µ-terminating. The only exception is [GM04, Example 49] (number 40 in the table below) which is terminating without introducing any replacement restriction. The collection is quite complete. The examples have been all processed with MU-TERM .

The column origin splits up into three columns which help to identify the origin of each example. A green cell in the column label means that the replacement map µ in the example is canonical, i.e., the non-variable parts of every left-hand side of the rules of the TRS are µ-replacing. The icon indicates that the system admits a safe modular decomposition in the sense that a proof of µ-termination for each component of the decomposition implies the µ-termination of the whole system (see [GL02a]). The decomposition is automatically computed by MU-TERM when the CS-TRS is loaded. The use of canonical replacement maps permits to use CSR as a suitable tool for (infinitary) normalization, computation of values, head-normal forms, etc; we refer to [Luc98] and [Luc02a] for further details in this respect. Regarding proofs of termination of (canonical) CSR, some interesting properties of the existing methods have been investigated in [Luc02b] .

The column source permits to obtain the description of the TRS and the replacement map. We provide two different descriptions:

  • TPDB format: Termination of CSR is one of the subcategories of termination of rewriting which is included in the Termination Problems Data Base (TPDB). It is possible to specify a term rewriting system with context-sensitive replacement restrictions (given by a replacement map) by using the TPDB format
  • OBJ format: provides a more compact description as an OBJ module (which is also compatible with the Maude syntax). Here, the replacement map is described by means of strategy annotations (i1 ··· in 0) associated to each symbol; this means that µ(f)={i1,...,in}, if the arity of f is k. (see [Luc03b]). Symbols f without any strategy OBJ module have no replacement restriction, i.e., µ(f)={1,...,k}.
The column direct methods contains documented proofs of termination which have been achieved by using some of the existing orderings for proving termination of CSR: the Context-Sensitive Knuth Bendix Ordering of [Bor03]; the Context-Sensitive Recursive Path Ordering of [BLR02]; and the use of polynomial orderings first introduced in [GL02b] and further developed in [Luc04], and the Context-Sensitive Dependency Pairs [AGL06]. A blue cell with a question mark inside (  ) means that no documented proof (or disproof) of µ-termination has been reported yet; on the other hand, a 'check' mark (  ) means that, although no proof has been reported yet, such a proof is (at least theoretically) possible, according to the results in the literature. A green cell means that the corresponding direct method was successfully applied to prove µ-termination of the example; the text inside refers to the paper which describes the proof. The presence of
  1. means that a safe modular decomposition has been used to obtain the proof with the corresponding basic technique, and
  2. means that the proof can be done automatically (possibly combining different tools).
Finally, a yellow cell means that the corresponding direct method cannot be used to prove µ-termination of the example; again, the text inside refers to the paper which describes the negative result. In all cases, links to an HTML document reporting more details are given.

The column transformations contains documented proofs of termination which have been achieved by using some of the existing transformations for proving termination of CSR, see [FR99], [GM04], [Luc96a] and [Zan97]. As for the column direct methods , each cell is coloured and labelled accordingly.

The column others collects documented proofs of termination which have been achieved by using a different technique. For instance: an ad-hoc µ-reduction ordering [Zan97], a modular proof of µ-termination [GL02a] [GL02b], the use of some semantic path ordering for CSR [Bor03], or the use of polynomial fractions [Luc04] .

The column report points to an HTML file containing the complete record of each example: the source of the example and information regarding the proofs of µ-termination.

The collection of all examples (in OBJ/Maude format) is here.

The collection of all examples (in TPDB format) is here .

-->
NUMBER ORIGIN SOURCE FORMATS DIRECT METHODS TRANSFORMATIONS OTHERS REPORT
Reference Conference / Journal Label TPDB OBJ CSKBO CSRPO POL CSDPs [FR99] [GM04] [Luc96b] [RTA97]
1 [Luc96b, Example 4.4] ICALP'96 Ex4_4_Luc96b tpdb obj report report report report [Luc96b, Ex 4.23] report
2 [Luc96a, Example 3.12] PLILP'96 Ex3_12_Luc96a tpdb obj report [Luc04, Ex 8] [Luc98, Sec 4.1] [Zan97, Ex 3] [Zan97, Ex 2] report
3 [Zan97,Introduction] RTA'97 ExIntrod_Zan97 tpdb obj report report report report
4 [Zan97, Example 1] RTA'97 Ex1_Zan97 tpdb obj report [Luc04, Ex 2] report [GM03, Ex 16] [GM03, Ex 16] [GM03, Ex 16] [GM03, Ex 16] [Zan97, Ex 1] report
5 [Zan97, Example 4] RTA'97 Ex4_Zan97 tpdb obj report report [Zan97, Ex 4] report
6 [Zan97, Example 5] RTA'97 Ex5_Zan97 tpdb obj report [Luc04, Ex 11] report report report report [Zan97, Ex 5] report
7 [Zan97, Conclusions] RTA'97 ExConc_Zan97 tpdb obj report report report [FR99, Ex 3] report report [Zan97, Conclusions] report
8 [Luc97, Example 3.2] PLILP'97 Ex3_2_Luc97 tpdb obj report report
9 [Luc97, Example 5.7] PLILP'97 Ex5_7_Luc97 tpdb obj report report
10 [Luc97, Example 5.8] PLILP'97 Ex5_8_Luc97 tpdb obj report report
11 [Luc98, Example 6] JFLP'98 Ex6_Luc98 tpdb obj report report report report [Luc03b, Sec 2.5.4] [Luc98, Sec 4.1] [Luc03b, Sec 2.5.2] report
12 [Luc98, Example 15] JFLP'98 Ex15_Luc98 tpdb obj report report report report report report report
13 [GM99, Introduction] RTA'99 ExIntrod_GM99 tpdb obj report report report
14 [GM99, Example 1] RTA'99 Ex1_GM99 tpdb obj [GL02b, Sec 5.1] [GL02b, Ex 9] report [GM04, Ex 15] [GM04, Ex 15] [GM04, Ex 15] [GM04, Ex 15] [GL02a, Ex 10] report
15 [GM01, Introduction] RPC'01 ExIntrod_GM01 tpdb obj [BLR02, Ex 10] report report [GM01, Sec 2] report [GM01, Sec 2] [GM01, Sec 2] report
16 [Luc02b, Example 1] RTA'02 Ex1_Luc02b tpdb obj report report [Luc02b, Ex 8] [Luc02b, Ex 8] report
17 [BLR02, Example 7] CADE'02 Ex7_BLR02 tpdb obj report report [BLR02, Sec 5] report report
18 [BLR02, Example 8] CADE'02 Ex8_BLR02 tpdb obj report report [BLR02, Sec 5] report report
19 [BLR02, Example 9] CADE'02 Ex9_BLR02 tpdb obj report report report report report report report
20 [GL02a, Example 1] PPDP'02 Ex1_GL02a tpdb obj report [GL02a, Ex 9] report report report [GL02a, Ex 2] report report
21 [AEL02, Example 6.15] WRLA'02 Ex6_15_AEL02 tpdb obj [Bor03, Ex 3.3.26] report report
22 [Luc02a, Example 2] IC'02 Ex2_Luc02a tpdb obj report report [Luc02a, Ex 3] report report
23 [Luc02a, Section 11.1] IC'02 ExSec11_1_Luc02a tpdb obj report report [Luc02a, Ex 3] report report
24 [Luc02c, Example 1.2] ENTCS volume 64 Ex1_2_Luc02c tpdb obj report report report report report report report report
25 [Luc02c, Example 6.9] ENTCS volume 64 Ex6_9_Luc02c tpdb obj report report report report
26 [AEGL02, Example 14] LPAR'02 Ex14_AEGL02 tpdb obj report report report report report report report report
27 [GM03, Example 1] DLT'02 Ex1_GM03 tpdb obj [Luc03b, Sec 6.2] report [GM02, Appendix A.2] report
28 [Bor03, Example 3.3.25] PhD Thesis Ex3_3_25_Bor03 tpdb obj report report report report [Bor03, Ex 3.3.25] report
29 [Bor03, Example 4.7.15] PhD Thesis Ex4_7_15_Bor03 tpdb obj [Bor03, Ex 4.7.15] report report report report report report [Bor03, Ex 4.7.15] report
30 [Bor03, Example 4.7.37] PhD Thesis Ex4_7_37_Bor03 tpdb obj [Bor03, Ex 4.7.37] report report report [Bor03, Ex 4.7.37] report
31 [Bor03, Example 4.7.56] PhD Thesis Ex4_7_56_Bor03 tpdb obj report report report report report [Bor03, Ex 4.7.56] report
32 [Bor03, Example 4.7.77] PhD Thesis Ex4_7_77_Bor03 tpdb obj [Bor03, Ex 4.7.77] report report report report report report report report
33 [Luc03b, Example 2] TR'03 Ex2_Luc03b tpdb obj report report report report report [Luc03b, Example 11] report report
34 [Luc03b, Example 26] TR'03 Ex26_Luc03b tpdb obj report report report report report report
35 [AEL03, Example 1.2] RULE'03 Ex1_2_AEL03 tpdb obj report report report report
36 [AEL03, Appendix B] RULE'03 ExAppendixB_AEL03 tpdb obj report report report report
37 [GM04, Introduction] JFP'04 ExIntrod_GM04 tpdb obj report [Luc04, Ex 3] report [GM04, Sec 3] [GM04, Ex 17] [GM04, Sec 3] [GM04, Sec 3] report
38 [GM04, Example 6] JFP'04 Ex6_GM04 tpdb obj report report report [GM04, Ex 6] report [GM04, Ex 6] [GM04, Ex 6] report
39 [GM04, Example 24] JFP'04 Ex24_GM04 tpdb obj report [Luc04, Ex 12] report report report report report report
40 [GM04, Example 49] JFP'04 Ex49_GM04 tpdb obj report [Luc04, Ex 7] [GM04, Ap D] report report report
41 [Luc04, Example 9] FOSSACS'04 Ex9_Luc04 tpdb obj report report report report report report [Luc04, Ex 9] report
42 [Luc04b, Example 1] RTA'04 Ex1_Luc04b tpdb obj report [Luc04b, Fig 2] report report [Luc04b, Fig 4] report report report
43 [DLMMU04, Example 4] PEPM'04 Ex4_DLMMU04 tpdb obj report report
44 [DLMMU04, Example 5] PEPM'04 Ex5_DLMMU04 tpdb obj report report report report report report
45 [DLMMU04, Example Section 4.2] PEPM'04 ExSec4_2_DLMMU04 tpdb obj report report report report report
46 [Luc06, Example 9] IC'06 Ex9_Luc06 tpdb obj report report report report report
47 [Luc06, Example 14] IC'06 Ex14_Luc06 tpdb obj report report report report
48 [Luc06, Example 15] IC'06 Ex15_Luc06 tpdb obj report report report report report report report
49 [Luc06, Example 16] IC'06 Ex16_Luc06 tpdb obj report report report report report report
50 [Luc06, Example 18] IC'06 Ex18_Luc06 tpdb obj report report report report report report report report
51 [Luc06, Example 23] IC'06 Ex23_Luc06 tpdb obj report report report report report report report report
52 [Luc06, Example 24] IC'06 Ex24_Luc06 tpdb obj report report report report report report
53 [Luc06, Example 25] IC'06 Ex25_Luc06 tpdb obj report report report report report report report report
54 [Luc06, Example Proposition 7] IC'06 ExProp7_Luc06 tpdb obj report report report report report report

Contributions

If you want to

  • Propose a new example,
  • Provide a proof for some of the existing examples,
  • Make any comment or suggestion, or
  • Help to fix some bug,
please, do not hesitate to contact me. Send your message to slucas@dsic.upv.es .

Apart from the authors of papers enumerated below, the following people have contributed to solve the examples in this collection.

  • Cristina Borralleras
  • Albert Rubio

References

Contact

Salvador Lucas

Please, report any bug, comment, or suggestion to: slucas@dsic.upv.es

Last update : June 23, 2006
On line after: January 15, 2004