research_rewrite 設計

research_rewrite パッケージは、カーネルファーストの規律を手放さずに QED がどのように書き換えと簡約を提供できるかを探る。研究専用であり、同梱パッケージからは使われず、research/rewrite-simplify/ に記録されたレビューは、監査済みのベースラインで昇格させないことを決定した。このページでは、それが実装するモデルと、昇格に際して満たすべき制約を説明する。

設計目標

書き換えは部分項を等しい項に置き換える。LCF システムでは、そのような置き換えのすべてが等式の定理で正当化されなければならないので、書き換え器は実質的に定理 $\vdash t = t'$ の生成器である。プロトタイプは、QED のゴールに対して、小さく監査可能なウィットネスの集合でそれが可能かどうか、また後の段階が再検査できるようにステップを記録できるかどうかを検証する。

数学的背景

変換と合同

変換 (conversion) は項 $t$ を定理 $\Gamma \vdash t = t'$ に写す。大きな項の内部の位置で書き換えるには合同が必要である。$\Gamma \vdash l = r$ ならば、すべての文脈 $C[\cdot]$ について

$$\Gamma \vdash C[l] = C[r].$$

適用のみからなる文脈では、これは hole への経路に関する帰納法で、ステップごとに 1 回の MK_COMB によって従う。

$$\frac{\vdash f = f \quad \Gamma \vdash l = r}{\Gamma \vdash f\,l = f\,r}\;\textsf{MK\_COMB} \qquad \frac{\Gamma \vdash l = r \quad \vdash a = a}{\Gamma \vdash l\,a = r\,a}\;\textsf{MK\_COMB}$$

変化しない側は REFL が供給する。これは CombFun と CombArg のサイトステップの経路が生成するもので、サイトステップごとに 1 つの Congruence ステップとして記録される。抽象の下ではステップは ABS となり、束縛変数が $\Gamma$ に自由に現れないことが必要になる。ローカルな仮定をウィットネスとする場合、この副条件は成り立たないことがあり、プロトタイプは AbsBody サイトをサポートしない。

ウィットネス

焦点にある等式 $l = r$ は、4 種類のウィットネスのいずれかから得られる。

ウィットネス	定理	記録されるステップ
LocalEquality(h)	ASSUME による $\{l = r\} \vdash l = r$	ResolveWitness
ExplicitTheorem(th)	与えられた定理	ResolveWitness
CanonicalUnfold(k)	結合子の定義を引数に適用して β 正規化したもの	Unfold, BetaNormalize
BetaNormalization	REFL の後に BETA と TRANS のステップ	BetaNormalize

等式による右から左への書き換えは Symmetry を追加する。ローカルな等式による書き換えはその等式を仮定として持つので、その等式が仮定であるゴールでのみ有効である。チュートリアルが示すように、ローカルなしでリプレイすると失敗する。

書き換えを証明で使う

書き換えたゴールを元のゴールの証明に戻すには、$\Gamma \vdash C[l] = C[r]$ と $C[r]$ の証明が必要である。対称な等式との EQ_MP により、$C[l]$ が証明される。

$$\frac{\Gamma \vdash C[r] = C[l] \qquad \Delta \vdash C[r]}{\Gamma \cup \Delta \vdash C[l]}\;\textsf{EQ\_MP}$$

プロトタイプは等式を内部で構築するが公開せず、この最後のステップを実行するタクティクも無い。これが、同梱の経路に含まれない主な理由である。

設計判断

義務を記録し、再構築して検査する

選択。 書き換えは新しい結論と ReplayObligation を返す。これは、リクエスト、前後の結論、使用されたカーネルステップの種類からなる。research_validate_replay_obligation は、リクエストからカーネル規則ですべてのセグメントを再構築し、結果を比較して義務を検査する。

理由。 義務は、研究ラインの昇格ゲートが要求するとおり、保存・比較・レビューできる単純なデータである。検査は記録を信頼せず再構築で行うため、偽造された、または古い義務は拒否される。

正直な失敗

未対応のケースはすべて、理由とともに HonestFailure を返す。非ブールの結論、AbsBody サイト、定義の折りたたみ、β 展開、未知のローカル、焦点に一致しないウィットネス、ステップ上限の超過である。明示的な NoChange(どの規則も適用されなかったことを意味する)を除いて、黙った何もしない処理に退化するものは無い。

上限付きの簡約

research_simplify_term_concl は、展開、β 正規化、ユーザーのリクエストを不動点まで繰り返し、セグメント数が step_limit を超えるときは失敗して停止する。この上限により、停止性は規則集合ではなく設定の性質となる。

正しさと不変条件

• 権限なし。 このパッケージが構築するすべての等式は、カーネルと logic の関数から得られ、パッケージから外へ出る定理は無い。
• 検査可能な記録。 義務が検証を通るのは、与えられた状態、プレリュード、ローカルに対して、すべてのセグメントをそのリクエストから再構築でき、セグメントが before_concl から after_concl まで連鎖している場合に限る。
• 停止性。 簡約は高々 step_limit 個のセグメントを実行する。

却下した代替案

• 定理を直接返す。 プロトタイプが、研究プロセスが要求するレビューを経ずに、事実上のタクティクになってしまう。
• リネームによる束縛子の下での書き換え。 ABS の副条件の管理が必要であり、評価対象の範囲から外した。

境界

• 研究専用であり、同梱されず、他のどのパッケージからもインポートされず、定理スクリプトやコマンドラインツールからは到達できない。
• 抽象の下での書き換えも、定義の折りたたみも、β 展開も無い。
• 元のゴールの証明は無い。このパッケージは定理ではなく、項と義務を返す。
• このラインの権威ある状況は research/README.md と research/rewrite-simplify/ の文書にあり、このページではない。