要約

  • Edinburgh LCF のタクティックは目標を部分目標に分け、validation を返す。部分目標の theorem を原始推論規則で組み上げ、元の目標の theorem を生成できて初めて結果は受理された。
  • 抽象型 thm は定理生成の権限を持つコードを絞ったが、論理体系の無矛盾性、仕様と現実の一致、コンパイラ・実行環境・ハードウェアの無欠陥性までは証明しない。
  • 成果は共同のものだ。基礎となる論理は Dana Scott に由来し、Stanford LCF が先行した。Michael Gordon、Christopher Wadsworth、Lockwood Morris、Malcolm Newey らも Edinburgh LCF と ML に貢献した。

探索の終了と定理の成立は別である

対話型証明はしばしば目標から逆向きに進む。タクティックは書き換えを試し、目標を細分化し、失敗すれば戻り、別の手順を組み合わせる。長いログが「すべて解けた」と示しても、LCF はもう一つの問いを残す。主張された結論を、保護されたインターフェースだけで構築できるのか。

タクティックは部分目標とともに validation を返す。これは部分目標の theorem 値を受け取り、元の目標の theorem を構成する関数である。逆向きの探索は、後で順向きの導出として清算される。validation が約束を果たせなければ、成功表示は定理にならない。

この分離は、拡張性と信頼の衝突を解いた。利用者は新しい証明手法を書きたいが、そのコードは誤り得る。拡張がどれも theorem を直接生成できれば、タクティックの追加ごとに信頼範囲が広がる。Edinburgh LCF は theorem を通常 thm と呼ばれる抽象型に封じ、公理と原始推論規則だけをその型の生成操作とした。

したがって、タクティックそのものが正しいわけではない。停止しないことも、不適切な部分目標を選ぶことも、例外を起こすことも、誤った validation を返すこともある。保証はもっと狭い。境界外の誤りは別の生成口を与えず、求めた theorem を得られないという失敗にとどまる。

Stanford から Edinburgh へ――単独発明ではない

Milner は 1972 年、Dana Scott の Logic for Computable Functions を対象とする実装済み証明チェッカーを報告した。Stanford LCF は機械支援の可能性を示す一方、長い証明を低水準で扱う負担も露呈した。Milner が 1973 年に Edinburgh へ移った後、よりプログラム可能な環境が築かれた。

1979 年の標準的な書籍 Edinburgh LCF の著者は Michael J. C. Gordon、Robin Milner、Christopher P. Wadsworth である。1978 年のメタ言語論文には Lockwood Morris と Malcolm Newey も名を連ねる。Larry Paulson と Gordon の回顧は、Stanford LCF から Edinburgh LCF、Cambridge LCF、HOL、Isabelle へ続く系譜を示す。Milner の中心的な着想を評価することと、ML やタクティックや対話型証明を一人の発明とすることは同じではない。

ML は当初 Meta Language、つまり証明手続きを記述する言語だった。多相型システムはその後、独立した大きな成果となった。Milner の 1978 年論文は意味論的・構文的な健全性を論じ、Edinburgh LCF で既に動いていた型推論を説明した。1991 年の ACM チューリング賞は LCF、ML、CCS を評価したが、共同開発の事実を消すものではない。

推論規則は既存 theorem から新しい theorem へ順向きに働く。タクティックは目標から部分目標へ逆向きに働く。validation が両者をつなぐ。tactical は順次適用、反復、選択などでタクティックを組み合わせるが、新たな公理にはならない。

抽象型が縮めるもの、縮めないもの

抽象データ型は内部表現を隠し、限られた操作だけを公開する。一般のコードは thm 値を保持して規則に渡せるが、内部を編集して別の値を捏造できない。型抽象がこの境界を守る。

その利点は審査範囲の縮小である。あらゆるタクティックではなく、比較的小さな公理と規則実装に注意を集中できる。探索コードが大きくなっても、受理権限を持つコードまで同じ割合で増える必要はない。

ただし「小さなカーネル」は「信頼不要」を意味しない。原始規則は選んだ論理に対して妥当でなければならない。ML 実装、コンパイラ、実行環境は抽象を保存しなければならない。危険な機能やハードウェア故障は前提を壊し得る。パーサや表示器が、保存された項とは別の式を利用者に見せる可能性もある。信頼の根は狭くなるだけで、消滅はしない。

カーネルの健全性と論理体系の無矛盾性も同義ではない。ある値が特定の関数だけで作られたという事実は生成履歴を述べるが、各関数が妥当な規則を表すことを独立に証明しない。また、モデル上の theorem は、そのモデルが現実の装置、制度、利用者の意図を正確に写したことまでは示さない。完全なカーネルでも、間違った形式的問いに完璧に答えられる。

validation は後払いの約束である

タクティックが部分目標を提示するとき、それらの theorem が元の目標に十分だと約束している。validation は後で、許可された規則によってその約束を履行する。画面から目標を消しただけでは証明にならない。

tactical が探索を合成するとき、validation も合成される。制御層は複雑になってよいが、受理の鎖は原始操作へ戻る。ログ、スクリプト、緑色の表示は活動の説明であって、受理された値と同じ権限を持たない。

HOL や Isabelle はこの考えを受け継いだが、同一設計ではない。Paulson は Isabelle の規則と証明状態が古典的 LCF とは異なる原理で表現されると説明する。proof term を保存する方式や証明書を外部検査する方式もある。Coq など型理論系の境界も別である。タクティックを使うという一点だけで LCF 型とは言えない。

出典と限界

本稿は歴史と設計の分析であり、現行証明器の監査やカーネル行数の測定ではない。最小で局所検証できる共通規則と将来の手法の自由を結び付ける部分は、Lu Heng の最小初期仕様の原則に触発された編集上の解釈であり、Milner の制度的見解として提示していない。