はじめに
想定読者
この記事を読む価値
TL;DR
- 本記事の主題
- この記事で扱うこと
対話篇:そもそも「処理系」とは何か
第１部 ── 「宣言的」という言葉は、３つの違うものを指している
- まずはSQL から
- 命令的とは何か
- Web の領域における「宣言的」
- ここまでに共通しているもの
- 関数型言語における「宣言的」
- 満たすべき性質を宣言する言語
- 定理証明支援系における「宣言的」
- 宣言の対象：３つの階層
第２部 ── 論証のための語彙
- タクティクとは何か
- タクティクの難点
- この難点は、開発者たち自身が認めている
- では、宣言的スタイルではどう書くのか
- 宣言的スタイルの語彙
- Isar には、事実を渡す構文が11種類ある
第３部 ── なぜ宣言的スタイルは読みやすいのか
- そもそも「演繹」とは何か
- なぜ「自然」演繹なのか
- 何と比べて「自然」なのか
- 導入規則と除去規則
- ゲンツェン流とヤシコフスキ流
- 「箱」とは何か
- では、木構造とは
- ヤシコフスキの箱
- 箱の構造が、そのまま構文になっている
- 【第３部の結論】
- 歴史の符合
第４部 ── 「読みやすい」とは、誰にとってか
- ① コードを書いている人間のプログラマ
- ② 数か月後の自分
- ③ 同僚、他のエンジニア
- ④ 査読者、数学の共同体
- ⑤ 大規模言語モデル
- 同じ冗長性が、読み手によって評価が逆転する
- この冗長性をどう評価するか？
  - 評価１: 冗長だから理解できる
  - 評価２: 冗長さが問題である
- 言い換えると
  - なぜ、評価が逆転するのか
- 第４部の結論
第５部 ── 計算をつなぐ書き方
- 数学の答案では、こう書く
- Isabelle の also と finally
- ... という記法
- finally が何をするか
- 事実を集める moreover と ultimately
- 【重要】これらは、言語に組み込まれた構文ではない
第６部 ── Lean 4 の calc
- 書き方
- Isabelle との違い
- calc で使える関係は、拡張できる
- Lean 4 の have と show
- まず、Isabelle の場合
- 次に、Lean 4 の場合
- 何が違うのか
- 見た目は同じでも、内部が違う
- Lean 4 には、Mizar に触発された構文もある
第７部 ── Agda の等式推論は、別の系統である
- Agda の等式推論
- しかし、書いているものが違う
- Ａとの違いは、何か
- 連載１回目の話とつながります
- だから、自動証明の能力が前提になります
- ３つを、隙間の大きさで並べると
- Agda は、２つ目のＢに属する
- 対話篇:Ｂは、手続き型に近いのではないか
- 「証明の対象」とは何か
- Mizar 系と Agda 系の違い
- なぜ、見た目が似るのか
- Lean 4 は、両方にまたがる
第８部 ── 同じ定理を、６つの言語で書く
- なぜ、この定理を選んだのか
- なお、Wiedijk も２つの定理で迷った
- 素数の無限性のコードを見たい方へ
- 証明したい命題
- ① Mizar
- 【重要】Trybulec 自身の注記
- ② Isabelle/Isar
- 【補足】Isar には、別の書き方もある
- ③ Agda
- ④ Lean 4
- 【重要】Mizar と Lean 4 の一行は、同じ構図である
- Lean 4 で、一から書いた場合
- ⑤ HOL Light の miz3
- ⑥ Rocq の C-zar
- 【注意】miz3 と C-zar だけ、定理が違う
- 語彙の対応表
- なぜ、こんなにも似ているのか
第９部 ── 30年の移植史
- 最初の実装:Mizar
- そして、移植が始まった
- 移植の一覧
- わずか41行で実装できる
- どの処理系にも載せられる
- 2026年、Lean 4 へ
第１０部 ── 定着したものと、しなかったもの
- 答え:一つだけ
- もう一人の証言
- miz3 の作者自身による位置づけ
- なぜ、Isar だけが定着したのか
- それでも、タクティクが選ばれる理由
- 実務での使い分け
第１１部 ── 長い証明での差
- ラグランジュの定理での比較
- この表から読み取れること
- 形式的証明の素描とは何か
- なぜ、骨格だけ書けるのか
- この部の結論
第１２部 ── AI が証明を書く時代の、宣言的スタイル
- まず、言葉を区別する
- 骨格を書いて、隙間を埋める
- 【重要】この手法は、1997年に提案されていた
- 1997年の Declare
- 1999年という年
- 2025年、同じ問題が再び論じられる
- 【この記事の見せ場】1997年と2025年で、同じ設計が目指されている
- 自然言語に近づける試み
- Naproche とは何か
- 実際のコードを見てください
- このコードの読み方
- 名前の区別
- Isar や Mizar と比べてください
- ただし、限界もあります
- 2026年、AI が移植を書いた
- 読める証明が必要な、もう一つの理由
- この部の結論
発展的な学習のために ── 専門書ではこう書かれています
- 用語の対応
- 表現の対応
実際に試すには
- Lean 4 をブラウザで試す
- 各言語の難易度
- 日本語の学習資料
日本語で読める議論
- 檜山正幸さんの記事
- myuon さんの記事
- タクティクの読みにくさをめぐる議論
おわりに
関連記事
出典
- 宣言的スタイルの分類と、その現況
- ６言語のコード
- C-zar
- Isar
- Declare
- 自然演繹
- 冗長性をめぐる議論
- AI と定理証明
- その他