Skip to Main content Skip to Navigation
Conference papers

Confluence of layered rewrite systems

Abstract : We investigate the new, Turing-complete class of layered systems, whose lefthand sides of rules can only be overlapped at a multiset of disjoint or equal positions. Layered systems define a natural notion of rank for terms: the maximal number of non-overlapping redexes along a path from the root to a leaf. Overlappings are allowed in finite or infinite trees. Rules may be non-terminating, non-left-linear, or non-right-linear. Using a novel unification technique, cyclic unification, we show that rank non-increasing layered systems are confluent provided their cyclic critical pairs have cyclic-joinable decreasing diagrams.
Document type :
Conference papers
Complete list of metadata

Cited literature [26 references]  Display  Hide  Download
Contributor : Jean-Pierre Jouannaud Connect in order to contact the contributor
Submitted on : Tuesday, December 1, 2015 - 11:43:58 PM
Last modification on : Tuesday, July 5, 2022 - 8:39:05 AM
Long-term archiving on: : Saturday, April 29, 2017 - 12:38:51 AM


Files produced by the author(s)




Jiaxiang Liu, Jean-Pierre Jouannaud, Mizuhito Ogawa. Confluence of layered rewrite systems. 24th EACSL Annual Conference on Computer Science Logic (CSL 2015), Sep 2015, Berlin, Germany. pp.423--440, ⟨10.4230/LIPIcs.CSL.2015.423⟩. ⟨hal-01199062v2⟩



Record views


Files downloads