ABSTRACT
We focus on (partial) functions that map input strings to a monoid such as the set of integers with addition and the set of output strings with concatenation. The notion of regularity for such functions has been defined using two-way finite-state transducers, (one-way) cost register automata, and MSO-definable graph transformations. In this paper, we give an algebraic and machine-independent characterization of this class analogous to the definition of regular languages by regular expressions. When the monoid is commutative, we prove that every regular function can be constructed from constant functions using the combinators of choice, split sum, and iterated sum, that are analogs of union, concatenation, and Kleene-*, respectively, but enforce unique (or unambiguous) parsing. Our main result is for the general case of non-commutative monoids, which is of particular interest for capturing regular string-to-string transformations for document processing. We prove that the following additional combinators suffice for constructing all regular functions: (1) the left-additive versions of split sum and iterated sum, which allow transformations such as string reversal; (2) sum of functions, which allows transformations such as copying of strings; and (3) function composition, or alternatively, a new concept of chained sum, which allows output values from adjacent blocks to mix.
- A. V. Aho, J. E. Hopcroft, and J. D. Ullman. A general theory of translation. Mathematical Systems Theory, 3(3):193--221, 1969.Google ScholarCross Ref
- R. Alur and P. Černý. Expressiveness of streaming string transducers. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, LIPIcs 8, pages 1--12, 2010.Google Scholar
- R. Alur and P. Černý. Streaming transducers for algorithmic verification of single-pass list-processing programs. In Proceedings of 38th ACM Symposium on Principles of Programming Languages, pages 599--610, 2011. Google ScholarDigital Library
- R. Alur and L. D'Antoni. Streaming tree transducers. In Automata, Languages, and Programming --- 39th International Colloquium, ICALP Part II, pages 42--53. 2012. Google ScholarDigital Library
- R. Alur, L. D'Antoni, J. V. Deshmukh, M. Raghothaman, and Y. Yuan. Regular functions and cost register automata. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 13--22, 2013. Google ScholarDigital Library
- R. Alur, E. Filiot, and A. Trivedi. Regular transformations of infinite strings. In 27th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 65--74, 2012. Google ScholarDigital Library
- M. Bojanczyk. Transducers with origin information. In Automata, Languages, and Programming --- 41st International Colloquium, ICALP Part II, 2014. Forthcoming.Google Scholar
- K. Chatterjee, L. Doyen, and T. A. Henzinger. Quantitative languages. ACM Trans. Comput. Log., 11(4), 2010. Google ScholarDigital Library
- M. Chytil and V. Jákl. Serial composition of 2-way finite-state transducers and simple programs on strings. In Automata, Languages and Programming --- 4th International Colloquium, LNCS 52, pages 135--147. 1977. Google ScholarDigital Library
- T. Colcombet. The theory of stabilisation monoids and regular cost functions. In Automata, Languages, and Programming --- 36th International Colloquium, ICALP Part II, pages 139--150. 2009. Google ScholarDigital Library
- B. Courcelle. Monadic second-order graph transductions. In 17th Colloquium on Trees in Algebra and Programming, LNCS 581, pages 124--144. 1992. Google ScholarDigital Library
- M. Droste, W. Kuich, and H. Vogler. Handbook of Weighted Automata. Springer, 2009. Google ScholarDigital Library
- J. Engelfriet and H. J Hoogeboom. MSO definable string transductions and two-way finite-state transducers. ACM Transactions on Computational Logic, 2(2):216--254, 2001. Google ScholarDigital Library
- J. Engelfriet and S. Maneth. Macro tree transducers, attribute grammars, and MSO definable tree translations. Information and Computation, 154:34--91, 1999. Google ScholarDigital Library
- S. Gulwani. Automating string processing in spreadsheets using input-output examples. In Proceedings of 38th ACM Symposium on Principles of Programming Languages, pages 317--330, 2011. Google ScholarDigital Library
- E. M. Gurari. The equivalence problem for deterministic two-way sequential transducers is decidable. In 21st Annual Symposium on Foundations of Computer Science, pages 83--85, 1980. Google ScholarDigital Library
- Michael Sipser. Introduction to the Theory of Computation. Cengage Learning, 3rd edition, 2012.Google Scholar
- M. Veanes, P. Hooimeijer, B. Livshits, D. Molnar, and N. Bjørner. Symbolic finite state transducers: Algorithms and applications. In Proceedings of 39th ACM Symposium on Principles of Programming Languages, pages 137--150, 2012. Google ScholarDigital Library
Index Terms
- Regular combinators for string transformations
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, ...
MSO definable string transductions and two-way finite-state transducers
We extend a classic result of Büchi, Elgot, and Trakhtenbrot: MSO definable string transductions i.e., string-to-string functions that are definable by an interpretation using monadic second-order (MSO) logic, are exactly those realized by deterministic ...
Regular Transformations of Infinite Strings
LICS '12: Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer ScienceThe theory of regular transformations of finite strings is quite mature with appealing properties. This class can be equivalently defined using both logic (Monadic second-order logic) and finite-state machines (two-way transducers, and more recently, ...
Comments