Structure Computer
有理写像で書ける離散力学系について、「状態 t は状態 s から何歩で着くか、または着かないか」を、独立に検査できる証明書つきで答える。
答えは「t = σⁿ s ⇔ n ≡ r (mod M)」「道なし」「s は正則でない」のどれかで、体は有限体 𝔽_q か有理数 ℚ を選べる。既知の族については、Lean で証明した定理にもとづいて、軌道をたどれば何年もかかるほど大きい q でも答える。
答える系の族
| 系の種類 | 答え方 |
|---|---|
| Lyness 写像 | 定理で答える（大きい q でも軌道をたどらない） |
| Euler のコマを Kahan の方法で離散化した写像 | 定理で答える（大きい q でも軌道をたどらない） |
| 行列式が 1 の線形写像（離散化した振動子など） | 定理で答える（大きい q でも軌道をたどらない） |
| 双曲面上の測地線を離散化した写像の一つ | 定理で答える（大きい q でも軌道をたどらない） |
| 上の族を、座標を取り替えて書いた系 | 見抜いて、同じく定理で答える |
| それ以外の系 | 軌道をたどって答える（上限を超えれば「結果なし」） |
保証の仕組み
答えを計算する部分は、信頼しなくてよいように作られている。答えの正しさを支えるのは、独立の検査器と、事前に Lean で証明した定理である。
- 1計算
計算する部分が、答えと、それを安く確かめるための手がかりを作る
- 2証明書
問い・答え・確かさの種類・手がかり・前提と、よりどころにする定理の名前を、証明書にまとめる
- 3独立の検査
計算する部分とは別のプログラム（検査器）が、証明書だけを使って定義どおりに確かめ直す
- 4確かさつきの答え
確定・確率的に確定・復元値・統計・結果なしのどれか。検査に通らなければ計算し直し、それでもだめなら理由つきの「結果なし」