2026-07-23T05:17:48Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5429 2024-03-06T10:36:26Z ddc:004 open_access

Confluence of Layered Rewrite Systems Liu, Jiaxiang Jouannaud, Jean-Pierre Ogawa, Mizuhito Layers confluence decreasing diagrams critical pairs cyclic unification We investigate a new, Turing-complete class of layered systems, whose linearized lefthand sides of rules can only be overlapped at the root position. Layered systems define a natural notion of rank for terms: the maximal number of 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jiaxiang Liu and Jean-Pierre Jouannaud and Mizuhito Ogawa 2015 Is Part Of LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2015.423 urn:nbn:de:0030-drops-54293 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.423 eng https://creativecommons.org/licenses/by/3.0/legalcode