Structure Computer
Structure Computer は、決まった規則で 1 歩ずつ状態が移り変わる系（離散力学系）について、その「構造」を厳密に計算し、答えに第三者が検査できる証明書を付けるシステムである。
数値シミュレーションは「これから何が起きるか」を近似で答える。Structure Computer が答えるのはその反対側の問い、つまり「どの状態に行き着き、どの状態には決して行き着かないか」「何が決して変わらないか」であり、丸め誤差のない計算と、あらかじめ証明した数学の定理にもとづいて答える。
Structure Computer は特許出願中である。
扱う系
状態は数の組で、次の状態は四則演算で書ける式（有理式）で決まる。たとえば Lyness の漸化式
xₙ₊₁ = (1 + xₙ) / xₙ₋₁
は、状態を (x, y) = (xₙ₋₁, xₙ) とすると、1 歩の規則が
(x, y) ↦ (y, (1 + y) / x)
の系になる。このような規則は、構造を保つ数値計算法（積分法）、可積分な写像、可逆計算などの研究に現れる。系は、既知の系を名前で選ぶか、変数・パラメータ・1 歩の式を並べた短いテキスト（系ファイル）で書く（例題）。
中心の問い：s から t へ何歩で着くか
上の系を s = (1, 2) から動かすと
(1, 2) → (2, 3) → (3, 2) → (2, 1) → (1, 1) → (1, 2)
と 5 歩で元に戻る。したがって t = (2, 1) には 3 歩で着き、8 歩、13 歩、… でも着く。規則は逆向きにもたどれるので、2 歩戻っても（n = −2）着く。Structure Computer はこれを
t = σⁿ s ⇔ n ≡ 3 (mod 5)
と答える。σ は 1 歩進めること、n ≡ 3 (mod 5) は「n を 5 で割ると 3 余る」ことである。t に着く歩数を逆向きも含めてすべて挙げ、それ以外の歩数では着かないことまで、一度に述べている。
答えは次の 3 つのどれかである。
| 答え | 意味 |
|---|---|
| t = σⁿ s ⇔ n ≡ r (mod M) | n を M で割って r 余るときに限り、n 歩で t に着く |
| 道なし | 何歩進めても戻しても、t には着かない |
| s は正則でない | s から進める（または戻す）途中で、式が定義されない状態（0 で割る）に行き当たる。そこまでに t に着くなら、その歩数を添える |
このサイトでは、この問いを Id(s, t) と書く。型理論で「2 つのものが等しいことの証拠の集まり」を表す記号にならったもので、ここでは「s から t への道（歩数）の集まり」を表す。
誤差のない計算：有限体と有理数
浮動小数点の計算では丸め誤差が積み重なり、長い時間がたった後の振る舞いは信用できなくなる。Structure Computer は、次の 2 つの、何も丸めない数の世界で計算する。
- 𝔽_q（有限体）：素数 q で割った余りだけで計算する世界。時計の針が 12 を過ぎると 0 に戻るのと同じように、値はいつも 0 から q − 1 までの整数になる。
- ℚ（有理数）：分数を分数のまま、正確に計算する。
q が大きいと、軌道は 1 歩ずつたどっていては終わらないほど長くなりうる。次の既知の族については、Lean で証明した定理にもとづいて、軌道をたどらずに答える。
- Lyness 写像
- Euler のコマ（回転する剛体）を Kahan の方法で離散化した写像
- 行列式が 1 の線形写像（離散化した調和振動子など）
- 双曲面上の測地線を離散化した写像の一つ
それ以外の系では、決めた上限の範囲で軌道を実際にたどり、上限を超えれば「結果なし」と答える。
ほかに答える問い
同じ仕組み（計算 → 証明書 → 独立の検査）で、Id(s, t) のほかに 11 種の構造の問いに答える。たとえば次のようなものがある。
- 規則を逆向きにたどれるか（可逆性）
- 軌道の周期がどう分布するか（周期構造）
- 運動が規則的な「可積分」な系か（可積分性）
- 軌道に沿って値が変わらない量（保存量）を見つける。与えた式が保存量かを確かめる
一覧と、それぞれで何が分かるかは「問い」にある。
答えの保証
Structure Computer は、計算する部分を信頼しなくてよいように作られている。
- 計算する部分が、答えと、それを安く確かめるための手がかりを作る。
- 問い・答え・手がかり・前提と、よりどころにする定理の名前を、証明書にまとめる。
- 計算する部分とは別のプログラム（検査器）が、証明書だけを使って、定義どおりに確かめ直す。
- 検査に通らなければ計算し直し、それでも通らなければ、理由を付けて「結果なし」を返す。
主な答えについては、「検査器が確かめる条件が成り立てば答えは正しい」ことを、証明支援系 Lean（数学の証明をコンピュータが 1 行ずつ確かめる道具）の定理としてあらかじめ証明してある。証明書はその定理を名前で引用するので、証明書を持つ人は誰でも、検査器で答えを確かめ直せる。𝔽_q 上の Lyness 写像の問いは、正しさ自体を Lean で証明した検査プログラムでも確かめられる。
結果には、どこまで確かかを表す種類が付く。
| 種類 | 意味 |
|---|---|
| 確定 | 検査と定理によって正しいと言える |
| 確率的に確定 | 誤りの確率が無視できるほど小さいと保証される |
| 復元値 | 値の大きさに上限があるという前提のもとで求めた値 |
| 統計 | 標本にもとづく判断 |
| 結果なし | 答えられなかった。理由を添える |
確かめられないものを「確定」とは言わない。
Structure Computer の新しさ
離散力学系を調べる道具はこれまでにもあるが、それぞれに足りないところがある。数値シミュレーションの答えは近似で、「決して着かない」とは言えない。数式処理は答えを出すが、その答えを他の人が独立に確かめるための証拠は付かない。証明支援系は定理を確かめるが、個々の系の個々の問いに答えを計算するものではない。Structure Computer は、この 3 つを 1 つにまとめた。
- 厳密な答え：「何歩で着くか」に、着く歩数のすべてと「それ以外では着かない」ことまでを、誤差なしで答える。「道なし」も、たどった範囲で見つからなかったという意味ではなく、どの歩数でも着かないという主張である。
- 答えごとの証明書：どの答えにも、計算をした側を信じなくても検査できる証明書が付く。計算した本人以外の誰でも、検査器で確かめ直せる。
- 定理による裏付け：答えの正しさのよりどころは、Lean で証明した定理である。定理は q を 1 つずつ確かめたものではなく、有限体一般について、例外的な場合も含めて証明してある。
- 途方もなく大きな問いにも答える：既知の族では、軌道を 1 歩ずつたどれば終わらない大きさの q でも、定理にもとづいて答える。
- 分からないことを分からないと言う：結果には確かさの種類が付き、確かめられないものを「確定」とは言わない。
想定する使い道
次のような場面での利用を想定している。
- 構造を保つ数値計算法の設計で、可逆性や保存量を、浮動小数点での長時間の試験ではなく、厳密に確かめる
- 可積分な写像、算術力学系、可逆計算などの研究で、周期や保存量を、誰でも確かめ直せる形で示す
- 計算の結果を、第三者が計算を全部やり直さずに検査できる証拠として残す
できないこと
- 扱うのは、四則演算（多項式・有理式）で書ける規則である。
- 有限体には大小も距離もないので、軌道がどれだけ近づくか、誤差がどう広がるかといった「近さ」の問いには答えない。数値シミュレーションの代わりではなく、それを補うものである。
- 既知の族と認識できない系では、大きい q の問いに定理で答えることはできない。上限まで軌道をたどり、超えれば「結果なし」と答える。