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 language | English |
---|---|
Pages (from-to) | 148-162 |
Number of pages | 15 |
Journal | Computer Software |
Volume | 30 |
Issue number | 3 |
Publication status | Published - 2013 Aug 1 |
ASJC Scopus subject areas
- Software