Advertisement

Decidability of reachability and disjoint union of term rewriting systems

  • Anne -Cécile Caron
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 581)

Abstract

The reachability problem for term rewriting systems is to decide whether, given a system S and two terms t and t′, t can be reduced in t′ with rules of S. We study the disjoint union of term rewriting systems whose reachability problem is decidable and give sufficient conditions for obtaining the modularity of decidability of this problem.

Keywords

Disjoint Union Inference Rule Ground Term Reachability Problem Modular Property 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [BJW82]
    R.V. Book, M. Jantzen, and C. Wrathall. Monadic Thue systems. Theoretical Computer Science, 19(3):231–252, 1982.Google Scholar
  2. [Dro89]
    K. Drosten. Termersetzungssysteme. Informatik-Fachberichte 210, Springer, Germany, 1989.Google Scholar
  3. [GB85]
    J.H. Gallier and R.V. Book. Reductions in tree replacement systems. Theoretical Computer Science, 37(2):123–150, 1985.Google Scholar
  4. [KO90]
    M. Kurihara and A. Ohuchi. Modularity of simple termination of term rewriting systems. Journal of IPS Japan, 31(5):633–642, 1990.Google Scholar
  5. [Mid89a]
    A. Middeldorp. Modular aspects of properties of term rewriting systems related to normal forms. In Lecture Notes in Computer Science Vol 355, pages 263–277, Chapel Hill, 1989. 3rd International Conference on Rewriting Techniques and Applications. Full version: Report IR-164, Vrije Universiteit, Amsterdam, 1988.Google Scholar
  6. [Mid89b]
    A. Middeldorp. A sufficient condition for the termination of the direct sum of term rewriting systems. In Proceeding of the 4th IEEE Symposium on Logic in Computer Science, pages 396–401, Pacific Grove, 1989.Google Scholar
  7. [Mid90]
    A. Middeldorp. Modular Properties of Term Rewriting Systems. PhD thesis, Vrije Universiteit, Amsterdam, 1990.Google Scholar
  8. [Mid91]
    A. Middeldorp. Modular properties of conditional term rewriting systems. Report CS R9105, Centre for Mathematics and Computer Science, Amsterdam, 1991.Google Scholar
  9. [Oya86]
    M. Oyamaguchi. The reachability problem for quasi-ground term rewriting systems. Journal of Information Processing, pages 9–4, 1986.Google Scholar
  10. [Rus87]
    M. Rusinowitch. On termination of the direct sum of term rewriting systems. Information Processing Letters, 26:65–70, 1987.Google Scholar
  11. [TKB89]
    Y. Toyama, J.W. Klop, and H.P. Barendregt. Termination for the direct sum of left-linear term rewriting systems. In Lecture Notes in Computer Science Vol 355, pages 477–491, Chapel Hill, 1989. 3rd International Conference on Rewriting Techniques and Applications.Google Scholar
  12. [Toy87a]
    Y. Toyama. Counterexamples to termination for the direct sum of term rewriting systems. Information Processing Letters, 25:141–143, 1987.Google Scholar
  13. [Toy87b]
    Y. Toyama. On the Church-Rosser property for the direct sum of term rewriting systems. Journal of the ACM, 34(1):128–143, 1987.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Anne -Cécile Caron
    • 1
  1. 1.Laboratoire d'Informatique Fondamentale de Lille UFR IEEA. UA 369 CNRSUniversité des Sciences et Techniques de Lille IVilleneuve d'Ascq CedexFrance

Personalised recommendations