Advertisement

Termination for the direct sum of left-linear term rewriting systems

Preliminary draft
  • Yoshihito Toyama
  • Jan Willem Klop
  • Hendrik Pieter Barendregt
Regular Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 355)

Abstract

The direct sum of two term rewriting systems is the union of systems having disjoint sets of function symbols. It is shown that two term rewriting systems both are left-linear and complete if and only if the direct sum of these systems is so.

Keywords

Induction Hypothesis Function Symbol Modular Property Case Rank Preliminary Draft 
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. [1]
    G. Huet and D. C. Oppen, Equations and rewrite rules: a survey, in: R. Book, ed., Formal languages: perspectives and open problems (Academic Press, 1980) 349–393.Google Scholar
  2. [2]
    N. Dershowitz. Termination of linear rewriting systems: Preliminary version, Lecture Notes in Comput. Sci. 115 (Springer-Verlag, 1981) 448–458.Google Scholar
  3. [3]
    H. Ganzinger and R. Giegerich, A note on termination in combinations of heterogeneous term rewriting systems, EATCS Bulletin 31 (1987) 22–28.Google Scholar
  4. [4]
    J. W. Klop and H. P. Barendregt, Private communication (January 19, 1986).Google Scholar
  5. [5]
    A. Middeldorp, A sufficient condition for the termination of the direct sum of term rewriting systems, Preliminary Draft, Report IR-150, Free University, Amsterdam (1988).Google Scholar
  6. [6]
    A. Middeldorp, Modular aspects of properties of term rewriting systems related to normal forms, Preliminary Draft, Free University, Amsterdam (September 1988).Google Scholar
  7. [7]
    M. Rusinowitch, On termination of the direct sum of term rewriting systems, Inform. Process. Lett. 26 (1987) 65–70.Google Scholar
  8. [8]
    Y. Toyama, On the Church-Rosser property for the direct sum of term rewriting systems, J. ACM 34 (1987) 128–143.Google Scholar
  9. [9]
    Y. Toyama, Counterexamples to termination for the direct sum of term rewriting systems, Inform. Process. Lett. 25 (1987) 141–143.Google Scholar
  10. [10]
    Y. Toyama, Commutativity of term rewriting systems, in: K. Fuchi and L. Kott, eds., Programming of Future Generation Computer II (Norht Holland 1988) 393–407.Google Scholar
  11. [11]
    Y. Toyama, J.W. Klop, H.P. Barendregt, Termination for the direct sum of left-linear term rewriting systems: Preliminary draft, IEICE technical report COM88-30 (July 1988) 47–55.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1989

Authors and Affiliations

  • Yoshihito Toyama
    • 1
  • Jan Willem Klop
    • 2
  • Hendrik Pieter Barendregt
    • 3
  1. 1.NTT Basic Research LaboratoriesTokyoJapan
  2. 2.Centre for Mathematics and Computer ScienceAmsterdamThe Netherlands
  3. 3.Informatica, Nijmegen UniversityNijmegenThe Netherlands

Personalised recommendations