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.
Type de document :
Communication dans un congrès
24th EACSL Annual Conference on Computer Science Logic (CSL 2015), Sep 2015, Berlin, Germany. 41, pp.423--440, 〈http://logic.las.tu-berlin.de/csl2015/〉. 〈10.4230/LIPIcs.CSL.2015.423〉
Liste complète des métadonnées

Littérature citée [26 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01199062
Contributeur : Jean-Pierre Jouannaud <>
Soumis le : mardi 1 décembre 2015 - 23:43:58
Dernière modification le : jeudi 11 janvier 2018 - 06:19:44
Document(s) archivé(s) le : samedi 29 avril 2017 - 00:38:51

Fichier

CSL-finalversion-150719.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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. 41, pp.423--440, 〈http://logic.las.tu-berlin.de/csl2015/〉. 〈10.4230/LIPIcs.CSL.2015.423〉. 〈hal-01199062v2〉

Partager

Métriques

Consultations de la notice

128

Téléchargements de fichiers

66