5
$\begingroup$

Five years ago, I made a conjecture on the number of correlation classes that are exhibited by pairs of words in an alphabet of a given size. I later speculated that the conjecture could be tackled via automated theorem proving. I would now like to make some progress on this conjecture, by finding out whether there are any automated theorem provers capable of at least formulating a simpler statement along the same lines.

The simpler statement that I have chosen is Theorem 1 of Halava, V., Harju, T., & Ilie, L. (2000). Periods and binary words. Journal of Combinatorial Theory, Series A, 89(2), 298-303. This theorem is a restatement of part of Theorem 5.1 of Guibas, L. J., & Odlyzko, A. M. (1981). Periods in strings. Journal of Combinatorial Theory, Series A, 30(1), 19-42:

Theorem 1: For any alphabet $A$ and any word $w \in A^*$, there exists a word $w' \in \{0,1\}^*$ such that $\mathcal{P}(w') = \mathcal{P}(w).$

Here $\mathcal{P}(w)$ is the set of periods of the word $w$:

An integer $p,$ with $1 \leqslant p \leqslant |w|,$ is called a period of $w$ if $w_i = w_{i+p},$ for all $1 \leqslant i \leqslant |w|-p.$

My questions are:

  1. Which automated theorem provers are capable of formulating Theorem 1 with its proper semantics (i.e arbitrary finite strings over an arbitrary finite alphabet)?
  2. Which automated theorem provers are cable of proving Theorem 1, along the lines of Guibas and Odlyzko, or Halava, Harju and Ilie, or in an otherwise intelligible manner?
  3. How much work would be involved in creating such a formulation and proof? Would this be an undergraduate student assignment, a PhD project, or a decades-long project for a research team? Or would it require the development of new types of theorem provers?
$\endgroup$
  • 2
    $\begingroup$ What does $\mathcal{P}(w') \Rightarrow \mathcal{P}(w)$ mean? $\endgroup$ – Andrej Bauer Feb 18 '14 at 7:48
  • 1
    $\begingroup$ It would be helpful if you outlined the sort of proof you want automated, or at least tell us what techniques it uses. $\endgroup$ – Andrej Bauer Feb 18 '14 at 7:49
  • 1
    $\begingroup$ How automated would you expect things to be. I could imagine that most common proof assistantants should be able to formulate and proove this thing, with the help of an experienced user and taking the paper you referenced as a guideline. In the end you will obtain a formal proof which can be verified automatically. If you want the proof generation to be automatic, and follow the direction of that paper, that would likely be a completely different thing. $\endgroup$ – MvG Feb 18 '14 at 8:37
  • $\begingroup$ Is it just me, or is this Theorem rather trivial? You compute the length $n=\lvert w\rvert$ and period $p=\mathcal P(w)$ of $w$, then take a single one followed by $p-1$ zeros, and repeat that until the length of the word $w'$ formed in this way equals $n$. Am I missing something? $\endgroup$ – MvG Feb 18 '14 at 8:40
  • $\begingroup$ @MvG: consider the word $w=001200$, with $\mathcal{P}(w)=\{4,5\}$. Note that for finite strings, the gcd of two periods need not be a period. $\endgroup$ – Neil Strickland Feb 18 '14 at 8:53
3
$\begingroup$

I think that

  • Any of the standard theorem provers could formulate your statement without much trouble. There would be various choices about what kind of data structures to use (implicitly or explicitly), and the right choice might make a big difference to the ease of writing proofs.
  • I had a quick look at the paper of Halava et al, which is five pages long and is written explicitly as an algorithm to find $w'$. I think that anyone who was reasonably fluent with a proof assistant could encode and verify that proof without much trouble. One would expect the formalised proof to be several times longer than the paper. For this kind of work, I don't think there is much reason to prefer any one of the standard systems over the others.
  • I do not think that any existing proof assistant has any chance of finding such a proof for itself, unless you can cast the problem into a form that can be attacked by a SAT solver. I don't really know anything about SAT solvers myself but this post by Gowers seems relevant and interesting.
  • If you need to enumerate a bunch of cases to consider, I would be more inclined to use a system like Maple or Mathematica (or a general programming language) to do the initial enumeration. Later on, you could feed the results into a proof assistant to validate the overall logic if necessary.
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.