kernel 設計

カーネルは QED の信頼計算基盤であり、定理が信頼されるために正しくなければならない唯一のコードである。このページでは、カーネルが実装する論理、そのインターフェースがなぜ他のすべてのパッケージを信頼不要にするのか、そして形式仕様の健全性の議論が src/kernel のコードにどう対応するかを説明する。

設計目標

定理証明器の信頼性は、定理を作れるコードの信頼性に等しい。QED は、Milner の Edinburgh LCF と、その後継である HOL Light や HOL4 の LCF 方式に従う。¹1 R. Milner, “LCF: A way of doing proofs with a machine”, 1979; J. Harrison, “HOL Light: An overview”, TPHOLs 2009. QED は基本規則の選択において HOL Light に最も近く従っている。 定理は抽象型の値であり、その唯一のコンストラクタは論理の推論規則である。パーサ、タクティク、証明探索、コマンドラインツールにはいくらバグがあってもよい。そこでのバグは証明を失敗させるだけで、偽の主張を定理にすることは決してない。

したがってカーネルには三つの目標がある。

• 小さく固定された規則の集合で高階論理（HOL）を実装し、人手で読み、検査できるようにする。
• 定理型をパッケージの外から偽造できないようにする。
• 理論は、保存的であることが証明できる拡大によってのみ成長させ、それぞれを監査のために記録する。

数学的背景

型

型は、型変数と、アリティが固定された型コンストラクタから生成される。

$$\tau ::= \alpha \mid c(\tau_1, \dots, \tau_n)$$

コンストラクタ bool（アリティ 0）、fun（アリティ 2、$\sigma \to \tau$ と書く）、ind（アリティ 0）は組み込みである。型代入 $\theta$ は型変数を型に写し、準同型的に作用する。型 $\tau$ がスキーマ $\sigma$ のインスタンスであるとは、ある $\theta$ について $\tau = \sigma\theta$ であることをいい、$\tau \preceq \sigma$ と書く。ty_is_instance_of は一階のマッチングによってこれを判定する。

項

項は、定数のシグネチャ上の単純型付き λ 計算のものである。

$$t ::= x{:}\tau \mid c{:}\tau \mid t\,t \mid \lambda (x{:}\tau).\,t$$

変数は名前と型の組である。定数の出現 $c{:}\tau$ が正当であるのは、$c$ がスキーマ $\sigma$ で宣言されており、$\tau \preceq \sigma$ であるときである。型付けの判断は通常のものである。

$$\frac{}{x{:}\tau : \tau} \qquad \frac{}{c{:}\tau : \tau} \qquad \frac{f : \sigma \to \tau \quad u : \sigma}{f\,u : \tau} \qquad \frac{t : \tau}{\lambda (x{:}\sigma).\,t : \sigma \to \tau}$$

型付けは構文主導であり、型付け可能な項はちょうど一つの型をもつため、type_of は HolType? への全域関数であり、線形時間で動作する。

コアの論理定数は、等号と選択のみである。

$$= \;:\; \alpha \to \alpha \to \mathit{bool} \qquad @ \;:\; (\alpha \to \mathit{bool}) \to \alpha$$

他のすべての結合子は、この二つによる定義であり、logic パッケージが DefOK ゲートを通して行う。logic の設計にその定義がある。結合子をカーネルの外に置くことで、カーネルは小さく保たれる。カーネルは $\wedge$ も $\to$ も知らない。

α 同値と de Bruijn 項

二つの項が α 同値であるとは、束縛変数の名前だけが異なることをいう。$\lambda x.\,x \equiv_\alpha \lambda y.\,y$ である。HOL の規則は束縛名に依存してはならないため、カーネルは名前なしの表現で動作する。de Bruijn 項は、各束縛出現を、それとその束縛子との間にある束縛子の数で置き換える。²2 N. G. de Bruijn, “Lambda calculus notation with nameless dummies”, Indagationes Mathematicae 34, 1972.

$$\lambda x.\,\lambda y.\,x \;\mapsto\; \lambda.\,\lambda.\,\underline{1} \qquad \lambda y.\,\lambda x.\,y \;\mapsto\; \lambda.\,\lambda.\,\underline{1}$$

変換 $\lceil\cdot\rceil$（to_db_term）は $t_1 \equiv_\alpha t_2 \iff \lceil t_1 \rceil = \lceil t_2 \rceil$ を満たすので、α 同値は構造的な等しさ（db_term_eq）になる。QED の de Bruijn 項は型付きである。束縛出現と束縛子は型を保つ。ここから二つの帰結が得られる。異なる型についての抽象は決して潰れない。$\sigma \ne \tau$ のとき $\lceil \lambda (x{:}\sigma).\,x \rceil \ne \lceil \lambda (x{:}\tau).\,x \rceil$ だからである。そして、$\lambda (x{:}A).\,(x{:}B)$ のように、内側の変数が束縛子と同じ名前で別の型をもつ項には、変換がまったく存在しない。to_db_term は None を返し、すべての規則は BoundaryFailure を報告する。HOL Light は内側の x を別の自由変数として読むが、QED はその項を拒否する。束縛子の名前が常に一つの変数を指すようにするためである。

代入と β 簡約

$t$ の中の $\ge c$ であるすべてのインデックスに $d$ を加えるシフトを $\uparrow^d_c\,t$ と書き、インデックス $j$ を $s$ で置き換える操作（束縛子の下を通るとき $s$ をシフトする）を $t[j \mapsto s]$ と書く。

$$\begin{aligned} \uparrow^d_c \underline{k} &= \underline{k} \text{ if } k < c, \quad \underline{k+d} \text{ otherwise} \\ \uparrow^d_c (\lambda.\,t) &= \lambda.\,\uparrow^d_{c+1} t \\ \underline{k}[j \mapsto s] &= s \text{ if } k = j, \quad \underline{k} \text{ otherwise} \\ (\lambda.\,t)[j \mapsto s] &= \lambda.\,\big(t[j{+}1 \mapsto \uparrow^1_0 s]\big) \end{aligned}$$

シフトと置換は適用に対して準同型的に作用し、自由変数と定数には触れない。このとき $(\lambda.\,t)\,u$ の β 縮約は次のとおりである。

$$\beta\big((\lambda.\,t)\,u\big) = \uparrow^{-1}_0\big(t[0 \mapsto \uparrow^1_0 u]\big).$$

これが捕獲を起こさない理由。$t$ の内部では、インデックス $0$ は取り除かれる束縛子を指し、$\ge 1$ のインデックスはその外側の束縛子を指す。$u$ を挿入する前に一つ上にシフトすることで、$u$ のすべての自由インデックスは、これから消える束縛子を飛び越える。置換は内側の束縛子ごとに再びシフトするので、$u$ のインデックスは常に、実際にそれを囲む束縛子を数える。置換後にはインデックス $0$ の出現は残らない。どれもが置換されたからである。したがって最後の一つ下げるシフトが定義でき、取り除かれた束縛子の先を指していたインデックスを元の値に戻す。名前付きの対応物は捕獲回避代入 $t[u/x]$ であり、仕様はこの対応を補題「Well-Scoped Beta Contraction Safety」として述べている。カーネルはすべてのインデックスをオーバーフロー検査付きで計算し、ラップアラウンドする代わりに CapacityExceeded を報告する。

自由変数に対する代入（db_subst_free_parallel、INST で使う）はより単純である。自由変数は名前であってインデックスではなく、挿入される項は現在の束縛子の深さだけシフトされる。緩いインデックスをもたない項では、これは何もしない。捕獲は構成上不可能であり、INST に名前の付け替えのステップが要らないのはそのためである。

シーケントと定理

定理はシーケント $\Gamma \vdash p$ である。すなわち、命題（型 bool の項）の有限集合 $\Gamma$ と、命題 $p$ からなる。カーネルは $\Gamma$ と $p$ を de Bruijn 項として保持するので、$\Gamma$ は文字どおり α 同値類の集合である。すでにある仮定と α 同値な仮定を挿入しても何も起こらない（db_hyps_union）。

意図される意味は、HOL の標準的な意味論である。型は空でない集合を表し、$\mathit{bool}$ は $\{\top, \bot\}$ を表し、$\sigma \to \tau$ は関数全体の集合を表し、$=$ は同一性を表し、$@$ は選択関数を表す。シーケントが妥当であるとは、$\Gamma$ のすべてを真にするあらゆるモデルと自由変数のあらゆる付値が、$p$ をも真にすることをいう。

設計判断

定理型は抽象的である

問題。 カーネルの外のコードが Thm を構築できるなら、そのコードのバグや近道によって偽の定理が作られうる。

選択肢。 LCF 方式の抽象型。別個の検査器で検査される証明項（Coq や Lean の方式）。あるいは「検証済み」フラグを付けた信頼レコード。

選択。 Thm はインターフェースで type Thm と宣言され、フィールドは非公開で、公開コンストラクタをもたない。Thm を返す関数は、11 個の規則関数（refl_checked から inst_checked まで、および add_assum_checked）、ゲート ks_define_const_thm と ks_specify_const、保存された定理の読み出し関数 ks_definition_theorem、ks_typedef_contract、ks_ind_infinity_axiom、そして検査した後に定数の同一性を記録して引数を返す thm_bind_const_ids だけである。MoonBit はこれをコンパイル時に強制する。

理由。 抽象型により、信頼基盤はちょうどこのパッケージとなる。証明項を使うと、第二の信頼コンポーネントである検査器と、定理ごとの大きな証明オブジェクトが加わる。QED の仕様は LCF の規律を規範とし（義務「Interface safety」）、インターフェースファイルの検査によってそれを確認する。

HOL Light の基本規則

問題。 すべての定理を生成する規則を選ぶ。

選択。 HOL Light の 10 個の規則。等号を唯一の基本結合子とする HOL の、最小の標準的な基底である。

$$\begin{gathered} \frac{}{\vdash t = t}\,\textsf{REFL} \qquad \frac{}{\{p\} \vdash p}\,\textsf{ASSUME} \qquad \frac{\Gamma \vdash s = t \quad \Delta \vdash t = u}{\Gamma \cup \Delta \vdash s = u}\,\textsf{TRANS} \\[1ex] \frac{\Gamma \vdash f = g \quad \Delta \vdash x = y}{\Gamma \cup \Delta \vdash f\,x = g\,y}\,\textsf{MK\_COMB} \qquad \frac{\Gamma \vdash s = t \quad x \notin \mathrm{FV}(\Gamma)}{\Gamma \vdash \lambda x.\,s = \lambda x.\,t}\,\textsf{ABS} \qquad \frac{}{\vdash (\lambda x.\,t)\,u = t[u/x]}\,\textsf{BETA} \\[1ex] \frac{\Gamma \vdash p = q \quad \Delta \vdash p}{\Gamma \cup \Delta \vdash q}\,\textsf{EQ\_MP} \qquad \frac{\Gamma \vdash p \quad \Delta \vdash q}{(\Gamma \setminus \{q\}) \cup (\Delta \setminus \{p\}) \vdash p = q}\,\textsf{DEDUCT\_ANTISYM\_RULE} \\[1ex] \frac{\Gamma \vdash p}{\Gamma\theta \vdash p\theta}\,\textsf{INST\_TYPE} \qquad \frac{\Gamma \vdash p}{\Gamma\sigma \vdash p\sigma}\,\textsf{INST} \end{gathered}$$

前提のマッチング（TRANS の中間項、EQ_MP の前件）は α 同値の範囲で行われ、定数の同一性は無視する（db_term_logical_eq）。両方の定理がすでに現在の状態に対して検査済みだからである。

一つの相違点がある。QED の BETA は任意のリデックス $(\lambda x.\,t)\,u$ を受け付けるが、HOL Light の基本 BETA は $(\lambda x.\,t)\,x$ だけを受け付け、一般形は INST で導出する。一般形は HOL Light では導出規則なので、これによって定理が増えることはない。カーネルから名前の付け替えのステップを省くことができ、これはまさに仕様に述べられた規則である。

HOL であって依存型ではない理由。 HOL には、単純でよく理解された集合論的意味論があり、HOL Light ではカーネルが数百行であり、定義と組み合わせれば 10 個の規則で数学に十分であることを示す数十年の経験がある。カーネルは、その健全性の議論を全文読める程度に小さく保たれる。それがカーネルファーストの設計の要点である。

弱化はネイティブに提供される

add_assum_checked は弱化を実装する。$\Gamma \vdash p$ から $\Gamma \cup \{q\} \vdash p$ が得られる。これは 10 個の規則の一つではなく、仕様にも載っていないが、導出規則であるため、定理は増えない。

$$\begin{aligned} &1.\;\; \{q\} \vdash q && \textsf{ASSUME} \\ &2.\;\; \Gamma \vdash p && \text{premise} \\ &3.\;\; (\{q\} \setminus \{p\}) \cup (\Gamma \setminus \{q\}) \vdash q = p && \textsf{DEDUCT\_ANTISYM\_RULE}(1, 2) \\ &4.\;\; (\{q\} \setminus \{p\}) \cup (\Gamma \setminus \{q\}) \cup \{q\} \vdash p && \textsf{EQ\_MP}(3, 1) \end{aligned}$$

4 行目の仮定集合は $\Gamma \cup \{q\}$ である。$\{q\} \setminus \{p\}$ の部分は $\{q\}$ に含まれ、$(\Gamma \setminus \{q\}) \cup \{q\} = \Gamma \cup \{q\}$ だからである。この導出は、$q \equiv_\alpha p$ であるか、$q \in \Gamma$ であるかによらず成り立つ。ネイティブ規則は、logic パッケージのリプレイが仮定集合を正確に一致させるために使う近道である。

de Bruijn コアの上の名前付き境界

問題。 ユーザーとフロントエンドは名前付きの項で考えるが、規則は名前に依存してはならない。

選択肢。 明示的な名前の付け替えをもつ名前付き項（HOL Light）。局所無名項。あらゆる箇所で de Bruijn 項。

選択。 インターフェースは名前付きの Term 値を受け取って返す。各規則は入力を to_db_term で変換し、DbTerm 上で動作し、呼び出し側が仮定や結論を求めたときにのみ from_db_term で戻す。変換の失敗は、導出ではなく BoundaryFailure というエラーである。

理由。 α 同値が等しさになり、代入は新しい名前を必要とせず、仮定集合は自然に α 同値類の集合になる。代償として、定理から読み戻した項には生成された束縛名（_b0、_b1、…）が付くため、呼び出し側は term_alpha_eq で比較する。仕様は、この境界を正当化する可換図式を証明している。ローワリングし、de Bruijn 規則を実行して持ち上げた結果は、名前付き規則を実行した結果と α 同値になる。

すべての規則は状態に対して検査される

問題。 定数はスコープ内で宣言され、隠蔽されうる。あるスコープで証明された定数 c についての定理は、内側のスコープが別の c を宣言した後に再利用されてはならない。

選択。 すべての規則は KernelState を受け取り、前提と結果に対して ensure_thm_admissible を実行する。定理は、それが言及する各定数の同一性（ConstId）を記録する。定理がある状態で許容されるのは、記録された各同一性が、状態がその名前を解決した先のものと一致し、各定数の出現が宣言されたスキーマのインスタンスであり、各型が認められたコンストラクタのみを使い、定義定理が依然としてその定義と一致するときである。

理由。 名前の検索はスコープが push・pop されると変わるが、記録された同一性は変わらない。同一性を凍結することで、解決はスコープの変更に対して安定になり（仕様の「Resolution Freeze」定理）、検査によって、古くなった定理は黙って意味が変わる代わりに InvalidInstantiation の失敗になる。チュートリアルでは、隠蔽するスコープの内側では拒否され、スコープを pop すると再び受け入れられる定理を示している。

拡大はゲートを通る

理論は三つの方法で成長し、それぞれ、副条件を検査して ExtensionCert を追加するゲートで守られている。

DefOK、定数定義。 ks_define_const(c, \tau, t) は定数 $c : \tau$ と定理 $\vdash c = t$ を追加する。各副条件は、保存性を壊す既知の方法を排除する。

条件	エラー	防ぐ反例
$t$ は閉じている	DefinitionNotClosed	$c = x$ は $\vdash c = x$ を与え、INST により $\vdash c = y$ が、したがって任意の $x, y$ について $\vdash x = y$ が得られてしまう。
$c$ は、以前の定義を経由してであっても $t$ に現れない	DefinitionIsCyclic	$c = \neg c$ は $\vdash c = \neg c$ を与え、矛盾となる。
$\mathrm{tyvars}(t) \subseteq \mathrm{tyvars}(\tau)$	GhostTypeVariable	$c : \mathit{bool}$ に対する $c = (\forall x{:}\alpha.\,\forall y{:}\alpha.\,x = y)$ は、$\alpha = \mathit{unit}$ では真で $\alpha = \mathit{bool}$ では偽だが、どちらのインスタンスも同じ定数 $c$ である。
$c$ は fresh である	DefinitionAlreadyExists	一つの名前の二つの定義は $\vdash c = t_1$ と $\vdash c = t_2$ を与え、したがって $\vdash t_1 = t_2$ となる。

これらの条件のもとで、定義は保存的である。$c$ のすべての出現を $t$ で置き換えると、拡大された理論のそれぞれの証明は古い理論の証明に写り、$c$ に言及しない定理は自分自身に写る。仕様はこれを「Definition-level conservativity」として証明している。

TypeDefOK、型定義。 ks_register_type_definition は、定理 $\vdash P\,w$ が与えられたとき、$\{x : \rho \mid P\,x\}$ と全単射をなす型 $\kappa(\bar\alpha)$ を認める。ウィットネスが重要なのは、HOL の型が空でない集合を表すからである。空の述語で定義された型にはモデルがなく、空の型に公理 $\vdash \mathit{abs}(\mathit{rep}\,a) = a$ を適用すると理論が矛盾してしまう。このゲートは、DefOK が幽霊型変数を禁じるのと同じ理由から、述語の型変数がパラメータ $\bar\alpha$ に含まれることを要求し、三つの契約定理を返す。

$$\vdash \mathit{abs}(\mathit{rep}\,a) = a \qquad \vdash P(\mathit{rep}\,a) \qquad P\,r \vdash \mathit{rep}(\mathit{abs}\,r) = r$$

最初の二つは、$\mathit{rep}$ が単射であり、その像が $P$ の内側にあることを述べる。三つ目は、$P$ のすべての元が像に含まれることを述べる。これらを合わせると、HOL Light による型の全単射の特徴づけとなり、同値 $P\,r = (\mathit{rep}(\mathit{abs}\,r) = r)$ を二つの向きに分けたものになる。

SpecOK、定数仕様。 ks_specify_const は、$\vdash P\,w$ が与えられたとき、性質 $\vdash P\,c$ をもつ $c$ を導入する。これは新しい基本ではない。DefOK を通して $c = @P$ を定義し、選択公理から従う $\vdash P\,c$ を返す。

$$P\,x \;\to\; P(@P)$$

を $x = w$ でインスタンス化したものである。拡大が定義であるため、その保存性は DefOK の保存性から従う。状態は DefOK と SpecOK の両方の証明書を記録する。

無限性のアンカー。 HOL が算術のために必要とするのは無限型である。ks_register_ind_infinity_axiom は、この役割を果たす ind についての定理を記録するが、すでに存在する定理しか受け付けない。これは、定理を追加することなく、仕様のモデルクラス制限に印を付けるものである。

例外ではなく結果

カーネルのすべての関数は Result または Option を返し、不正な入力で中断するものはない。適用できない規則は、LogicError または SigError のコンストラクタでその理由を述べ、呼び出し側が対処を決める。これがフロントエンドをフェイルクローズにするものである。tactics と prover パッケージはこれらの値を構造化された診断に変換し、失敗した規則を定理に変える経路は存在しない。

正しさと不変条件

健全性がカーネルに帰着する理由

定理の値が健全であるとは、そのシーケントが現在の理論のあらゆるモデルで妥当であることをいう。議論は三つのステップからなる。

1. すべての規則は妥当性を保存する。 各基本規則について、妥当な前提から妥当な結論が得られる。二つの場合でその型を示す。

ABS。$M$ をモデルとし、$v$ を $\Gamma$ を満たす付値とする。$x \notin \mathrm{FV}(\Gamma)$ なので、すべての付値 $v[x \mapsto a]$ も $\Gamma$ を満たす。したがって前提の妥当性により、すべての $a$ について $[\![s]\!]_{v[x \mapsto a]} = [\![t]\!]_{v[x \mapsto a]}$ である。よって

$$[\![\lambda x.\,s]\!]_v = \big(a \mapsto [\![s]\!]_{v[x\mapsto a]}\big) = \big(a \mapsto [\![t]\!]_{v[x\mapsto a]}\big) = [\![\lambda x.\,t]\!]_v$$

が標準モデルでの関数の外延性により成り立つ。副条件がなければ、「すべての $v[x \mapsto a]$ が $\Gamma$ を満たす」というステップは失敗する。$\{x = 0\} \vdash x = 0$ から $\{x = 0\} \vdash (\lambda x.\,x) = (\lambda x.\,0)$ が導けてしまうが、これは $x = 0$ が成り立つときはいつでも偽である。

DEDUCT_ANTISYM_RULE。$v$ が $(\Gamma \setminus \{q\}) \cup (\Delta \setminus \{p\})$ を満たすとする。$[\![p]\!]_v = \top$ ならば、$v$ は $\Delta$ を満たし（$\Delta$ から取り除かれた可能性のある仮定は $p$ だけである）、したがって $[\![q]\!]_v = \top$ である。対称に、$[\![q]\!]_v = \top$ ならば $[\![p]\!]_v = \top$ である。互いに含意する二つの真偽値は等しいので、$[\![p = q]\!]_v = \top$ である。

残りの規則も同様に従う。REFL と TRANS は同一性の反射律と推移律から、MK_COMB は適用の合同性から、BETA は代入補題 $[\![t[u/x]]\!]_v = [\![t]\!]_{v[x \mapsto [\![u]\!]_v]}$ から、EQ_MP は真偽値上の $=$ の意味から、ASSUME は自明に、INST と INST_TYPE は妥当なシーケントがあらゆる付値と型変数のあらゆる解釈のもとで妥当だからである。仕様は各場合を証明している（「Rule-level preservation」）。

2. すべての拡大は無矛盾性を保存する。 DefOK、TypeDefOK、SpecOK は上で論じたとおり保存的である。古い理論のすべてのモデルは新しい理論のモデルに拡張されるので、古い言語の新しい文が証明可能になることはない。

3. インターフェースの安全性。 Thm は抽象型なので、実行時に存在するすべての Thm は、規則の適用とゲートの出力を節点とする有限の導出木の根である。ステップ 1 と 2 を用いてこの木の深さに関する帰納法を行えば、すべての Thm が健全であることが示される。

ステップ 3 は論理ではなくコードの性質であり、src/kernel の外側の何も信頼する必要がないのはそのためである。logic、tactics、prover パッケージはカーネル APIの関数しか呼べないので、何を計算しようとも、それらが返す Thm には導出がある。仕様は六つの義務とその依存関係を述べており、formal_verification/ の適合性パックは、その紙の上の側面を Lean で検査する。

コードが保つ不変条件

• Thm は仮定を α 重複除去したリストとして、結論を de Bruijn 項として保持する。すべての規則の結果は、それが構築された状態において ensure_thm_admissible を通過する。
• KernelState は永続的である。ゲートは新しい状態を返し、元の状態は有効なまま残る。そのため ks_conservative_replay_ok(base, extended, th) は th を両方の状態に対して再検査できる。
• 定数の同一性は理論状態内のカウンタから割り当てられ、スコープが pop された後でも再利用されない。
• 定義ヘッド、型定義ヘッド、無限性アンカーは理論履歴に記録され、ks_pop_scope はこれに触れない。一度定義された名前は再定義できない。

計算量

各規則は前提のサイズに対して線形である。ただし仮定集合の和集合は仮定を総当たりで比較するため、その数について二次である。許容性検査は定数の出現ごとに定理を一度走査し、スコープ付きシグネチャで名前を引くので、宣言数について線形である。同梱サブセットの証明サイズは小さく、カーネルは漸近的な速度よりも監査しやすい検査を優先する。

却下した代替案

• HOL Light のような名前付き項とリネーム。 すべての規則に正しいリネーム関数が必要になるが、これはカーネルのバグの典型的な原因である。de Bruijn コアはリネームを完全に避ける。
• 結合子をカーネルのプリミティブにする。 $\wedge$、$\to$、$\forall$ を固有の規則を持つ基本定数として加えると、カーネルとその健全性証明が大きくなる。代わりにこれらは $=$ 上の定義とする。
• 規則の失敗に例外を使う。 HOL Light は Failure を送出する。Result は失敗をすべて型に現し、フロントエンドが誤って失敗を捕捉して無視することを防ぐ。
• 検証パスを別に持つ未検査の規則。 許容性を最後にだけ検査すると、許容されない中間定理が後続のステップに入り込みうる。代わりにすべての規則が入力と出力を検査する。
• 任意の公理。 項を定理に変える関数は存在しない。導出によらない定理は定義と型定義契約のみであり、いずれも保存性の条件を持つゲートが生成する。

境界

• カーネルはテキストの解析、名前のエラボレーション、タクティクの実行を行わない。これらは elab、parser、tactics パッケージの役割であり、いずれも信頼されない。
• 等号と選択以外の結合子も、量化子の構文も実装しない。残りは logic パッケージが定義する。
• 証明済みの定理を名前で保存しない。定理名はフロントエンドの関心事である。
• メタ変数も未完了の定理も持たない。証明スクリプト中の hole がカーネルに到達することはない。
• 自身の健全性を証明しない。上記および仕様中の議論は紙の上の証明であり、formal_verification/ が Lean と整合させるのは仕様であって MoonBit のソースではない。
• 選択公理を定理として提供しない。@ は宣言され SpecOK で使われるが、$P\,x \to P(@P)$ を返す公開関数は存在しない。

Footnotes

1. R. Milner, “LCF: A way of doing proofs with a machine”, 1979; J. Harrison, “HOL Light: An overview”, TPHOLs 2009. QED は基本規則の選択において HOL Light に最も近く従っている。 ↩

2. N. G. de Bruijn, “Lambda calculus notation with nameless dummies”, Indagationes Mathematicae 34, 1972. ↩