LIPIcs.FSCD.2018.6.pdf
- Filesize: 453 kB
- 15 pages
Document
Confluence of Prefix-Constrained Rewrite Systems
Authors
-
Part of:
Volume:
3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Formal Structures for Computation and Deduction (FSCD) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2018-07-04
Cite As Get BibTex
Nirina Andrianarivelo and Pierre Réty. Confluence of Prefix-Constrained Rewrite Systems. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.FSCD.2018.6
Abstract
Prefix-constrained rewriting is a strict extension of context-sensitive rewriting. We study the confluence of prefix-constrained rewrite systems, which are composed of rules of the form L: l -> r where L is a regular string language that defines the allowed rewritable positions. The usual notion of Knuth-Bendix's critical pair needs to be extended using regular string languages, and the convergence of all critical pairs is not enough to ensure local confluence. Thanks to an additional restriction we get local confluence, and then confluence for terminating systems, which makes the word problem decidable. Moreover we present an extended Knuth-Bendix completion procedure, to transform a non-confluent prefix-constrained rewrite system into a confluent one.
Subject Classification
ACM Subject Classification
- Theory of computation → Rewrite systems
Keywords
- prefix-constrained term rewriting
- confluence
- critical pair
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Nirina Andrianarivelo, Vivien Pelletier, and Pierre Réty. Transforming prefix-constrained or controlled rewrite systems. In Mohamed Mosbah and Michaël Rusinowitch, editors, SCSS 2017, The 8th International Symposium on Symbolic Computation in Software Science 2017, April 6-9, 2017, Gammarth, Tunisia, volume 45 of EPiC Series in Computing, pages 49-62. EasyChair, 2017. URL: http://www.easychair.org/publications/paper/Transforming_Prefix-constrained_or_Controlled_Rewrite_Systems.
- Leo Bachmair and Nachum Dershowitz. Completion for rewriting modulo a congruence. In Pierre Lescanne, editor, Rewriting Techniques and Applications, 2nd International Conference, RTA-87, Bordeaux, France, May 25-27, 1987, Proceedings, volume 256 of Lecture Notes in Computer Science, pages 192-203. Springer, 1987. URL: http://dx.doi.org/10.1007/3-540-17220-3_17.
- Alonzo Church and J. B. Rosser. Some properties of conversion. Transactions of the American Mathematical Society, 39(3):472-482, 1936. URL: http://www.jstor.org/stable/1989762.
- Kokichi Futatsugi, Joseph A. Goguen, Jean-Pierre Jouannaud, and José Meseguer. Principles of OBJ2. In Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, New Orleans, Louisiana, USA, January 1985, pages 52-66, 1985. URL: http://dx.doi.org/10.1145/318593.318610.
- Jürgen Giesl and Aart Middeldorp. Transformation Techniques for Context-Sensitive Rewrite Systems. J. Funct. Program., 14(4):379-427, 2004. URL: http://dx.doi.org/10.1017/S0956796803004945.
- Gérard P. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems: Abstract properties and applications to term rewriting systems. J. ACM, 27(4):797-821, 1980. URL: http://dx.doi.org/10.1145/322217.322230.
- Florent Jacquemard, Yoshiharu Kojima, and Masahiko Sakai. Controlled Term Rewriting. In Cesare Tinelli and Viorica Sofronie-Stokkermans, editors, Frontiers of Combining Systems, 8th International Symposium, FroCoS 2011, Saarbrücken, Germany, October 5-7, 2011. Proceedings, volume 6989 of Lecture Notes in Computer Science, pages 179-194. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-24364-6_13.
- Florent Jacquemard, Yoshiharu Kojima, and Masahiko Sakai. Term Rewriting with Prefix Context Constraints and Bottom-Up Strategies. In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, volume 9195 of LNCS, pages 137-151. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-319-21401-6_9.
-
D. E. Knuth and P. B. Bendix. Simple word problems in universal algebras. In J. Siekmann and G. Wrightson, editors, Automation of Reasoning 2: Classical Papers on Computational Logic 1967-1970, pages 342-376. Springer, Berlin, Heidelberg, 1983.
-
S. Lucas. Context-Sensitive Computations in Functional and Functional logic Programs. Journal of Functional and Logic Programming, 1998(1), January 1998.
- Salvador Lucas. Context-sensitive computations in confluent programs. In Herbert Kuchen and S. Doaitse Swierstra, editors, Programming Languages: Implementations, Logics, and Programs, 8th International Symposium, PLILP'96, Aachen, Germany, September 24-27, 1996, Proceedings, volume 1140 of Lecture Notes in Computer Science, pages 408-422. Springer, 1996. URL: http://dx.doi.org/10.1007/3-540-61756-6_100.