Confluence proofs of term rewriting systems based on persistency

Tsubasa Suzuki, Takahito Aoto, Yoshihito Toyama

Research output: Contribution to journalArticlepeer-review

2 Citations (Scopus)

Abstract

Since the confluence property of term rewrite systems is persistent, a term rewriting system R is confluent if it is decomposed into small subsystems by introducing appropriate many-sorted types and each of them is confluent. However, if introducing types does not decompose R into small subsystems, this proof method does not work. In this paper we propose a new method for confluence proof based on persistency, which can be applied to non-left-linear term rewriting systems not decomposed into subsystems by introducing types.

Original languageEnglish
Pages (from-to)148-162
Number of pages15
JournalComputer Software
Volume30
Issue number3
Publication statusPublished - 2013 Aug 1

ASJC Scopus subject areas

  • Software

Cite this