Confluence of layered rewrite systems
From MaRDI portal
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, and the so-alled subrewriting relation, we show that rank non-increasing layered systems are confluent provided their cyclic critical pairs have cyclic-joinable decreasing diagrams.
Recommendations
Cited in
(9)- Unification of drags and confluence of drag rewriting
- Pushing the frontiers of combining rewrite systems farther outwards
- Layer systems for proving confluence
- Layer systems for proving confluence
- scientific article; zbMATH DE number 6744203 (Why is no real title available?)
- scientific article; zbMATH DE number 5172485 (Why is no real title available?)
- Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs
- Sort-based confluence criteria for non-left-linear higher-order rewriting
- Confluence of almost parallel-closed generalized term rewriting systems
This page was built for publication: Confluence of layered rewrite systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5351972)
