First-order logic and numeration systems. (English) Zbl 1486.03055
Berthé, Valérie (ed.) et al., Sequences, groups, and number theory. Cham: Birkhäuser. Trends Math., 89-141 (2018).
Summary: The Büchi-Bruyère theorem states that a subset of \(\mathbb N^d\) is \(b\)-recognizable if and only if it is \(b\)-definable. This result is a powerful tool for showing that many properties of \(b\)-automatic sequences are decidable. Going a step further, first-order logic can be used to show that many enumeration problems of \(b\)-automatic sequences can be described by \(b\)-regular sequences. The latter sequences can be viewed as a generalization of \(b\)-automatic sequences to integer-valued sequences. These techniques were extended to two wider frameworks: \(U\)-recognizable subsets of \(\mathbb N^d\) and \(\beta\)-recognizable subsets of \(\mathbb R^d\). In the second case, real numbers are represented by infinite words, and hence, the notion of \(\beta\)-recognizability is defined by means of Büchi automata. Again, logic-based characterization of \(U\)-recognizable (resp. \(\beta\)-recognizable) sets allows us to obtain various decidability results. The aim of this chapter is to present a survey of this very active research domain.
For the entire collection see [Zbl 1394.05002].
For the entire collection see [Zbl 1394.05002].
MSC:
| 03C07 | Basic properties of first-order languages and structures |
| 03C62 | Models of arithmetic and set theory |
| 03D05 | Automata and formal grammars in connection with logical questions |
Software:
WalnutReferences:
| [1] | Adamczewski, B., Bell, J.P.: An analogue of Cobham’s theorem for fractals. Trans. Am. Math. Soc. 363(8), 4421-4442 (2011) · Zbl 1229.28007 · doi:10.1090/S0002-9947-2011-05357-2 |
| [2] | Allouche, J.-P., Rampersad, N., Shallit, J.: Periodicity, repetitions, and orbits of an automatic sequence. Theor. Comput. Sci. 410(30-32), 2795-2803 (2009) · Zbl 1173.68044 · doi:10.1016/j.tcs.2009.02.006 |
| [3] | Allouche, J.-P., Shallit, J.: Automatic Sequences: Theory, Applications, Generalizations. Cambridge University Press, Cambridge (2003) · Zbl 1086.11015 |
| [4] | Allouche, J.-P., Shallit, J.O.: The ring of k-regular sequences. Theor. Comput. Sci. 98, 163-197 (1992) · Zbl 0774.68072 · doi:10.1016/0304-3975(92)90001-V |
| [5] | Berend, D., Frougny, C.: Computability by finite automata and Pisot bases. Math. Syst. Theory 27, 275-282 (1994) · Zbl 0819.11005 · doi:10.1007/BF01578846 |
| [6] | Berstel, J., Reutenauer, C.: Noncommutative rational series with applications. Encyclopedia of Mathematics and Its Applications, vol. 137. Cambridge University Press, Cambridge (2011) · Zbl 1250.68007 |
| [7] | Berthé, V., Rigo, M. (eds.): Combinatorics, automata and number theory. Encyclopedia of Mathematics and Its Applications, vol. 135. Cambridge University Press, Cambridge (2010) · Zbl 1197.68006 |
| [8] | Boigelot, B., Brusten, J.: A generalization of Cobham’s theorem to automata over real numbers. Theor. Comput. Sci. 410(18), 1694-1703 (2009) · Zbl 1172.68029 · doi:10.1016/j.tcs.2008.12.051 |
| [9] | Boigelot, B., Brusten, J., Bruyère, V.: On the sets of real numbers recognized by finite automata in multiple bases. Log. Methods Comput. Sci. 6, 1-17 (2010) · Zbl 1189.03045 |
| [10] | Boigelot, B., Brusten, J., Leroux, J.: A generalization of Semenov’s theorem to automata over real numbers. In: Automated Deduction—CADE-22. Lecture Notes in Computer Science, vol. 5663, pp. 469-484. Springer, Berlin (2009) · Zbl 1250.03061 · doi:10.1007/978-3-642-02959-2_34 |
| [11] | Boigelot, B., Rassart, S., Wolper, P.: On the expressiveness of real and integer arithmetic automata (extended abstract). In: ICALP. Lecture Notes in Computer Science, vol. 1443, pp. 152-163. Springer, Berlin (1998) · Zbl 0910.68149 · doi:10.1007/BFb0055049 |
| [12] | Brusten, J.: On the sets of real vectors recognized by finite automata in multiple bases. PhD thesis, University of Liège (2011) |
| [13] | Bruyère, V.: Entiers et automates finis (1985). Mémoire de fin d’études, Université de Mons |
| [14] | Bruyère, V., Hansel, G.: Bertrand numeration systems and recognizability. Theor. Comput. Sci. 181, 17-43 (1997) · Zbl 0957.11015 · doi:10.1016/S0304-3975(96)00260-5 |
| [15] | Bruyère, V., Hansel, G., Michaux, C., Villemaire, R.: Logic and p-recognizable sets of integers. Bull. Belg. Math. Soc. 1, 191-238 (1994). Corrigendum, Bull. Belg. Math. Soc. 1 (1994), 577 · Zbl 0804.11024 |
| [16] | Büchi, J.R.: Weak second-order arithmetic and finite automata. Zeitschrift für mathematische Logik und Grundlagen der Mathematik 6, 66-92 (1960). Reprinted in Mac Lane, S., Siefkes, D. (eds.) The Collected Works of J. Richard Büchi. Springer, 1990, pp. 398-424 · Zbl 0142.24902 |
| [17] | Carpi, A., D’Alonzo, V.: On factors of synchronized sequences. Theor. Comput. Sci. 411(44-46), 3932-3937 (2010) · Zbl 1238.68114 · doi:10.1016/j.tcs.2010.08.005 |
| [18] | Carpi, A., Maggi, C.: On synchronized sequences and their separators. Theor. Inform. Appl. 35(6), 513-524 (2002) (2001) · Zbl 1003.68064 · doi:10.1051/ita:2001129 |
| [19] | Chan, D.H.Y., Hare, K.G.: A multi-dimensional analogue of Cobham’s theorem for fractals. Proc. Am. Math. Soc. 142(2), 449-456 (2014) · Zbl 1291.28008 · doi:10.1090/S0002-9939-2013-11843-5 |
| [20] | Charlier, É., Kärki, T., Rigo, M.: Multidimensional generalized automatic sequences and shape-symmetric morphic words. Discret. Math. 310(6-7), 1238-1252 (2010) · Zbl 1231.05010 · doi:10.1016/j.disc.2009.12.002 |
| [21] | Charlier, É., Lacroix, A., Rampersad, N.: Multi-dimensional sets recognizable in all abstract numeration systems. RAIRO Theor. Inform. Appl. 46(1), 51-65 (2012) · Zbl 1254.68132 · doi:10.1051/ita/2011112 |
| [22] | Charlier, É., Leroy, J., Rigo, M.: An analogue of Cobham’s theorem for graph directed iterated function systems. Adv. Math. 280, 86-120 (2015) · Zbl 1332.28013 · doi:10.1016/j.aim.2015.04.008 |
| [23] | Charlier, É., Rampersad, N.: The growth function of S-recognizable sets. Theor. Comput. Sci. 412(39), 5400-5408 (2011) · Zbl 1222.68100 |
| [24] | Charlier, É., Rampersad, N., Shallit, J.: Enumeration and decidable properties of automatic sequences. Int. J. Found. Comput. Sci. 23(5), 1035-1066 (2012) · Zbl 1282.68186 · doi:10.1142/S0129054112400448 |
| [25] | Charlier, É., Rigo, M., Steiner, W.: Abstract numeration systems on bounded languages and multiplication by a constant. Integers 8, A35, 19 (2008) · Zbl 1210.68066 |
| [26] | Cobham, A.: On the base-dependence of sets of numbers recognizable by finite automata. Math. Syst. Theory 3, 186-192 (1969) · Zbl 0179.02501 · doi:10.1007/BF01746527 |
| [27] | Durand, F., Rigo, M.: On Cobham’s theorem. In: Handbook of Automata. European Mathematical Society Publishing House (in press) · Zbl 07425662 |
| [28] | Edgar, G.: Measure, Topology, and Fractal Geometry, 2nd edn. Undergraduate Texts in Mathematics. Springer, New York (2008) · Zbl 1152.28008 |
| [29] | Eilenberg, S.: Automata, Languages, and Machines, vol. A. Academic Press, New York (1974) · Zbl 0317.94045 |
| [30] | Elekes, M., Keleti, T., Máthé, A.: Self-similar and self-affine sets: measure of the intersection of two copies. Ergodic Theory Dyn. Syst. 30(2), 399-440 (2010) · Zbl 1200.28005 · doi:10.1017/S0143385709000121 |
| [31] | Feng, D.J., Wang, Y.: On the structures of generating iterated function systems of Cantor sets. Adv. Math. 222(6), 1964-1981 (2009) · Zbl 1184.28013 · doi:10.1016/j.aim.2009.06.022 |
| [32] | Ferrante, J., Rackoff, C.: A decision procedure for the first order theory of real addition with order. SIAM J. Comput. 4, 69-76 (1975) · Zbl 0294.02022 · doi:10.1137/0204006 |
| [33] | Frougny, C.: Representations of numbers and finite automata. Math. Syst. Theory 25, 37-60 (1992) · Zbl 0776.11005 · doi:10.1007/BF01368783 |
| [34] | Frougny, C., Pelantova, E.: Beta-representations of 0 and Pisot numbers. J. Théor. Nombres Bordeaux (in press) · Zbl 1424.11107 |
| [35] | Frougny, C., Sakarovitch, J.: Number representation and finite automata. In: Combinatorics, Automata and Number Theory. Encyclopedia of Mathematics and Its Applications, vol. 135, pp. 34-107. Cambridge University Press, Cambridge (2010) · Zbl 1216.68142 |
| [36] | Frougny, C., Solomyak, B.: On representation of integers in linear numeration systems. In: Pollicott, M., Schmidt, K. (eds.) Ergodic Theory of \({\mathbb{Z}}^d\) Actions (Warwick, 1993-1994). London Mathematical Society Lecture Note Series, vol. 228, pp. 345-368. Cambridge University Press, Cambridge (1996) · Zbl 0856.11007 |
| [37] | Goč, D., Henshall, D., Shallit, J.: Automatic theorem-proving in combinatorics on words. Int. J. Found. Comput. Sci. 24(6), 781-798 (2013) · Zbl 1304.68143 · doi:10.1142/S0129054113400182 |
| [38] | Goč, D., Mousavi, H., Shallit, J.: On the number of unbordered factors. In: Language and Automata Theory and Applications. Lecture Notes in Computer Science, vol. 7810, pp. 299-310. Springer, Heidelberg (2013) · Zbl 1377.68191 · doi:10.1007/978-3-642-37064-9_27 |
| [39] | Hollander, M.: Greedy numeration systems and regularity. Theory Comput. Syst. 31, 111-133 (1998) · Zbl 0895.68088 · doi:10.1007/s002240000082 |
| [40] | Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Boston (1979) · Zbl 0426.68001 |
| [41] | Hutchinson, J.E.: Fractals and self-similarity. Indiana Univ. Math. J. 30(5), 713-747 (1981) · Zbl 0598.28011 · doi:10.1512/iumj.1981.30.30055 |
| [42] | Lecomte, P.B.A., Rigo, M.: Numeration systems on a regular language. Theory Comput. Syst. 34, 27-44 (2001) · Zbl 0969.68095 · doi:10.1007/s002240010014 |
| [43] | Leroux, J.: A polynomial time Presburger criterion and synthesis for number decision diagrams. In: Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, pp. 147-156. IEEE Computer Society (2005) |
| [44] | Löding, C.: Efficient minimization of deterministic weak ω-automata. Inform. Process. Lett. 79(3), 105-109 (2001) · Zbl 1032.68103 · doi:10.1016/S0020-0190(00)00183-6 |
| [45] | Lothaire, M.: Algebraic Combinatorics on Words. Encyclopedia of Mathematics and Its Applications, vol. 90. Cambridge University Press, Cambridge (2002) · Zbl 1001.68093 |
| [46] | Maler, O., Staiger, L.: On syntactic congruences for ω-languages. Theor. Comput. Sci. 183(1), 93-112 (1997) · Zbl 0911.68145 · doi:10.1016/S0304-3975(96)00312-X |
| [47] | Marsault, V., Sakarovitch, J.: Ultimate periodicity of b-recognisable sets: a quasilinear procedure. In: Developments in Language Theory. Lecture Notes in Computer Science, vol. 7907, pp. 362-373. Springer, Heidelberg (2013) · Zbl 1381.68128 · doi:10.1007/978-3-642-38771-5_32 |
| [48] | Milchior, A.: Büchi automata recognizing sets of reals definable in first-order logic with addition and order (2016). ArXiv:1610.06027 · Zbl 1485.03143 |
| [49] | Mousavi, H.: Automatic theorem proving in Walnut (2016). ArXiv:1603.06017 |
| [50] | Mousavi, H., Schaeffer, L., Shallit, J.: Decision algorithms for Fibonacci-automatic words, I: Basic results. RAIRO Theor. Inform. Appl. 50(1), 39-66 (2016) · Zbl 1366.68226 |
| [51] | Mousavi, H., Shallit, J.: Mechanical proofs of properties of the Tribonacci word. In: Combinatorics on Words. Lecture Notes in Computer Science, vol. 9304, pp. 170-190. Springer, Cham (2015) · Zbl 1350.68218 |
| [52] | Parry, W.: On the β-expansions of real numbers. Acta Math. Acad. Sci. Hung. 11, 401-416 (1960) · Zbl 0099.28103 · doi:10.1007/BF02020954 |
| [53] | Perrin, D., Pin, J.E.: Infinite Words. Automata, Semigroups, Logic and Games. Elsevier/Academic Press, Amsterdam (2004) · Zbl 1094.68052 |
| [54] | Rigo, M.: Construction of regular languages and recognizability of polynomials. Discret. Math. 254, 485-496 (2002) · Zbl 1002.68086 · doi:10.1016/S0012-365X(01)00377-6 |
| [55] | Rigo, M.: Formal Languages, Automata and Numeration Systems, Applications to Recognizability and Decidability, vol. 2. ISTE, Wiley (2014) · Zbl 1326.68003 |
| [56] | Salomaa, A., Soittola, M.: Automata-Theoretic Aspects of Formal Power Series. Springer, New York/Heidelberg (1978). Texts and Monographs in Computer Science · Zbl 0377.68039 · doi:10.1007/978-1-4612-6264-0 |
| [57] | Schaeffer, D.G.L., Shallit, J.: Subword complexity and k-synchronization. In: Developments in Language Theory. 17th International Conference, DLT 2013, Marne-la-Vallée, France, June 18-21, 2013. Proceedings, no. 7907 in Lecture Notes in Computer Science, pp. 252-263. Springer, Berlin (2013) · Zbl 1381.68234 |
| [58] | Schaeffer, L.: Deciding properties of automatic sequences. Master’s Thesis, University of Waterloo (2013) |
| [59] | Schaeffer, L., Shallit, J.: The critical exponent is computable for automatic sequences. Int. J. Found. Comput. Sci. 23(8), 1611-1626 (2012) · Zbl 1285.68138 · doi:10.1142/S0129054112400655 |
| [60] | Semenov, A.L.: Presburgerness of predicates regular in two number systems. Sibirskii Matematicheskii Zhurnal 18, 403-418 (1977, in Russian). English translation in Sib. J. Math. 18, 289-300 (1977) · Zbl 0411.03054 · doi:10.1007/BF00967164 |
| [61] | Shallit, J.: Decidability and enumeration for automatic sequences: a survey. In: Computer Science—Theory and Applications. Lecture Notes in Computer Science, vol. 7913, pp. 49-63. Springer, Heidelberg (2013) · Zbl 1381.68238 · doi:10.1007/978-3-642-38536-0_5 |
| [62] | Shallit, J.: Enumeration and automatic sequences. Pure Math. Appl. (PU.M.A.) 25(1), 96-106 (2015) · Zbl 1374.11038 |
| [63] | Staiger, L.: Finite-state ω-languages. J. Comput. Syst. Sci. 27(3), 434-448 (1983) · Zbl 0541.68052 · doi:10.1016/0022-0000(83)90051-X |
| [64] | Strogalov, A.S.: Regular languages with polynomial growth in the number of words. Diskret. Mat. 2(3), 146-152 (1990) · Zbl 0724.68065 |
| [65] | Zeckendorf, E.: Représentation des nombres naturels par une somme de nombres de Fibonacci ou de nombres Lucas. Bull. Soc. R. Liége 41, 179-182 (1972) · Zbl 0252.10011 |
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.
