Fibonacci Challenge

The infinite sequence of Fibonacci words is defined recursively as

w(0) = b
w(1) = a
w(i_+2) = w(i)w(i+1)

and consists of the words b, a, ba, aba, baaba, ababaaba, ...

After quick inspection one may notice that none of the words in the sequence above contains 'bb' as a subword. The same seems to be true for the subword 'aaa'. Indeed, these are known properties of Fibonacci words and the reader may wish to try to prove it himself/herself, or consult String Rewriting and the Fibonacci Word by Steve Whealton for further hints and easygoing introduction.

I call the problem(s) of proving that netheir 'bb' nor 'aaa' appear as the subwords in Fibonachhi words the Fibonacci puzzle(s).

Automated Solution

In Tackling Fibonacci words puzzles by finite countermodels (to appear in Proc. of FWFM 2013 ) I have demonstrated the automated solution to both variants of the Fibonacci puzzle using automated finite model finding for first-order logic. In that I have followed the general FCM (Finite CounterModels) methodology for the safety verification of infinite state and parameterized systems.

I was surprised by the simplicity of these soultions and the power of FCM method in this context. I strongly suspect that it would be difficult to get such a solution in any other way. That is why the challenge below.

Fibonacci Challenge

I would like to challenge anyone to demonstrate an alternative automated solution(s) to both variants of Fibonacci puzzle above (no 'bb' and no 'aaa' as the subwords).

Original condition (ceased by 25.07.2013):
I, Alexei Lisitsa, will pay 50 GBP (fifty British pounds, or an equivalent in an agreed currency) to the author of the first submitted solution satisfying the conditions below.

Update: As the first correct solution has arrived (see below) and the author of the solution has declined to accept the award, the conditions of the challenge have changed to

New condition (starts 25.07.2013, 15:30 UTC time)
I, Alexei Lisitsa, will pay 30 GBP (thirty British pounds, or an equivalent in an agreed currency) and 20 GBP (twenty British pounds, or an equivalent in an agreed currency) to the authors of the second and third submitted solutions, respectively. The solutions should satisfy the conditions below.

Any tools can be used for such solutions (theorem provers, SMT and SAT tools, special algorithms, etc);
Solutions should be reproducible, so please indicate/provide with a tool and instructions of how to execute your solutuion;
Solution should be alternative to the one described in the paper Tackling Fibonacci words puzzles by finite countermodels and to the all solutions already made public on this web page. Since the novelty is difficult to formalize, I will apply my best judgement and common sense to decide. Please provide a short explanation of why your solution is an alternative;
Solution should be non-vacuous. For example, the program just priniting "yes, no words bb or aa" won't count :-)

The challenge starts 13.07.2013 at 13:00 UTC time

The updated challenge starts 25.07.2013 at 15.30 UTC time

Please submit your solution to A.Lisitsa@liverpool.ac.uk (sub: Fibonacci challenge). The second and third soultions will be judged by the time they received at the email box. If you have any questions on the challenge please send an email to A.Lisitsa@liverpool.ac.uk (subj: Q on Fibonacci challenge)

Solutions arrived

First solution:
Author: Naoki Kobayashi, Received: 25.07.2013 4:50 UTC time
From author's description:
"It can be easily solved by reduction to higher-order model checking (or, model checking of higher-order recursion schemes), which asks if the (possibly infinite) tree generated by a higher-order tree grammar (called higher-order recursion scheme) satisfies a given regular property.
In the case of your Fibonacci challenge, one can write a grammar that generates the tree of which each path corresponds to a Fibonacci number:
-------
S = Fib b a.
Fib x y = br (x e) (Fib y (Concat x y)).
Concat x y z = x (y z).
-------
One can also specifiy properties "no bb" "no aaa" by using tree automata, hence one can solve your challenge by using a higher-order model checker. I attach below two input files for our higher-order model checker TRecS (which can be tested at TRecS (Types for RECursion Schemes): Type-Based Model Checker for Higher-Order Recursion Schemes ), respectively for "no bb" and "no aaa" . In general, you can use this approach to decide inclusion between higher-order languages (cf. Werner Damm: The IO- and OI-Hierarchies. Theor. Comput. Sci. 20: 95-207 (1982)) and regular languages."