parser 設計

parser パッケージは、テキストを構文木に、構文木をカーネルの項に変換する。信頼されず、意図的に守備範囲を狭くしている。表層記法を定め、ユーザーが見つけられる位置でエラーを報告し、ゴールを単純なデータとして上位に渡す。このページでは、文法、ローワリングの経路、タクティク層との境界を説明する。

設計目標

• 命題のゴールと証明スクリプトのために、小さく曖昧さのない記法を受け付ける。Unicode を正準形とし、ASCII 綴りは入力の便宜として扱う。
• 正規化後であっても、すべてのエラーをユーザーが書いたテキスト中のオフセットで報告する。
• カーネルの項へのローワリングは、elab の解決境界と logic の結合子ビルダーだけを通じて行い、パーサが名前や結合子の意味を決めることがないようにする。
• タクティク層より下にとどまる。ゴールを生成するが、証明状態は生成しない。

数学的背景

文法

項は次の文法に従う。ここで name は識別子であり、適用は並置である。

$$\begin{aligned} \mathit{term} &::= \mathit{term}\ \mathit{op}\ \mathit{term} \mid \neg\,\mathit{term} \mid \mathit{app} \\ \mathit{app} &::= \mathit{atom}^{+} \\ \mathit{atom} &::= \mathit{name} \mid (\,\mathit{term}\,) \\ \mathit{op} &::= {=} \mid {\wedge} \mid {\vee} \mid {\to} \end{aligned}$$

最初の生成規則の曖昧さは、優先順位と結合性で解決される。

演算子	優先順位	結合性	連鎖の読み方
=	40	なし	a = b = c はエラーである
∧	30	左	a ∧ b ∧ c は (a ∧ b) ∧ c である
∨	20	左	a ∨ b ∨ c は (a ∨ b) ∨ c である
->	15	右	a -> b -> c は a -> (b -> c) である

ゴールはシーケント $h_1, \dots, h_n \vdash c$ であり、forall (x : A), ... で始まってもよい。定理スクリプトは、束縛子を持つヘッダと、ステップの本体を加える。split、left、right の後には、任意で { ... } の分岐ブロックを置ける。

演算子順位解析

中置の連鎖 $t_0\ o_1\ t_1\ \dots\ o_n\ t_n$ は演算子スタックで解析される。新しい演算子 $o$ が到着したとき、スタックの先頭に演算子 $o'$ があれば、パーサが先に $o'$ を簡約するのは次の場合に限る。

$$\mathrm{prec}(o') > \mathrm{prec}(o) \;\lor\; \big(\mathrm{prec}(o') = \mathrm{prec}(o) \land \text{both are left-associative}\big),$$

は、優先順位が低い場合、または両方が右結合の場合に $o'$ を保持し、優先順位が等しくどちらかが非結合の場合は NonAssocChain で失敗する。各演算子は 1 回ずつ push と pop されるので、アルゴリズムは連鎖の長さに対して線形であり、表を尊重する唯一の木を生成する。

ローワリング

ローワリングは構文をカーネルの項に写す。

$$\begin{aligned} [\![x]\!]_\Gamma &= x{:}\tau &&\text{if } (x:\tau) \in \Gamma \\ [\![c]\!]_\Gamma &= c^{\iota}{:}\sigma &&\text{if } c \text{ is declared with identity } \iota \text{ and schema } \sigma \\ [\![a\ b]\!]_\Gamma &= [\![a]\!]_\Gamma\,[\![b]\!]_\Gamma \\ [\![a = b]\!]_\Gamma &= ([\![a]\!]_\Gamma = [\![b]\!]_\Gamma) \\ [\![a \wedge b]\!]_\Gamma &= \texttt{prop\_mk\_and}([\![a]\!]_\Gamma, [\![b]\!]_\Gamma) &&\text{and likewise for } \vee, \to, \neg \end{aligned}$$

名前は elab を通る(ローカルが定数より先、同一性は固定)。結合子は logic のビルダーを通り、ビルダーは引数が命題であることを検査する。ゴール forall (x : A), body は、$x{:}A$ を $\Gamma$ に加えて body をローワリングすることで処理される。量化子は取り除かれ、$x$ はゴール中で自由のままとなる。これは定理ヘッダの束縛子 (x : A) とまったく同じである。自由変数を持つ定理は、その変数のすべての値について成り立つ。INST が同じ型の任意の項を代入できるからであり、したがって $x$ が自由な $\vdash \mathit{body}$ は、量化された主張の HOL での読み方である。

設計判断

先に正規化し、オフセット対応を保持する

問題。 ユーザーは \and、|-、余分な空白を入力する。エラーメッセージは、ユーザーが入力したものを指さなければならない。

選択。 normalize_parser_input は入力を一度だけ正準テキストに書き換え、各文字について元のオフセットを記録する。レキサとパーサは正準テキストで動作し、すべてのエラーのオフセットとスパンは、パッケージを出る前に元に戻して対応づけられる。

理由。 正準形が 1 つであることで文法が小さく保たれ、対応表によって診断が正直なものになる。古い ASCII 綴りの /\ と \/ はもう受け付けないので、結合子ごとに ASCII 綴りは 1 つである。

生の解析とローワリングの分離

問題。 ローワリングにはカーネル状態が必要である。prover のようなツールは、状態が存在する前にスクリプトの構造を必要とする。たとえばステップの位置を報告するためである。

選択。 すべての構文要素に、位置付きで状態を持たない構文木を返す _raw パーサと、状態を受け取るローワリング関数を用意する。定理スクリプトは生の解析のみを行い、ゴールのローワリングは prover 自身が行う。

理由。 prover は再解析せずに、失敗したステップをそのスパンとインデックスで指摘できる。パーサは証明の実行から独立したままである。

パーサ所有のゴール

問題。 parse_goal の戻り値の型として自然なのは tactics パッケージの Goal だが、そうするとパーサが tactics 層に依存し、そこでの変更が構文に波及してしまう。

選択。 パーサは独自の ParsedGoal を返し、prover が @tactics.mk_goal で変換する。

理由。 これにより、コードガバナンスが要求するとおり、層の順序 kernel → logic/elab → parser → tactics → prover が非循環に保たれ、パーサは誤ってでも証明オブジェクトを構築できなくなる。

結合子は構築するもので、検索するものではない

結合子は logic のビルダーで基底項にローワリングされる。パーサは and や imp という名前の定数の存在を要求しない。これにより、すべての結合子はどの状態でも同じ意味を持ち、命題でない引数をタクティクに任せず、ローワリング時に Logic(NotBoolTerm) として報告できる。

量化子はゴールの糖衣としてのみ

生の forall はゴールの先頭でのみ受け付け、他の場所では受け付けない。項の中の一般的な束縛子には、量化子定数とその規則が logic 層に必要だが、同梱サブセットにはそれがない。ゴールの先頭、つまり定理ヘッダの束縛子と同じ意味になる場所に限ることで、表層は正直なまま保たれる。解析できるものは既存の仕組みで証明でき、項の内部の forall は明確な UnexpectedToken で失敗する。

すべてのステップに位置を

スクリプトの各ステップは、そのインデックス、分岐パス、スパンを記録する。これらは、prover と CLI が失敗時や未完了の証明に対して報告するフィールドであり、ユーザーは素っ気ないエラーではなく、step: 3、branch: 1 とソーステキストを目にする。

正しさと不変条件

• 権限なし。 パーサは項を構築し、parse_def_function を通じてカーネルの DefOK ゲートを呼び出す。これ以外の経路で定理を生成することはない。
• オフセットは生の入力を指す。 すべての ParseError と SourceSpan について、オフセットは元の文字列中の位置であり、$[0, \text{raw length}]$ の範囲内にある。
• 決定的な構造。 優先順位表は、受理されるすべての連鎖に対して 1 つの木を定める。= の連鎖は推測せず拒否する。
• ローカルが定数より先。 束縛子または let のローカルは同名の定数を覆い隠す。これは elab およびタクティク層と一貫している。
• ステップ番号。 step_index は、分岐ブロック内のステップを含め、スクリプト全体でソース順に 1 から数える。そのため、診断中の番号はスクリプトの読む順序と一致する。

却下した代替案

• パーサジェネレータ。 文法は小さいので、手書きのレキサと演算子順位パーサのほうが短く、エラーオフセットも良くなり、ビルドステップも不要である。
• タクティクのオブジェクトを返す。 上述のとおり、層構造のために却下した。
• 型付き束縛子、型注釈、あらゆる場所の量化子を持つ完全な HOL 項構文。 タクティク層が証明できないスクリプトを招いてしまう。構文は証明の仕組みとともにのみ拡張する。
• 暗黙の T と F。 これらは状態を通じて解決される通常の定数名である。したがって、プレリュードが無い場合、スクリプトは別の意味を黙って使うのではなく、目に見える形で失敗する。

境界

• 型推論は無い。束縛子と let の型は明示的に書く。項の内部に型注釈は無い。
• 項の内部に forall も exists も、λ 抽象の構文も、ユーザー定義の演算子も無い。
• 整形出力は無い。項はカーネルの構造的プリンタで描画される。
• 証明の実行は無い。ステップは SynTacticStep の値に解析され、tactics パッケージが実行し、prover がスケジュールする。