Search Results

Documents authored by Holub, Štěpán

Found 2 Possible Name Variants:

Holub, Štepán

Document
DOI: 10.4230/LIPIcs.ITP.2021.22
Formalization of Basic Combinatorics on Words

Authors: Štěpán Holub and Štěpán Starosta

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

Abstract
Combinatorics on Words is a rather young domain encompassing the study of words and formal languages. An archetypal example of a task in Combinatorics on Words is to solve the equation x ⋅ y = y ⋅ x, i.e., to describe words that commute. This contribution contains formalization of three important classical results in Isabelle/HOL. Namely i) the Periodicity Lemma (a.k.a. the theorem of Fine and Wilf), including a construction of a word proving its optimality; ii) the solution of the equation x^a ⋅ y^b = z^c with 2 ≤ a,b,c, known as the Lyndon-Schützenberger Equation; and iii) the Graph Lemma, which yields a generic upper bound on the rank of a solution of a system of equations. The formalization of those results is based on an evolving toolkit of several hundred auxiliary results which provide for smooth reasoning within more complex tasks.
Cite as

Štěpán Holub and Štěpán Starosta. Formalization of Basic Combinatorics on Words. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{holub_et_al:LIPIcs.ITP.2021.22,
  author =	{Holub, \v{S}t\v{e}p\'{a}n and Starosta, \v{S}t\v{e}p\'{a}n},
  title =	{{Formalization of Basic Combinatorics on Words}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{22:1--22:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.22},
  URN =		{urn:nbn:de:0030-drops-139177},
  doi =		{10.4230/LIPIcs.ITP.2021.22},
  annote =	{Keywords: combinatorics on words, formalization, Isabelle/HOL}
}
Document
DOI: 10.4230/LIPIcs.STACS.2016.44
Periods and Borders of Random Words

Authors: Štepán Holub and Jeffrey Shallit

Published in: LIPIcs, Volume 47, 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)

Abstract
We investigate the behavior of the periods and border lengths of random words over a fixed alphabet. We show that the asymptotic probability that a random word has a given maximal border length k is a constant, depending only on k and the alphabet size l. We give a recurrence that allows us to determine these constants with any required precision. This also allows us to evaluate the expected period of a random word. For the binary case, the expected period is asymptotically about n-1.641. We also give explicit formulas for the probability that a random word is unbordered or has maximum border length one.
Cite as

Štepán Holub and Jeffrey Shallit. Periods and Borders of Random Words. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 44:1-44:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{holub_et_al:LIPIcs.STACS.2016.44,
  author =	{Holub, \v{S}tep\'{a}n and Shallit, Jeffrey},
  title =	{{Periods and Borders of Random Words}},
  booktitle =	{33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)},
  pages =	{44:1--44:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-001-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{47},
  editor =	{Ollinger, Nicolas and Vollmer, Heribert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.44},
  URN =		{urn:nbn:de:0030-drops-57453},
  doi =		{10.4230/LIPIcs.STACS.2016.44},
  annote =	{Keywords: random word, period, word border}
}

Holub, Štěpán

Document
DOI: 10.4230/LIPIcs.ITP.2021.22
Formalization of Basic Combinatorics on Words

Authors: Štěpán Holub and Štěpán Starosta

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

Abstract
Combinatorics on Words is a rather young domain encompassing the study of words and formal languages. An archetypal example of a task in Combinatorics on Words is to solve the equation x ⋅ y = y ⋅ x, i.e., to describe words that commute. This contribution contains formalization of three important classical results in Isabelle/HOL. Namely i) the Periodicity Lemma (a.k.a. the theorem of Fine and Wilf), including a construction of a word proving its optimality; ii) the solution of the equation x^a ⋅ y^b = z^c with 2 ≤ a,b,c, known as the Lyndon-Schützenberger Equation; and iii) the Graph Lemma, which yields a generic upper bound on the rank of a solution of a system of equations. The formalization of those results is based on an evolving toolkit of several hundred auxiliary results which provide for smooth reasoning within more complex tasks.
Cite as

Štěpán Holub and Štěpán Starosta. Formalization of Basic Combinatorics on Words. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{holub_et_al:LIPIcs.ITP.2021.22,
  author =	{Holub, \v{S}t\v{e}p\'{a}n and Starosta, \v{S}t\v{e}p\'{a}n},
  title =	{{Formalization of Basic Combinatorics on Words}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{22:1--22:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.22},
  URN =		{urn:nbn:de:0030-drops-139177},
  doi =		{10.4230/LIPIcs.ITP.2021.22},
  annote =	{Keywords: combinatorics on words, formalization, Isabelle/HOL}
}
Document
DOI: 10.4230/LIPIcs.STACS.2016.44
Periods and Borders of Random Words

Authors: Štepán Holub and Jeffrey Shallit

Published in: LIPIcs, Volume 47, 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)

Abstract
We investigate the behavior of the periods and border lengths of random words over a fixed alphabet. We show that the asymptotic probability that a random word has a given maximal border length k is a constant, depending only on k and the alphabet size l. We give a recurrence that allows us to determine these constants with any required precision. This also allows us to evaluate the expected period of a random word. For the binary case, the expected period is asymptotically about n-1.641. We also give explicit formulas for the probability that a random word is unbordered or has maximum border length one.
Cite as

Štepán Holub and Jeffrey Shallit. Periods and Borders of Random Words. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 44:1-44:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{holub_et_al:LIPIcs.STACS.2016.44,
  author =	{Holub, \v{S}tep\'{a}n and Shallit, Jeffrey},
  title =	{{Periods and Borders of Random Words}},
  booktitle =	{33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)},
  pages =	{44:1--44:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-001-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{47},
  editor =	{Ollinger, Nicolas and Vollmer, Heribert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.44},
  URN =		{urn:nbn:de:0030-drops-57453},
  doi =		{10.4230/LIPIcs.STACS.2016.44},
  annote =	{Keywords: random word, period, word border}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact