An evaluable function computing the border array of a list in Isabelle/HOL is presented. The correctness of the function is verified in a straightforward lightweight manner, and it is applied to computation of other important properties of lists. A border of a word (word is used as a preferred synonym for 'list' or 'string' in this text) is a word (possibly empty, that is, of length 0) such that ̸= and is both prefix and sufix of . The maximal border of is its longest border. The concept of the border is complementary to the concept of a periodic root. If = · where is a border of , then is a periodic root of , that is, is a prefix of · · · · · (Here · denotes the concatenation, which is motivated by the fact words with concatenation form a monoid). Obviously, a border of is determined by its length. The border array BA = [0, . . . , ||− 1] of is the list (of the same length as , which is denoted here by ||) of natural numbers such that is the length of the maximal border of the prefix of of length + 1. In particular, the last element of BA is the length of the maximal border of . The border array, possibly slightly modified and with diferent terminology, is a well known structure. In particular, the border array of the searched pattern plays a crucial role in the Knuth-Morris-Pratt text search algorithm (cf. the function defined on p. 327 of [ 1]). Moreover, establishing the maximal border is itself a search task: the maximal border of corresponds to (the beginning of) the first repeated occurrence of in itself. It follows that using the eficient Knuth-Morris-Pratt algorithm for the computation of the maximal border of a word is equivalent to the first part of the algorithm, namely to the computation of the whole border array.
My interest in formalization of diferent aspects of periods of words, and therefore in (maximal)
borders, is motivated by the project formalizing combinatorics on words, see [
On the other hand, words commute if and only if they are powers of the same word. The rest is easy.
If we denote the maximal border of by (), we have = () · (). Therefore, being able to compute the maximal border yields an efective test of the primitivity of the word.
For convenience and future reference, I briefly and informally review a concrete version of the well known algorithm computing the border array. Let be the word whose maximal border we want to compute. Fix the elements of as = [, − 1, . . . , 1, 0], where || = + 1. Following the order of construction of lists we shall process from right to left, and construct gradually its sufix border array , that is, a list [||, ||− 1, . . . , 1] of natural numbers where is the length of the maximal border of , which is the sufix of of length .
The construction uses, in addition to , three variables arr, pos and bord with the following meaning. The integer pos indicates the currently processed position of , while arr is the sufix border array of the already processed part. More precisely, we have = 1 · 2, where pos = |1| and |arr| = |2|. The list arr = [|2|, . . . , 1] of natural numbers is the sufix border array of 2 (and a sufix of the computed sufix border array of ). The initial value of bord (for a new pos) is |2|.
The algorithm terminates with pos = 0. If pos ̸= 0, let be the last element of 1. The algorithm is currently looking for the maximal border of #2 (where # denotes insertion of an element at the beginning of a list), and considers # as a candidate, where is the prefix of 2 of length bord. Moreover (or bord) has two additional properties: • is a border of 2; • bord + 1 is an upper bound on the length of the maximal border of #2. These conditions reflect the basic idea of the algorithm: if # is the maximal border of #2, then is a border of 2, and (in view of the second condition) also a border of , which is also a sufix of 2. This dictates the next step: the algorithm compares and bord. • If = bord, then # is the maximal border of #2. Then arr can be updated, and the algorithm proceeds to pos − 1; • If ̸= bord, then there are two possibilities: – if is empty, then #2 is unbordered (its maximal border is empty), and we can again proceed to pos − 1; – otherwise, the next candidate is #′ where ′ is the maximal border of . The length of ′ is stored in arr, namely, it is bord.
My formalization of the above described algorithm in Isabelle/HOL is realized by three functions: kmp_arr, kmp_bord and kmp_pos which map the four parameters , arr, bord and pos to updated values corresponding to the situation after one step of the algorithm. The algorithm kmp is then a straightforward recursive call which is exited when pos = 0. The termination is obtained easily by the lexicographic order on the pair (pos, bord).
The invariant properties of variables described above are captured by the predicate kmp_valid. The key task is then to prove lemma kmp_valid_step which shows that the properties are indeed preserved by the above mentioned functions. That is, if (, arr, bord, pos) satisfies the predicate, then also the quadruple
︀( , kmp_arr( arr bord pos), kmp_bord( arr bord pos), kmp_pos( arr bord pos))︀ does. A fully structured commented proof in Isar language is given. Together with obvious validity of the predicate for the initial quadruple (, [0], 0, || − 1), this establishes the correctness proof, which is explicitly reformulated for the border_array (which simply inverts the sufix border array yielded by kmp).
Summarizing, our main goal is achieved by a pair of theorems. The correctness theorem bord_array shows that the function border_array indeed computes the desired length of maximal borders: theorem bord_array: assumes Suc k ≤ | |
w shows (border_array w)!k = |max_border (take (Suc k) w)| The function can be evaluated. For example,
value border_array [5,4,5,3,5,5,5,4,5::nat] yields
[
theorem max_border_comp [code]: max_border w = take ((border_array w)!(|w|− 1)) w
As can be seen, the described formalization is a handmade version of a verification process
which can be nowadays heavily automatized by the Isabelle Refinement Framework (IRF) by
Peter Lammich (see [
Therefore, in view of the above work, the value of the formalization presented here is open to judgment. I want to make two comments. First, using IRF brings about a significant overhead (in terms of the bootstrapping time for example) which discourages me from making my theory depend on it. In particular since the theory of borders is relatively simple layer of our larger development. Second, it is not clear (to me) how easily the exported code can be used in subsequent proofs in the way we need as indicated in Section 2, and described in the next section.
Using appropriate code equations we are now able to evaluate several important properties of particular words, like the maximal border, the minimal periodic root and the minimal period, as well as predicates bordered and primitive. For example, primitivity can be tested using Lemma 1 and the equality = () · () by the following four pieces of code leading to the function KMP described in the previous section: lemma primitive_if [code]: primitive w →← w ̸= ∧ ( w = w ∨ w · w ̸= w · w) lemma min_per_root_take [code]: w = take (|w| − |max_border w|) w lemma max_border_comp [code]: max_border w = take ((border_array w)!(|w|− 1)) w fun border_array :: ′a list ⇒ nat list where
border_array = | border_array (a#w) = rev (KMP (rev (a#w)) [0] 0 (|a#w|− 1)) An obvious drawback is that the evaluation is available only for types that are of class equal, which does not apply to general lists of type ’a list. In order to avoid this limitation, we encode into a binary alphabet (which is of class equal) by a simple function bin_encode: fun bin_encode :: ′b ⇒ ′b ⇒ ′b ⇒ Enum.finite_2
where bin_encode x y = ( z. (if z = x then Enum.finite_2 .a1 else Enum.finite_2 .a2)) Decoding function bin_decode is analogous. We can now prove that the encoded word is primitive if and only if the original one is: lemma prim_bin_enc_if : assumes x ̸= y and ws ∈ lists {x,y}
shows primitive ws →← primitive (map (bin_encode x y) ws)
An archive version of the formalization described in this paper is available at [
A current (and possibly significantly modified) version of these theories is maintained as part of
our large development [
Note added in proof: Recently, we implemented an alternative method of proving primitivity of a word, which makes this particular application of the border array calculation slightly outdated. We have also already formalized the theorem spehner, which was used without proof (with sorry) for sake of illustration in the theory Spehner.thy (see [10]).
The author acknowledge support by the Czech Science Foundation grant GAČR 20-20621S. [10] Š. Holub, M. Raška, Š. Starosta, Binary codes that do not preserve primitivity, IJCAR 2022, accepted.