Mikołaj Bojańczyk
ABSTRACT
We define two classes of functions, called regular (respectively, first-order) list functions, which manipulate objects such as lists, lists of lists, pairs of lists, lists of pairs of lists, etc. The definition is in the style of regular expressions: the functions are constructed by starting with some basic functions (e.g. projections from pairs, or head and tail operations on lists) and putting them together using four combinators (most importantly, composition of functions). Our main results are that first-order list functions are exactly the same as first-order transductions, under a suitable encoding of the inputs; and the regular list functions are exactly the same as MSO-transductions.
- Alfred V Aho and Jeffrey D Ullman. 1970. A Characterization of Two-Way Deterministic Classes of Languages. J. Comput. Syst. Sci. 4, 6 (1970), 523--538. Google Scholar
Digital Library
- Rajeev Alur and Pavol Černý. 2011. Streaming transducers for algorithmic verification of single-pass list-processing programs. In Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages -POPL '11. ACM Press, New York, New York, USA, 599. Google ScholarDigital Library
- Rajeev Alur and Loris D'Antoni. 2017. Streaming Tree Transducers. J. ACM 64, 5 (2017), 1--55. Google ScholarDigital Library
- Rajeev Alur, Adam Freilich, and Mukund Raghothaman. 2014. Regular combinators for string transformations. CSL-LICS (2014), 1--10. Google ScholarDigital Library
- Alur, Rajeev and Cerný, Pavol. 2010. Expressiveness of streaming string transducers. FSTTCS (2010).Google Scholar
- Richard S. Bird. 1987. An Introduction to the Theory of Lists. In Logic of Programming and Calculi of Discrete Design, M. Broy (Ed.). Springer-Verlag, 3--42. NATO ASI Series F Volume 36. Also available as Technical Monograph PRG-56, from the Programming Research Group, Oxford University. Google ScholarDigital Library
- M. Bojańczyk. 2009. Factorization forests. Vol. 5583 LNCS.Google Scholar
- Mikołaj Bojańczyk, Laure Daviaud, and Krishna Shankara Narayanan. 2018. Regular and First Order List Functions. CoRR abs/1803.06168 (2018). arXiv:1803.06168 http://arxiv.org/abs/1803.06168Google Scholar
- Olivier Carton and Luc Dartois. 2015. Aperiodic Two-way Transducers and FO-Transductions. In 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany (LIPIcs), Stephan Kreutzer (Ed.), Vol. 41. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 160--174.Google Scholar
- Thomas Colcombet. 2007. A Combinatorial Theorem for Trees. In Automata, Languages and Programming. Springer, Berlin, Heidelberg, Berlin, Heidelberg, 901--912. Google ScholarDigital Library
- Bruno Courcelle and Joost Engelfriet. 2012. Graph Structure and Monadic Second-Order Logic - A Language-Theoretic Approach. Encyclopedia of mathematics and its applications, Vol. 138. CUP. I-XIV, 1--728 pages. Google ScholarDigital Library
- Luc Dartois, Ismaël Jecker, and Pierre-Alain Reynier. 2016. Aperiodic String Transducers. In Developments in Language Theory - 20th International Conference, DLT 2016, Montréal, Canada, July 25-28, 2016, Proceedings (Lecture Notes in Computer Science), Srecko Brlek and Christophe Reutenauer (Eds.), Vol. 9840. Springer, 125--137. Google ScholarDigital Library
- C C Elgot and J E Mezei. 1965. On Relations Defined by Generalized Finite Automata. IBM Journal of Research and Development 9, 1 (1965), 47--68. Google ScholarDigital Library
- Joost Engelfriet and Hendrik Jan Hoogeboom. 2001. MSO definable string transductions and two-way finite-state transducers. ACM Transactions on Computational Logic 2, 2 (April 2001), 216--254. Google ScholarDigital Library
- Emmanuel Filiot, Shankara Narayanan Krishna, and Ashutosh Trivedi. 2014. First-order Definable String Transformations. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014, December 15-17, 2014, New Delhi, India (LIPIcs), Venkatesh Raman and S. P. Suresh (Eds.), Vol. 29. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 147--159.Google Scholar
- Emmanuel Filiot and Pierre-Alain Reynier. 2016. Transducers, logic and algebra for functions of finite words. SIGLOG News (2016). Google ScholarDigital Library
- Eitan M. Gurari. 1982. The Equivalence Problem for Deterministic Two-Way Sequential Transducers is Decidable. SIAM J. Comput. 11, 3 (1982), 448--452. arXiv:https://doi.org/10.1137/0211035Google ScholarDigital Library
- Wiflrid Hodges. 1993. Model Theory. Cambridge University Press. https://books.google.pl/books?id=Rf6GWut4D30CGoogle Scholar
- John Rhodes and Pedro V Silva. 2008. Turing machines and bimachines. Theor. Comput. Sci. 400, 1-3 (2008), 182--224. Google ScholarDigital Library
- Jacques Sakarovitch. 2009. Elements of Automata Theory. Cambridge University Press. http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=9780521844253 Google ScholarDigital Library
- Jacques Sakarovitch and Reuben Thomas. 2009. Elements of Automata Theory. Cambridge University Press, Cambridge. Google ScholarDigital Library
- Claude E Shannon. 1948. A mathematical theory of communication, Part I, Part II. Bell Syst. Tech. J. 27 (1948), 623--656.Google ScholarCross Ref
- Imre Simon. 1990. Factorization Forests of Finite Height. Theor. Comput. Sci. 72, 1 (1990), 65--94. Google ScholarDigital Library
- Howard Straubing. 2012. Finite Automata, Formal Logic, and Circuit Complexity. Springer Science & Business Media.Google Scholar
- Wolfgang Thomas. 1997. Languages, Automata, and Logic. In Handbook of Formal Languages. 389--455. arXiv:arXiv:1011.1669v3Google Scholar
Recommendations
Regular Transducer Expressions for Regular Transformations
LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer ScienceFunctional MSO transductions, deterministic two-way transducers, as well as streaming string transducers are all equivalent models for regular functions. In this paper, we show that every regular function, either on finite words or on infinite words, ...
Deciding Regular Grammar Logics with Converse Through First-Order Logic
We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF 2 , which is the intersection of the guarded fragment and the 2-variable fragment of first-order logic. The translation is theoretically ...
Logic and regular cost functions
LICS '17: Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer ScienceRegular cost functions offer a toolbox for automatically solving problems of existence of bounds, in a way similar to the theory of regular languages. More precisely, it allows to test the existence of bounds for quantities that can be defined in cost ...
Comments