Luna Flow
日本語

prover 設計

prover パッケージは、定理スクリプトを 3 つの結果、すなわちカーネルの定理、構造化された失敗、未完了の証明のいずれかに変える。このページでは、その結果モデル、tactics 層の上で分岐ブロックがどのようにスケジュールされるか、そしてこのパッケージがフェイルクローズである理由を説明する。述べられたゴールに対するカーネルの定理なしに、成功を報告できる経路は存在しない。

設計目標

  • 定理スクリプトをエンドツーエンドで実行する。解析、プレリュードのインストール、ゴールのローワリング、ステップの実行、分岐ブロックのスケジュールを行う。
  • 証明が止まった場所を正確に示す。定理、ステップ番号、分岐パス、ソーステキスト、現在のゴールとローカルな仮定である。
  • カーネルの Thm 以外を証明として提示しない。未対応の入力、失敗するステップ、hole は、そのまま報告される。
  • テストが実行しマニュアルが引用するスクリプトのコーパスを公開することで、ドキュメントを正直に保つ。

数学的背景

和型としての結果

ゴールが Γ⊢c\Gamma \vdash c であるスクリプトに対する結果は次のとおりである。

run(script)∈ThmΓ⊢c⏟Proved  +  Failure⏟Failed  +  Goal×Position⏟Unfinished\mathsf{run}(\mathit{script}) \in \underbrace{\mathsf{Thm}_{\Gamma \vdash c}}_{\texttt{Proved}} \;+\; \underbrace{\mathsf{Failure}}_{\texttt{Failed}} \;+\; \underbrace{\mathsf{Goal} \times \mathsf{Position}}_{\texttt{Unfinished}}

3 つの場合は互いに排他的で、定理を持つのは最初のものだけである。特に、未完了の証明は余分な仮定を持つ定理ではない。それは hole が表すゴール Γ′⊢c′\Gamma' \vdash c' を含む報告である。hole を仮定に変えると定理 Γ∪{c′}⊢c\Gamma \cup \{c'\} \vdash c が得られるが、これはユーザーが求めた主張とは別のものである。

入れ子の証明としての分岐ブロック

split { s₁ } { s₂ } のように分岐ブロックが続くステップは、現在のゴール GG に対してステップを実行し、サブゴール G1,G2G_1, G_2 を生成する。各ブロック sis_i は GiG_i の独立した証明となる。

s1 proves G1s2 proves G2split {s1} {s2} proves G\frac{s_1 \text{ proves } G_1 \qquad s_2 \text{ proves } G_2}{\texttt{split}\,\{s_1\}\,\{s_2\} \text{ proves } G}

prover は GiG_i を根とする新しい証明状態(ps_isolate_pending_at)で sis_i を実行し、その状態から GiG_i の定理 tit_i を得て、親の状態で tit_i を使って GiG_i を閉じる。親の split の正当化は有効であるから、これらの定理は合成されて GG の定理となる。これは tactics 設計で説明した正当化の LCF 的な合成を、一段上で適用したものである。

設計判断

Result ではなく三者択一の結果

問題。 Result[Thm, Error] では、未完了の証明を、偽である定理か、「誤り」と「まだ終わっていない」の違いが失われるエラーのどちらかにせざるを得ない。

選択。 ProverRunResult は 3 つのコンストラクタを持つ。prove_theorem_script は、定理だけを求める呼び出し側のために引き続き Result を返すが、そのエラー側の ProverScriptError は失敗と未完了の証明を区別して保持する。

理由。 エディタとコマンドラインツールはこれらの場合を別々に扱う。エラーはユーザーを止め、未完了の証明は取り組むべきゴールを伴う警告である。仕様は、hole が定理の権限を生まないことを要求しており、型によってそれを誤ることは不可能になっている。

診断は位置と文脈を持つ

すべての失敗および未完了の報告は、定理名、ステップのインデックス、分岐パス、ステップのスパンとソーステキスト、その時点のゴールとローカルを、すべて生の入力に基づいて記録する。cmd パッケージはこれらのフィールドをそのまま出力する。代償は幅の広いレコードであるが、利点として、どの利用側も結果を説明するために何かを再実行する必要がない。

分岐ブロックの分離されたフレーム

問題。 分岐の本体を親の状態の内部で実行すると、ある分岐の失敗が兄弟分岐の管理情報を乱しうるし、報告される分岐パスがスケジュールの細部に依存してしまう。

選択。 各分岐の本体は、親のリプレイ文脈を持たず、1 つの保留中ゴールから作られた独自の証明状態で実行される。本体が終了すると、ps_close_frame がそのゴールの定理を返さなければならず、親はそれでゴールを閉じる。ゴールを残したままの本体は、その分岐ステップでの失敗となる。

理由。 こうして各ブロックは、ブロック構文が示唆するとおり、そのサブゴールの独立した証明となり、ステップのインデックスと分岐パスは、入れ子に関わらず読む順序で割り当てられる。

不正な定理の後もファイルは継続する

問題。 複数の定理を含むファイルは、最初の 1 つだけでなく、すべての問題を報告すべきである。

選択。 prove_theorem_file_results_detailed はすべての定理を実行し、それぞれについて 1 項目を返す。ファイル全体が失敗するのは、解析できないファイルか、プレリュードのインストールに失敗した場合だけである。証明済みの定理は状態に追加されない。後の定理が名前で前の定理を引用することはできない。

理由。 すべての定理を報告することが、CLI の利用者の期待である。定理を状態に追加しないことで、ユーザーマニュアルが述べるように、引用できる名前のカタログが固定される。定理環境は同梱サブセットに含まれない。

プレリュードはオプションでインストールされる

auto_install_prelude が(既定の)オンの場合、prover は実行前に命題のプレリュードをインストールする。そのためスクリプトは、状態を準備せずに T、F、カタログの定理を使える。特定の状態を必要とするテストは、これをオフにして自分で定数をインストールする。

コーパスはコードである

マニュアルとこれらのページが引用するスクリプトは corpus.mbt の値である。肯定的、否定的、未完了、量化子のケースがあり、それぞれに識別子と、それが示す能力または失敗がある。さらにケースからドキュメントのアンカーへの対応表がある。テストはすべてのケースを実行して対応を検査するので、公開された例がコードの挙動からずれることはない。適合性ガイドは、これを公開例の規則としている。

正しさと不変条件

  • フェイルクローズ。 Proved は 1 箇所でのみ構築される。ps_qed の結果からであり、ps_qed は tactics 層がルートのゴールに照らして検査した後にのみ定理を返す。それ以外のすべての経路は Failed または Unfinished を返す。
  • 権限なし。 このパッケージはパーサ、tactics 層、カーネル状態関数を呼び出す。自分では定理を構築しない。
  • hole は漏れない。 hole はスクリプトを ps_qed の前に止める。未完了の状態を定理に変えるコード経路は存在しない。
  • 位置は生の入力。 報告中のオフセットとスパンは、パーサのオフセット対応を通じて、与えられたとおりの入力文字列を指す。
  • 順序。 ファイル報告の項目はソース順であり、ステップのインデックスは分岐ブロックをまたいで読む順序で数える。

却下した代替案

  • 失敗に例外を使う。 Result はすべての結果を型に見える形で保ち、CLI がそれらをすべて一様に描画できるようにする。
  • hole を仮定として扱う。 上で示したとおり、結果の定理がゴールとは別のことを述べるため却下した。
  • 分岐本体の共有状態。 実装は単純になるが、兄弟分岐を結合させ、責任の所在がスケジュールに依存してしまう。
  • ファイル全体にわたる定理環境。 後の定理が前の定理を引用できるようにするには、仕様がまだ定めていない命名とリプレイの規律が必要になる。それまでは、カタログが名前の唯一の情報源である。

境界

  • prover はステップを追加しない。ステップの集合は tactics のものに hole を加えたものである。
  • ファイルの読み込みや出力は行わない。それは cmd パッケージの役割である。
  • 証明探索、書き換え、簡約は行わない。research_rewrite の研究用プロトタイプは組み込まれていない。
  • 証明済みの定理を保存せず、スクリプト同士が互いを参照することも許さない。