Confluent term rewriting systems with membership conditions

Yoshihito Toyama

Research output: Chapter in Book/Report/Conference proceedingConference contribution

22 Citations (Scopus)


We propose a new type of conditional term rewriting system: the membership-conditional term rewriting system, in which, each rewriting rule can have membership conditions which restrict the substitution values for the variables occurring in the rule. For example, the rule f(x, x, y) ▹ g(x, y) if x ∈ T' yields the reduction f(M, M, N) → g(M, N) only when M is in the term set T'. Thus, by using membership-conditional rewriting, we can easily provide a strategy for term reduction. We study the confluence of membership-conditional term rewriting systems that are nonterminating and nonlinear. It is shown that a restricted nonlinear term rewriting system in which membership conditions satisfy the closure and termination properties is confluent if the system is nonoverlapping.

Original languageEnglish
Title of host publicationConditional Term Rewriting Systems - 1st International Workshop, Proceedings
EditorsStephane Kaplan, Jean-Pierre Jouannaud
PublisherSpringer Verlag
Number of pages14
ISBN (Print)9783540192428
Publication statusPublished - 1988
Event1st International Workshop on Conditional Term Rewriting Systems, 1987 - Orsay, France
Duration: 1987 Jul 81987 Jul 10

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume308 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other1st International Workshop on Conditional Term Rewriting Systems, 1987

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Confluent term rewriting systems with membership conditions'. Together they form a unique fingerprint.

Cite this