Aperiodicity, star-freeness, and first-order logic definability of operator precedence languages. (English) Zbl 07788984
Summary: A classic result in formal language theory is the equivalence among non-counting, or aperiodic, regular languages, and languages defined through star-free regular expressions, or first-order logic. Past attempts to extend this result beyond the realm of regular languages have met with difficulties: for instance it is known that star-free tree languages may violate the non-counting property and there are aperiodic tree languages that cannot be defined through first-order logic.
We extend such classic equivalence results to a significant family of deterministic context-free languages, the operator-precedence languages (OPL), which strictly includes the widely investigated visibly pushdown, alias input-driven, family and other structured context-free languages. The OP model originated in the ’60s for defining programming languages and is still used by high performance compilers; its rich algebraic properties have been investigated initially in connection with grammar learning and recently completed with further closure properties and with monadic second order logic definition.
We introduce an extension of regular expressions, the OP-expressions (OPE) which define the OPLs and, under the star-free hypothesis, define first-order definable and non-counting OPLs. Then, we prove, through a fairly articulated grammar transformation, that aperiodic OPLs are first-order definable. Thus, the classic equivalence of star-freeness, aperiodicity, and first-order definability is established for the large and powerful class of OPLs.
We argue that the same approach can be exploited to obtain analogous results for visibly pushdown languages, too.
We extend such classic equivalence results to a significant family of deterministic context-free languages, the operator-precedence languages (OPL), which strictly includes the widely investigated visibly pushdown, alias input-driven, family and other structured context-free languages. The OP model originated in the ’60s for defining programming languages and is still used by high performance compilers; its rich algebraic properties have been investigated initially in connection with grammar learning and recently completed with further closure properties and with monadic second order logic definition.
We introduce an extension of regular expressions, the OP-expressions (OPE) which define the OPLs and, under the star-free hypothesis, define first-order definable and non-counting OPLs. Then, we prove, through a fairly articulated grammar transformation, that aperiodic OPLs are first-order definable. Thus, the classic equivalence of star-freeness, aperiodicity, and first-order definability is established for the large and powerful class of OPLs.
We argue that the same approach can be exploited to obtain analogous results for visibly pushdown languages, too.
Keywords:
operator precedence languages; aperiodicity; first-order logic; star-free expressions; visibly pushdown languages; input-driven languages; structured languagesReferences:
| [1] | AAB + 08] Rajeev Alur, Marcelo Arenas, Pablo Barcelo, Kousha Etessami, Neil Immerman, and Leonid Libkin. First-order and temporal logics for nested words. Logical Methods in Computer Science, 4(4), 2008. · Zbl 1159.03018 |
| [2] | Jean-Michel Autebert, Jean Berstel, and Luc Boasson. Context-free languages and push-down automata. In Handbook of Formal Languages (1), pages 111-174. 1997. doi:10.1007/ 978-3-642-59136-5_3. · doi:10.1007/978-3-642-59136-5_3 |
| [3] | Rajeev Alur, Swarat Chaudhuri, and Parthasarathy Madhusudan. Software model checking using languages of nested trees. ACM Trans. Program. Lang. Syst., 33(5):15:1-15:45, 2011. doi:10.1145/2039346.2039347. · doi:10.1145/2039346.2039347 |
| [4] | Rajeev Alur and Dana Fisman. Colored nested words. In Adrian-Horia Dediu, Jan Janousek, Carlos Martín-Vide, and Bianca Truthe, editors, Language and Automata Theory and Applications -10th International Conference, LATA 2016, Prague, Czech Republic, March 14-18, 2016, Proceedings, volume 9618 of Lecture Notes in Computer Science, pages 143-155. Springer, 2016. doi:10.1007/978-3-319-30000-9_11. · Zbl 1443.68079 · doi:10.1007/978-3-319-30000-9_11 |
| [5] | Rajeev Alur and Parthasarathy Madhusudan. Adding nesting structure to words. J. ACM, 56(3), 2009. · Zbl 1325.68138 |
| [6] | + 15] Alessandro Barenghi, Stefano Crespi Reghizzi, Dino Mandrioli, Federica Panella, and Matteo Pradella. Parallel parsing made practical. Sci. Comput. Program., 112(3):195-226, 2015. doi: 10.1016/j.scico.2015.09.002. · doi:10.1016/j.scico.2015.09.002 |
| [7] | Laura Bozzelli and César Sánchez. Visibly linear temporal logic. In Stéphane Demri, Deepak Kapur, and Christoph Weidenbach, editors, Automated Reasoning -7th International Joint Conference, IJCAR, volume 8562 of Lecture Notes in Computer Science, pages 418-433. Springer, 2014. doi:10.1007/978-3-319-08587-6_33. · Zbl 1423.68274 · doi:10.1007/978-3-319-08587-6_33 |
| [8] | Mikolaj Bojanczyk, Luc Segoufin, and Howard Straubing. Piecewise testable tree languages. Log. Methods Comput. Sci., 8(3), 2012. doi:10.2168/LMCS-8(3:26)2012. · Zbl 1261.03126 · doi:10.2168/LMCS-8(3:26)2012 |
| [9] | Julius R. Büchi. Weak Second-Order Arithmetic and Finite Automata. Mathematical Logic Quarterly, 6(1-6):66-92, 1960. · Zbl 0103.24705 |
| [10] | Didier Caucal. Synchronization of Pushdown Automata. In O. H. Ibarra and Z. Dang, editors, Developments in Language Theory, volume 4036 of LNCS, pages 120-132. Springer, 2006. · Zbl 1227.68049 |
| [11] | Fabrice Chevalier, Deepak D’Souza, and Pavithra Prabhakar. Counter-free input-determined timed automata. In Formal Modeling and Analysis of Timed Systems, 5th International Confer-ence, FORMATS 2007, Salzburg, Austria, October 3-5, 2007, Proceedings, pages 82-97, 2007. doi:10.1007/978-3-540-75454-1_8. · Zbl 1142.68039 · doi:10.1007/978-3-540-75454-1_8 |
| [12] | Stefano Crespi Reghizzi, Giovanni Guida, and Dino Mandrioli. Noncounting Context-Free Languages. J. ACM, 25:571-580, 1978. · Zbl 0388.68073 |
| [13] | Stefano Crespi Reghizzi, Giovanni Guida, and Dino Mandrioli. Operator Precedence Grammars and the Noncounting Property. SIAM J. Comput., 10:174-191, 1981. · Zbl 0454.68090 |
| [14] | Noam Chomsky. Reflections on Language. New York: Pantheon Books, 1975. |
| [15] | Stefano Crespi Reghizzi and Dino Mandrioli. A class of grammars generating non-counting languages. Inf. Process. Lett., 7(1):24-26, 1978. doi:10.1016/0020-0190(78)90033-9. · doi:10.1016/0020-0190(78)90033-9 |
| [16] | Stefano Crespi Reghizzi and Dino Mandrioli. Operator Precedence and the Visibly Pushdown Property. J. Comput. Syst. Sci., 78(6):1837-1867, 2012. · Zbl 1250.68175 |
| [17] | Stefano Crespi Reghizzi, Michel A. Melkanoff, and Larry Lichten. The use of grammatical inference for designing programming languages. Commun. ACM, 16(2):83-90, 1973. doi:10. 1145/361952.361958. · Zbl 0248.68037 · doi:10.1145/361952.361958 |
| [18] | Stefano Crespi Reghizzi, Dino Mandrioli, and Daniel F. Martin. Algebraic Properties of Operator Precedence Languages. Information and Control, 37(2):115-133, May 1978. · Zbl 0377.68048 |
| [19] | Michele Chiari, Dino Mandrioli, and Matteo Pradella. Operator precedence temporal logic and model checking. Theoretical Computer Science, 2020. doi:10.1016/j.tcs.2020.08.034. · Zbl 1464.68197 · doi:10.1016/j.tcs.2020.08.034 |
| [20] | Michele Chiari, Dino Mandrioli, and Matteo Pradella. Model-checking structured context-free languages. In A. Silva and K. R. M. Leino, editors, CAV ’21, volume 12760 of LNCS, pages 387-410. Springer, 2021. doi:10.1007/978-3-030-81688-9_18. · Zbl 1493.68207 · doi:10.1007/978-3-030-81688-9_18 |
| [21] | Michele Chiari, Dino Mandrioli, and Matteo Pradella. A first-order complete temporal logic for structured context-free languages. Logical Methods in Computer Science, 18(3), 2022. doi: 10.46298/lmcs-18(3:11)2022. · Zbl 07577575 · doi:10.46298/lmcs-18(3:11)2022 |
| [22] | Stefano Crespi Reghizzi and Matteo Pradella. Beyond operator-precedence grammars and languages. Journal of Computer and System Sciences, 113:18-41, 2020. doi:10.1016/j.jcss. 2020.04.006. · Zbl 1444.68092 · doi:10.1016/j.jcss.2020.04.006 |
| [23] | Volker Diekert and Paul Gastin. First-order definable languages. In Logic and Automata: History and Perspectives, Texts in Logic and Games, pages 261-306. Amsterdam University Press, 2008. · Zbl 1234.03024 |
| [24] | ZoltánÉsik and Szabolcs Iván. Aperiodicity in tree automata. In Algebraic Informatics, 2nd International Conference, CAI, pages 189-207, 2007. doi:10.1007/978-3-540-75414-5_12. · Zbl 1148.68399 · doi:10.1007/978-3-540-75414-5_12 |
| [25] | Calvin C. Elgot. Decision problems of finite automata design and related arithmetics. Trans. Am. Math. Soc., 98(1):21-52, 1961. · Zbl 0111.01102 |
| [26] | Robert W. Floyd. Syntactic Analysis and Operator Precedence. J. ACM, 10(3):316-333, 1963. · Zbl 0133.25504 |
| [27] | Dick Grune and Ceriel J. Jacobs. Parsing techniques: a practical guide. Springer, New York, 2008. 12:54 · Zbl 1138.68022 |
| [28] | D. Mandrioli, M. Pradella, and S. Crespi Reghizzi Vol. 19:4 |
| [29] | Michael A. Harrison. Introduction to Formal Language Theory. Addison Wesley, 1978. · Zbl 0411.68058 |
| [30] | Uschi Heuter. First-order properties of trees, star-free expressions, and aperiodicity. ITA, 25:125-145, 1991. doi:10.1051/ita/1991250201251. · Zbl 0741.68065 · doi:10.1051/ita/1991250201251 |
| [31] | Thomas A. Henzinger, Pavol Kebis, Nicolas Mazzocchi, and N. Ege Saraç. Regular methods for operator precedence languages. In Kousha Etessami, Uriel Feige, and Gabriele Puppis, editors, 50th International Colloquium on Automata, Languages, and Programming, ICALP 2023, July 10-14, 2023, Paderborn, Germany, volume 261 of LIPIcs, pages 129:1-129:20. Schloss Dagstuhl -Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPIcs.ICALP.2023.129. · doi:10.4230/LIPIcs.ICALP.2023.129 |
| [32] | Tore Langholm. A descriptive characterisation of linear languages. Journal of Logic, Language and Information, 15(3):233-250, 2006. doi:10.1007/s10849-006-9016-z. · Zbl 1105.68064 · doi:10.1007/s10849-006-9016-z |
| [33] | Violetta Lonati, Dino Mandrioli, Federica Panella, and Matteo Pradella. First-order logic definability of free languages. In Lev D. Beklemishev and Daniil V. Musatov, editors, Computer Science -Theory and Applications -10th International Computer Science Symposium in Russia, CSR 2015, Listvyanka, Russia, July 13-17, 2015, Proceedings, volume 9139 of Lecture Notes in Computer Science, pages 310-324. Springer, 2015. · Zbl 1465.68122 |
| [34] | Violetta Lonati, Dino Mandrioli, Federica Panella, and Matteo Pradella. Operator precedence languages: Their automata-theoretic and logic characterization. SIAM J. Comput., 44(4):1026-1088, 2015. doi:10.1137/140978818. · Zbl 1522.68278 · doi:10.1137/140978818 |
| [35] | Clemens Lautemann, Thomas Schwentick, and Denis Thérien. Logics for context-free languages. In Leszek Pacholski and Jerzy Tiuryn, editors, Computer Science Logic, 8th International Workshop, CSL ’94, Kazimierz, Poland, September 25-30, 1994, Selected Papers, volume 933 of Lecture Notes in Computer Science, pages 205-216. Springer, 1994. · Zbl 1044.68631 |
| [36] | Maarten Marx. Conditional XPath. ACM Transactions on Database Systems, 30(4):929-959, dec 2005. doi:10.1145/1114244.1114247. · doi:10.1145/1114244.1114247 |
| [37] | Robert McNaughton. Parenthesis Grammars. J. ACM, 14(3):490-500, 1967. · Zbl 0168.01206 |
| [38] | Robert McNaughton and Seymour Papert. Counter-free Automata. MIT Press, Cambridge, USA, 1971. · Zbl 0232.94024 |
| [39] | Dino Mandrioli and Matteo Pradella. Generalizing input-driven languages: Theoretical and practical benefits. Computer Science Review, 27:61-87, 2018. doi:10.1016/j.cosrev.2017.12. 001. · Zbl 1382.68136 · doi:10.1016/j.cosrev.2017.12.001 |
| [40] | Dino Mandrioli, Matteo Pradella, and Stefano Crespi Reghizzi. Star-freeness, first-order defin-ability and aperiodicity of structured context-free languages. In Proceedings of ICTAC 2020, Lecture Notes in Computer Science. Springer, 2020. doi:10.1007/978-3-030-64276-1_9. · Zbl 07369988 · doi:10.1007/978-3-030-64276-1_9 |
| [41] | Dirk Nowotka and Jiri Srba. Height-Deterministic Pushdown Automata. In L. Kucera and A. Kucera, editors, MFCS 2007, Ceský Krumlov, Czech Republic, August 26-31, 2007, Proceedings, volume 4708 of LNCS, pages 125-134. Springer, 2007. · Zbl 1147.68562 |
| [42] | Jean-Eric Pin. Logic on words. In Current Trends in Theoretical Computer Science, pages 254-273. 2001. · Zbl 1049.68600 |
| [43] | Andreas Potthoff. Modulo-counting quantifiers over finite trees. Theor. Comput. Sci., 126(1):97-112, 1994. doi:10.1016/0304-3975(94)90270-4. · Zbl 0798.03007 · doi:10.1016/0304-3975(94)90270-4 |
| [44] | Andreas Potthoff. First-order logic on finite trees. In Peter D. Mosses, Mogens Nielsen, and Michael I. Schwartzbach, editors, TAPSOFT’95: Theory and Practice of Software Development, volume 915 of Lecture Notes in Computer Science, pages 125-139. Springer, 1995. doi:10.1007/ 3-540-59293-8_191. · Zbl 1496.68178 · doi:10.1007/3-540-59293-8_191 |
| [45] | Thomas Place and Luc Segoufin. A decidable characterization of locally testable tree languages. Log. Methods Comput. Sci., 7(4), 2011. doi:10.2168/LMCS-7(4:3)2011. · Zbl 1237.68119 · doi:10.2168/LMCS-7(4:3)2011 |
| [46] | Alexander Rabinovich. A proof of Kamp’s theorem. Logical Methods in Computer Science, 10(1), 2014. doi:10.2168/LMCS-10(1:14)2014. · Zbl 1326.03024 · doi:10.2168/LMCS-10(1:14)2014 |
| [47] | Arto K. Salomaa. Formal Languages. Academic Press, New York, NY, 1973. · Zbl 0262.68025 |
| [48] | Victor L. Selivanov. Fine hierarchy of regular aperiodic omega-languages. Int. J. Found. Comput. Sci., 19(3):649-675, 2008. doi:10.1142/S0129054108005875. · Zbl 1155.03022 · doi:10.1142/S0129054108005875 |
| [49] | James W. Thatcher. Characterizing derivation trees of context-free grammars through a general-ization of finite automata theory. Journ. of Comp. and Syst.Sc., 1:317-322, 1967. · Zbl 0155.01802 |
| [50] | Wolfgang Thomas. Logical aspects in the study of tree languages. In Bruno Courcelle, editor, CAAP’84, 9th Colloquium on Trees in Algebra and Programming, Bordeaux, France, March 5-7, 1984, Proceedings, pages 31-50. Cambridge University Press, 1984. · Zbl 0557.68051 |
| [51] | Wolfgang Thomas. Automata on infinite objects. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pages 133-191. Elsevier and MIT Press, 1990. doi:10.1016/b978-0-444-88074-1.50009-3. · Zbl 0900.68316 · doi:10.1016/b978-0-444-88074-1.50009-3 |
| [52] | Boris A. Trakhtenbrot. Finite automata and logic of monadic predicates (in Russian). Doklady Akademii Nauk SSR, 140:326-329, 1961. |
| [53] | Burchard von Braunmühl and Rutger Verbeek. Input-driven languages are recognized in log n space. In Proceedings of the Symposium on Fundamentals of Computation Theory, Lect. Notes Comput. Sci. 158, pages 40-51. Springer, 1983. · Zbl 0549.68082 |
| [54] | Klaus W. Wagner. On omega-regular sets. Inf. Control., 43(2):123-177, 1979. doi:10.1016/ S0019-9958(79)90653-3. · Zbl 0434.68061 · doi:10.1016/S0019-9958(79)90653-3 |
| [55] | Thomas Wilke. Classifying discrete temporal properties. In Christoph Meinel and Sophie Tison, editors, STACS 99, 16th Annual Symposium on Theoretical Aspects of Computer Science, Trier, Germany, March 4-6, 1999, Proceedings, volume 1563 of Lecture Notes in Computer Science, pages 32-46. Springer, 1999. doi:10.1007/3-540-49116-3_3. · Zbl 0926.03018 · doi:10.1007/3-540-49116-3_3 |
| [56] | Mary K. Yntema. Cap expressions for context-free languages. Information and Control, 18:311-318, 1971. This work is licensed under the Creative Commons Attribution License. To view a copy of this license, visit https://creativecommons.org/licenses/by/4.0/ or send a letter to Creative Commons, 171 Second St, Suite 300, San Francisco, CA 94105, USA, or Eisenacher Strasse 2, 10777 Berlin, Germany |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
