Non-Looping String Rewriting

Alfons Geser; Hans Zantema

RAIRO - Theoretical Informatics and Applications (2010)

  • Volume: 33, Issue: 3, page 279-301
  • ISSN: 0988-3754

Abstract

top
String rewriting reductions of the form t → R + u t v , called loops, are the most frequent cause of infinite reductions (non- termination). Regarded as a model of computation, infinite reductions are unwanted whence their static detection is important. There are string rewriting systems which admit infinite reductions although they admit no loops. Their non-termination is particularly difficult to uncover. We present a few necessary conditions for the existence of loops, and thus establish a means to recognize the difficult case. We show in detail four relevant criteria: (i) the existence of loops is characterized by the existence of looping forward closures; (ii) dummy elimination, a non-termination preserving transformation method, also preserves the existence of loops; (iii) dummy introduction, a transformation method that supports subsequent dummy elimination, likewise preserves loops; (iv) bordered systems can be reduced to smaller systems on a larger alphabet, preserving the existence and the non-existence of loops. We illustrate the power of the four methods by giving a two-rule string rewriting system over a two-letter alphabet which admits an infinite reduction but no loop. So far, the least known such system had three rules.

How to cite

top

Geser, Alfons, and Zantema, Hans. "Non-Looping String Rewriting." RAIRO - Theoretical Informatics and Applications 33.3 (2010): 279-301. <http://eudml.org/doc/222096>.

@article{Geser2010,
abstract = { String rewriting reductions of the form $t\to_R^+ utv$, called loops, are the most frequent cause of infinite reductions (non- termination). Regarded as a model of computation, infinite reductions are unwanted whence their static detection is important. There are string rewriting systems which admit infinite reductions although they admit no loops. Their non-termination is particularly difficult to uncover. We present a few necessary conditions for the existence of loops, and thus establish a means to recognize the difficult case. We show in detail four relevant criteria: (i) the existence of loops is characterized by the existence of looping forward closures; (ii) dummy elimination, a non-termination preserving transformation method, also preserves the existence of loops; (iii) dummy introduction, a transformation method that supports subsequent dummy elimination, likewise preserves loops; (iv) bordered systems can be reduced to smaller systems on a larger alphabet, preserving the existence and the non-existence of loops. We illustrate the power of the four methods by giving a two-rule string rewriting system over a two-letter alphabet which admits an infinite reduction but no loop. So far, the least known such system had three rules. },
author = {Geser, Alfons, Zantema, Hans},
journal = {RAIRO - Theoretical Informatics and Applications},
keywords = {string rewriting; semi-thue system; termination; loop; term rewriting; transformation ordering; dummy introduction; dummy elimination; overlap closure; forward closure.; string rewriting reductions; loops},
language = {eng},
month = {3},
number = {3},
pages = {279-301},
publisher = {EDP Sciences},
title = {Non-Looping String Rewriting},
url = {http://eudml.org/doc/222096},
volume = {33},
year = {2010},
}

TY - JOUR
AU - Geser, Alfons
AU - Zantema, Hans
TI - Non-Looping String Rewriting
JO - RAIRO - Theoretical Informatics and Applications
DA - 2010/3//
PB - EDP Sciences
VL - 33
IS - 3
SP - 279
EP - 301
AB - String rewriting reductions of the form $t\to_R^+ utv$, called loops, are the most frequent cause of infinite reductions (non- termination). Regarded as a model of computation, infinite reductions are unwanted whence their static detection is important. There are string rewriting systems which admit infinite reductions although they admit no loops. Their non-termination is particularly difficult to uncover. We present a few necessary conditions for the existence of loops, and thus establish a means to recognize the difficult case. We show in detail four relevant criteria: (i) the existence of loops is characterized by the existence of looping forward closures; (ii) dummy elimination, a non-termination preserving transformation method, also preserves the existence of loops; (iii) dummy introduction, a transformation method that supports subsequent dummy elimination, likewise preserves loops; (iv) bordered systems can be reduced to smaller systems on a larger alphabet, preserving the existence and the non-existence of loops. We illustrate the power of the four methods by giving a two-rule string rewriting system over a two-letter alphabet which admits an infinite reduction but no loop. So far, the least known such system had three rules.
LA - eng
KW - string rewriting; semi-thue system; termination; loop; term rewriting; transformation ordering; dummy introduction; dummy elimination; overlap closure; forward closure.; string rewriting reductions; loops
UR - http://eudml.org/doc/222096
ER -

References

top
  1. S. Adjan and G. Oganesjan, Problems of equality and divisibility in semigroups with a single defining relation. Mat. Zametki41 (1987) 412-421.  
  2. R. Book and F. Otto, String-rewriting systems. Texts and Monographs in Computer Science. Springer, New York (1993).  
  3. N. Dershowitz, Termination of linear rewriting systems. In Proc. of the 8th InternationalColloquium on Automata, Languages and Programming (ICALP81), Springer, Lecture Notes in Computer Science115 (1981) 448-458.  
  4. N. Dershowitz, Termination of rewriting. J. Symb. Comput.3 (1987) 69-115; Corrigendum4 (1987) 409-410.  
  5. N. Dershowitz and C. Hoot, Natural termination. Theoret. Comput. Sci.142 (1995) 179-207.  
  6. M. Ferreira and H. Zantema, Dummy elimination: Making termination easier. In Proc. 10th Conf. Fundamentals of Computation Theory, H. Reichel, Ed., Springer, Lecture Notes in Computer Science965 (1995) 243-252.  
  7. A. Geser, Termination of one-rule string rewriting systems ℓ → r where |r| ≤ 9. Tech. Rep., Universität Tübingen, D (Jan. 1998).  
  8. J.V. Guttag, D. Kapur and D.R. Musser, On proving uniform termination and restricted termination of rewriting systems. SIAM J. Comput.12 (1983) 189-214.  
  9. G. Huet and D.S. Lankford, On the uniform halting problem for term rewriting systems. Rapport Laboria 283, INRIA (1978).  
  10. M. Jantzen, Confluent string rewriting, Vol. 14 of EATCS Monographs on TheoreticalComputer Science. Springer, Berlin (1988).  
  11. Y. Kobayashi, M. Katsura and K. Shikishima-Tsuji, Termination and derivational complexity of confluent one-rule string rewriting systems. Tech. Rep., Dept. of Computer Science, Toho University, JP (1997).  
  12. W. Kurth, Termination und Konfluenz von Semi-Thue-Systemen mit nur einer Regel. Dissertation, Technische Universität Clausthal, Germany (1990).  
  13. W. Kurth, One-rule semi-Thue systems with loops of length one, two, or three. RAIRO Theoret. Informatics Appl.30 (1995) 415-429.  
  14. D.S. Lankford and D.R. Musser, A finite termination criterion. Tech. Rep., Information Sciences Institute, Univ. of Southern California, Marina-del-Rey, CA (1978).  
  15. Y. Matiyasevitch and G. Sénizergues, Decision problems for semi-Thue systems with a few rules. In IEEE Symp. Logic in Computer Science'96 (1996).  
  16. R. McNaughton, The uniform halting problem for one-rule Semi-Thue Systems. Tech. Rep. 94-18, Dept. of Computer Science, Rensselaer Polytechnic Institute, Troy, NY, Aug. 1994. See also ``Correction to The Uniform Halting Problem for One-rule Semi-Thue Systems'', personal communication (Aug. 1996).  
  17. R. McNaughton, Well-behaved derivations in one-rule Semi-Thue Systems. Tech. Rep. 95-15, Dept. of Computer Science, Rensselaer Polytechnic Institute, Troy, NY (Nov. 1995).  
  18. R. McNaughton, Semi-Thue Systems with an inhibitor. Tech. Rep. 97-5, Dept. of Computer Science, Rensselaer Polytechnic Institute, Troy, NY (1997).  
  19. F. Otto, The undecidability of self-embedding for finite semi-Thue and Thue systems. Theoret. Comput. Sci.47 (1986) 225-232.  
  20. B.K. Rosen, Tree-manipulating systems and Church-Rosser Theorems. J. ACM20 (1973) 160-187.  
  21. K. Shikishima-Tsuji, M. Katsura and Y. Kobayashi, On termination of confluent one-rule string rewriting systems. Inform. Process. Lett.61 (1997) 91-96.  
  22. C. Wrathall, Confluence of one-rule Thue systems. In Word Equations and Related Topics, K.U. Schulz, Ed., Springer, Lecture Notes in Computer Science572 (1991).  
  23. H. Zantema and A. Geser, A complete characterization of termination of 0p 1q → 1r 0s.Applicable Algebra in Engineering, Communication, and Computing. In print.  
  24. H. Zantema and A. Geser, A complete characterization of termination of 0p 1q → 1r 0s. In Proc. of the 6th Conference on Rewriting Techniques and Applications, J. Hsiang, Ed., Springer, Lecture Notes in Computer Science914 (1995) 41-55.  

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.