×

Lyndon words formalized in Isabelle/HOL. (English) Zbl 1511.68214

Moreira, Nelma (ed.) et al., Developments in language theory. 25th international conference, DLT 2021, Porto, Portugal, August 16–20, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12811, 217-228 (2021).
Summary: We present a formalization of Lyndon words and basic relevant results in Isabelle/HOL. We give a short review of Isabelle/HOL and focus on challenges that arise in this formalization. The presented formalization is based on an ongoing larger project of formalization of combinatorics on words.
For the entire collection see [Zbl 1482.68035].

MSC:

68R15 Combinatorics on words
68V20 Formalization of mathematics in connection with theorem provers
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Archive of Formal Proofs. https://www.isa-afp.org/topics.html · Zbl 1417.68176
[2] Bannai, H., Tomohiro, I., Inenaga, S., Nakashima, Y., Takeda, M., Tsuruta, K.: A new characterization of maximal repetitions by Lyndon trees. In: Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms. Society for Industrial and Applied Mathematics (December 2015) · Zbl 1372.68216
[3] Blanchette, JC; Kaliszyk, C.; Paulson, LC; Urban, J., Hammering towards QED, J. Form. Reason., 9, 1, 101-148 (2016) · Zbl 1451.68318
[4] Carpi, A.; Fici, G.; Holub, Š.; Opršal, J.; Sciortino, M.; Csuhaj-Varjú, E.; Dietzfelbinger, M.; Ésik, Z., Universal Lyndon words, Mathematical Foundations of Computer Science 2014, 135-146 (2014), Heidelberg: Springer, Heidelberg · Zbl 1425.68325 · doi:10.1007/978-3-662-44522-8_12
[5] Dolce, F.; Restivo, A.; Reutenauer, C., On generalized Lyndon words, Theor. Comput. Sci., 777, 232-242 (2019) · Zbl 1426.68229 · doi:10.1016/j.tcs.2018.12.015
[6] Duval, JP, Génération d’une section des classes de conjugaison et arbre des mots de Lyndon de longueur bornée, Theor. Comput. Sci., 60, 3, 255-283 (1988) · Zbl 0673.68042 · doi:10.1016/0304-3975(88)90113-2
[7] Fredricksen, H.; Maiorana, J., Necklaces of beads in \(k\) colors and \(k\)-ary de Bruijn sequences, Discret. Math., 23, 3, 207-210 (1978) · Zbl 0384.05004 · doi:10.1016/0012-365X(78)90002-X
[8] Harrison, J.; Berghofer, S.; Nipkow, T.; Urban, C.; Wenzel, M., Without loss of generality, Theorem Proving in Higher Order Logics, 43-59 (2009), Heidelberg: Springer, Heidelberg · Zbl 1252.68254 · doi:10.1007/978-3-642-03359-9_3
[9] Hivert, F., et al.: Coq-Combi (2021). https://github.com/hivert/Coq-Combi
[10] Holub, Š., Starosta, Š., et al.: Combinatorics on words formalized (2021). https://gitlab.com/formalcow/combinatorics-on-words-formalized · Zbl 1477.68152
[11] Holub, Š.; Veroff, R.; Kari, J.; Manea, F.; Petre, I., Formalizing a fragment of combinatorics on words, Unveiling Dynamics and Complexity, 24-31 (2017), Cham: Springer, Cham · Zbl 1433.68579 · doi:10.1007/978-3-319-58741-7_3
[12] Holub, Š., Raška, M., Starosta, Š.: Combinatorics on words basics. Archive of Formal Proofs (May 2021). https://isa-afp.org/entries/Combinatorics_Words.html. Formal proof development
[13] Holub, Š., Starosta, Š.: Lyndon words. Archive of Formal Proofs (May 2021). https://isa-afp.org/entries/Combinatorics_Words_Lyndon.html. Formal proof development
[14] Isabelle generic proof assistant. https://isabelle.in.tum.de/
[15] Kaliszyk, C.; Rabe, F.; Benzmüller, C.; Miller, B., A survey of languages for formalizing mathematics, Intelligent Computer Mathematics, 138-156 (2020), Cham: Springer, Cham · Zbl 1455.68257 · doi:10.1007/978-3-030-53518-6_9
[16] Lothaire, M., Combinatorics on Words (1997), Cambridge: Cambridge University Press, Cambridge · Zbl 0874.20040 · doi:10.1017/CBO9780511566097
[17] Lyndon, RC, On Burnside’s problem, Trans. Am. Math. Soc., 77, 2, 202-215 (1954) · Zbl 0058.01702
[18] Marcus, S.; Sokol, D., 2D Lyndon words and applications, Algorithmica, 77, 1, 116-133 (2015) · Zbl 1362.68240 · doi:10.1007/s00453-015-0065-z
[19] Nikpow, T.: A tutorial introduction to structured Isar proofs. https://courses.grainger.illinois.edu/cs576/sp2015/doc/isar-overview.pdf
[20] Nipkow, T.; Prehofer, C., Type reconstruction for type classes, J. Funct. Program., 5, 2, 201-224 (1995) · Zbl 0833.68025 · doi:10.1017/S0956796800001325
[21] Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): 9. Advanced Simplification, Recursion, and Induction. Isabelle/HOL. LNCS, vol. 2283, pp. 175-193. Springer, Heidelberg (2002). doi:10.1007/3-540-45949-9_9
[22] Raška, M., Starosta, Š.: Producing symmetrical facts for lists induced by the list reversal mapping in Isabelle/HOL. http://arxiv.org/abs/2104.11622 (2021)
[23] Thompson, S.: Type Theory and Functional Programming. Addison-Wesley, Boston (1991). https://www.cs.kent.ac.uk/people/staff/sjt/TTFP · Zbl 0753.68026
[24] Wiedijk, F.: Formalizing 100 theorems. https://www.cs.ru.nl/ freek/100/ · Zbl 1176.91039
[25] Zeller, P.: Szpilrajn extension theorem. Archive of Formal Proofs (July 2019). https://isa-afp.org/entries/Szpilrajn.html. Formal proof development
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.