Email Gateway (Mar 16 2023 at 15:04): Email Gateway (Mar 16 2023 at 15:04):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
I’d like to announce two new AFP entries.
Intersection of two monoids generated by two element codes
by Štěpán Holub and Štěpán Starosta
This article provides a formalization of the classification of intersection
({x,y}^* \cap {u,v}^*) of two monoids generated by two element codes.
Namely, the intersection has one of the following forms
{beta, gamma}^* or (beta_0 + beta(gamma(1+delta+ ... + delta^t))^* epsilon)^*.
Note that it can be infinitely generated.
The result is due to [Karhumäki, 84]. Our proof uses the terminology of
morphisms which allows us to formulate the result in a shorter and more
transparent way.
https://www.isa-afp.org/entries/Two_Generated_Word_Monoids_Intersection.html
Binary codes that do not preserve primitivity
by Štěpán Holub and Martin Raška
A code X is not primitivity preserving if there is a primitive list ws in lists
X whose concatenation is imprimitive. We formalize a full characterization of
such codes in the binary case in the proof assistant Isabelle/HOL. Part of the
formalization, interesting on its own, is a description of {x,y}-interpretations
of the square xx if length y <= length x. We also provide a formalized
parametric solution of the related equation x^jy^k = z^l.
The core of the theory is an investigation of imprimitive words which are
concatenations of copies of two noncommuting words (such a pair of words is
called a binary code). We follow the article [Barbin-Le Rest, Le Rest, '85]
(mainly Théorème 2.1 and Lemme 3.1), while substantially optimizing the proof.
See also [Spehner, '76] for an earlier result on this question, and [Maňuch, '01]
for another proof.
https://www.isa-afp.org/entries/Binary_Code_Imprimitive.html
Enjoy,
René
Last updated: Jan 04 2025 at 20:18 UTC