×

Mechanical proofs of properties of the Tribonacci word. (English) Zbl 1350.68218

Manea, Florin (ed.) et al., Combinatorics on words. 10th international conference, WORDS 2015, Kiel, Germany, September 14–17, 2015. Proceedings. Cham: Springer (ISBN 978-3-319-23659-9/pbk; 978-3-319-23660-5/ebook). Lecture Notes in Computer Science 9304, 170-190 (2015).
In this very interesting paper, the authors use a computerized formal method to prove properties of the Tribonacci word, i.e., the fixed point of the morphism \(0 \rightarrow 01, 1 \rightarrow 02, 2 \rightarrow 0\). These mechanical proofs yield some old results from the literature as well as some new results. Many of them relate to occurrences of squares, cubes, and palindromes in the Tribonacci word, and to its subword complexity, which calculates the number of subwords of any given length in the word. The method has not yet been successful in proving, for instance, results regarding the abelian complexity of the Tribonacci word (similar to subword complexity but up to permutation of letters) since the method runs out of space.
For the entire collection see [Zbl 1320.68023].

MSC:

68R15 Combinatorics on words
03B25 Decidability of theories and sets of sentences
03B35 Mechanization of proofs and logical operations
11B85 Automata sequences
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Allouche, JP; Rampersad, N.; Shallit, J., Periodicity, repetitions, and orbits of an automatic sequence, Theoret. Comput. Sci., 410, 2795-2803 (2009) · Zbl 1173.68044 · doi:10.1016/j.tcs.2009.02.006
[2] Allouche, JP; Shallit, J., Automatic Sequences: Theory, Applications, Generalizations (2003), Cambridge: Cambridge University Press, Cambridge · Zbl 1086.11015 · doi:10.1017/CBO9780511546563
[3] Barcucci, E.; Bélanger, L.; Brlek, S., On Tribonacci sequences, Fibonacci Quart., 42, 314-319 (2004) · Zbl 1138.11309
[4] Berstel, J.; Reutenauer, C., Noncommutative Rational Series with Applications, Encylopedia of Mathematics and Its Applications (2011), Cambridge: Cambridge University Press, Cambridge · Zbl 1250.68007
[5] Bruyère, V.; Hansel, G., Bertrand numeration systems and recognizability, Theoret. Comput. Sci., 181, 17-43 (1997) · Zbl 0957.11015 · doi:10.1016/S0304-3975(96)00260-5
[6] Bruyère, V., Hansel, G., Michaux, C.,Villemaire, R.: Logic and \(p\)-recognizable sets of integers. Bull. Belgian Math. Soc. 1, 191-238 (1994), corrigendum. Bull. Belg. Math. Soc. 1, 577 (1994) · Zbl 0804.11024
[7] Carlitz, L., Scoville, R., Hoggatt, Jr., V.E.: Fibonacci representations of higher order. Fibonacci Quart. 10, 43-69, 94 (1972) · Zbl 0236.05002
[8] Charlier, E.; Rampersad, N.; Shallit, J., Enumeration and decidable properties of automatic sequences, Int. J. Found. Comp. Sci., 23, 1035-1066 (2012) · Zbl 1282.68186 · doi:10.1142/S0129054112400448
[9] Chekhova, N.; Hubert, P.; Messaoudi, A., Propriétés combinatoires, ergodiques et arithmétiques de la substitution de Tribonacci, J. Théorie Nombres Bordeaux, 13, 371-394 (2001) · Zbl 1038.37010 · doi:10.5802/jtnb.328
[10] Christou, M., Crochemore, M., Iliopoulos, C.S.: Quasiperiodicities in Fibonacci strings (2012), to appear in Ars Combinatoria. Preprint available at http://arxiv.org/abs/1201.6162 · Zbl 1413.05002
[11] Cobham, A., Uniform tag sequences, Math. Syst. Theory, 6, 164-192 (1972) · Zbl 0253.02029 · doi:10.1007/BF01706087
[12] Droubay, X.; Justin, J.; Pirillo, G., Episturmian words and some constructions of de Luca and Rauzy, Theoret. Comput. Sci., 255, 539-553 (2001) · Zbl 0981.68126 · doi:10.1016/S0304-3975(99)00320-5
[13] Du, C.F., Mousavi, H., Schaeffer, L., Shallit, J.: Decision algorithms for Fibonacci-automatic words, with applications to pattern avoidance (2014). http://arxiv.org/abs/1406.0670 · Zbl 1366.68224
[14] Duchêne, E.; Rigo, M., A morphic approach to combinatorial games: theTribonacci case, RAIRO Inform. Théor. App., 42, 375-393 (2008) · Zbl 1143.91314 · doi:10.1051/ita:2007039
[15] Frougny, C., Representations of numbers and finite automata, Math. Systems Theory, 25, 37-60 (1992) · Zbl 0776.11005 · doi:10.1007/BF01368783
[16] Frougny, C.; Solomyak, B.; Pollicott, M.; Schmidt, K., On representation of integers in linear numeration systems, Ergodic Theory of \({\mathbb{Z}}^d\) Actions (Warwick, 1993-1994), 345-368 (1996), Cambridge: Cambridge University Press, Cambridge · Zbl 0856.11007
[17] Glen, A.: On sturmian and episturmian words, and related topics. Ph.D. thesis, University of Adelaide (2006) · Zbl 1102.68516
[18] Glen, A., Powers in a class of \(a\)-strict episturmian words, Theoret. Comput. Sci., 380, 330-354 (2007) · Zbl 1119.68140 · doi:10.1016/j.tcs.2007.03.023
[19] Glen, A.; Justin, J., Episturmian words: a survey, RAIRO Inform. Théor. App., 43, 402-433 (2009) · Zbl 1182.68155
[20] Glen, A.; Levé, F.; Richomme, G., Quasiperiodic and Lyndon episturmian words, Theoret. Comput. Sci., 409, 578-600 (2008) · Zbl 1155.68065 · doi:10.1016/j.tcs.2008.09.056
[21] Goč, D.; Henshall, D.; Shallit, J.; Moreira, N.; Reis, R., Automatic theorem-proving in combinatorics on words, Implementation and Application of Automata, 180-191 (2012), Heidelberg: Springer, Heidelberg · Zbl 1297.68215 · doi:10.1007/978-3-642-31606-7_16
[22] Goč, D.; Mousavi, H.; Shallit, J.; Dediu, A-H; Martín-Vide, C.; Truthe, B., On the number of unbordered factors, Language and Automata Theory and Applications, 299-310 (2013), Heidelberg: Springer, Heidelberg · Zbl 1377.68191 · doi:10.1007/978-3-642-37064-9_27
[23] Goč, D.; Saari, K.; Shallit, J.; Dediu, A-H; Martín-Vide, C.; Truthe, B., Primitive words and Lyndon words in automatic and linearly recurrent sequences, Language and Automata Theory and Applications, 311-322 (2013), Heidelberg: Springer, Heidelberg · Zbl 1377.68192 · doi:10.1007/978-3-642-37064-9_28
[24] Goč, D.; Schaeffer, L.; Shallit, J.; Béal, M-P; Carton, O., Subword complexity and k-synchronization, Developments in Language Theory, 252-263 (2013), Heidelberg: Springer, Heidelberg · Zbl 1381.68234 · doi:10.1007/978-3-642-38771-5_23
[25] Hales, TC, Formal proof, Notices Am. Math. Soc., 55, 11, 1370-1380 (2008) · Zbl 1188.68002
[26] Justin, J.; Pirillo, G., Episturmian words and episturmian morphisms, Theoret. Comput. Sci., 276, 281-313 (2002) · Zbl 1002.68116 · doi:10.1016/S0304-3975(01)00207-9
[27] Konev, B., Lisitsa, A.: A SAT attack on the Erdős discrepancy problem (2014). Preprint available at http://arxiv.org/abs/1402.2184 · Zbl 1343.68217
[28] Presburger, M.: Über die Volständigkeit eines gewissen Systems derArithmetik ganzer Zahlen, in welchem die Addition als einzigeOperation hervortritt. In: Sparawozdanie z I Kongresu matematykówkrajów slowianskich, Warsaw, pp. 92-101, 395 (1929) · JFM 56.0825.04
[29] Presburger, M., On the completeness of a certain system of arithmetic of whole numbers in which addition occurs as the only operation, Hist. Phil. Logic, 12, 225-233 (1991) · Zbl 0741.03027 · doi:10.1080/014453409108837187
[30] Richomme, G.; Saari, K.; Zamboni, LQ, Balance and Abelian complexity of the Tribonacci word, Adv. Appl. Math., 45, 212-231 (2010) · Zbl 1203.68131 · doi:10.1016/j.aam.2010.01.006
[31] Rosema, S.W., Tijdeman, R.: The Tribonacci substitution. INTEGERS 5 (3), Paper #A13 (2005). Available at http://www.integers-ejcnt.org/vol5-3.html · Zbl 1099.11004
[32] Shallit, J.; Bulatov, AA; Shur, AM, Decidability and enumeration for automatic sequences: a survey, Computer Science - Theory and Applications, 49-63 (2013), Heidelberg: Springer, Heidelberg · Zbl 1381.68238 · doi:10.1007/978-3-642-38536-0_5
[33] Tan, B.; Wen, ZY, Some properties of the Tribonacci sequence, Eur. J. Comb., 28, 1703-1719 (2007) · Zbl 1120.11009 · doi:10.1016/j.ejc.2006.07.007
[34] Turek, O.: Abelian complexity function of the Tribonacci word. J. Integer Sequences 18, Article 15.3.4 (2015). Available at https://cs.uwaterloo.ca/journals/JIS/VOL18/Turek/turek3.html · Zbl 1311.68128
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.