核心概念
The first-order theory of Sturmian words over Presburger arithmetic is decidable, allowing for automatic reproval of classical theorems and new results.
摘要
この記事は、Sturmian wordsの第一階理論がPresburger算術上で決定可能であることを示しています。Baranwal、Schaeffer、ShallitによるOstrowski数表示の加算を認識する一般的な加算器を使用して、Presburger算術の第一階拡張が単一のSturmian wordによって均一にω-自動的であることを証明しました。これにより、この構造体の理論の決定可能性が導かれます。Pecanと呼ばれるこの決定アルゴリズムの実装を使用することで、Sturmian wordsに関する古典的な定理を数秒で再証明し、新しい結果も得られます。さらに、この記事ではSturmian wordsの基本的な結果や特性についても言及されています。
统计
α = [a0; a1, ...] (αは無理数)
Theorem A. The first-order logical theories FO(Ksturmian) and FO(Kchar) are decidable.
Fact 1.1 (Hieronymi [Hie16, Theorem A]). Let α be a quadratic irrational. Then FO(Rα) is decidable.
Fact 2.5: Let α = [a0; a1, ...], α' = [a'0; a'1, ...] ∈ R be irrational. Let k ∈ N be minimal such that ak ≠ a'k. Then α < α' if and only if...
Fact 2.7: Let x ∈ Iα. Then x can be written uniquely as ∞Σn=0 bn+1qn...
Fact 2.8 ([Hie16, Lemma 3.4]): Let X ∈ N be such that PNk=0 bk+1qk is the α-Ostrowski representation of X...
Fact 2.9 ([Hie16, Fact 2.13]): Let x, y ∈ Iα with x ≠ y and let [b1b2 · · · ]α and [c1c2 · · · ]α be the α-Ostrowski representations of x and y...
引用
"The first-order theory of Sturmian characteristic words is decidable."
"We show that no Sturmian word is eventually periodic."
"The theory FO(M) is decidable."