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 metadatas

Cited literature [26 references]  Display  Hide  Download

https://hal.inria.fr/hal-01199062
Contributor : Jean-Pierre Jouannaud <>
Submitted on : Tuesday, December 1, 2015 - 11:43:58 PM
Last modification on : Wednesday, March 27, 2019 - 4:41:27 PM
Long-term archiving on : Saturday, April 29, 2017 - 12:38:51 AM

File

CSL-finalversion-150719.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

405

Files downloads

126