Luna Flow
日本語

kernel チュートリアル

このチュートリアルでは、kernel パッケージの基本規則で直接定理を証明する。最後には、型付きの項を構築し、等号の対称性のような新しい規則を 10 個の基本規則から導出し、定数を宣言・定義し、定理がその定数の意味より長く生き延びられない理由を理解できるようになる。parser や prover パッケージは不要で、ここでのすべては素の MoonBit である。

クイックスタート

モジュールに QED を追加し、それを使うパッケージの moon.pkg でカーネルをインポートする。

moon add Luna-Flow/QED@0.1.0
import {
  "Luna-Flow/QED/kernel",
}

最小の証明は規則一つである。REFL は任意の項がそれ自身に等しいことを証明する。

test "quick start" {
  let st = @kernel.empty_kernel_state()
  let p = @kernel.mk_var("p", @kernel.bool_ty())
  let th = @kernel.refl_checked(st, p).unwrap()
  inspect(
    @kernel.thm_to_string(th),
    content="[] |- Comb(Comb(Const(= : fun(bool, fun(bool, bool))), FVar(p : bool)), FVar(p : bool))",
  )
}

出力は ⊢p=p\vdash p = p と読める。仮定はなく（[]）、結論は型 bool→bool→bool\mathit{bool} \to \mathit{bool} \to \mathit{bool} の等号定数 = を p に 2 回適用したものである。thm_to_string はカーネルが扱う de Bruijn 形式を出力するため、自由変数は FVar として現れる。

すべての規則は最初に KernelState を取る。空の状態は型 bool、ind、fun、組み込みの等号、そして選択定数 @ を知っている。

日常的な作業

項を構築して型検査する

項は mk_var、mk_comb、mk_abs、mk_eq で構築する。型を求めるか規則で項を使うまで、何も検査されない。

test "build terms" {
  let a = @kernel.mk_tyvar("A")
  let f = @kernel.mk_var("f", @kernel.fun_ty(a, a))
  let x = @kernel.mk_var("x", a)
  let fx = @kernel.mk_comb(f, x)
  inspect(@kernel.hol_type_to_string(@kernel.type_of(fx).unwrap()), content="A")
  // λx. f x has type A -> A
  let lam = @kernel.mk_abs(x, fx)
  inspect(@kernel.hol_type_to_string(@kernel.type_of(lam).unwrap()), content="fun(A, A)")
  // f applied to itself is ill-typed
  inspect(@kernel.type_of(@kernel.mk_comb(f, f)) is None, content="true")
  // α-equivalence ignores the name of the bound variable
  let y = @kernel.mk_var("y", a)
  inspect(@kernel.term_alpha_eq(lam, @kernel.mk_abs(y, @kernel.mk_comb(f, y))), content="true")
}

仮定を使う

ASSUME は仮定を導入し、EQ_MP は命題間の等式を使って証明を一方の辺から他方へ移す。両者を合わせると {p=q,p}⊢q\{p = q, p\} \vdash q が証明できる。

test "hypotheses" {
  let st = @kernel.empty_kernel_state()
  let bool = @kernel.bool_ty()
  let p = @kernel.mk_var("p", bool)
  let q = @kernel.mk_var("q", bool)
  let th_eq = @kernel.assume_checked(st, @kernel.mk_eq(p, q).unwrap()).unwrap() // {p = q} |- p = q
  let th_p = @kernel.assume_checked(st, p).unwrap() // {p} |- p
  let th_q = @kernel.eq_mp_checked(st, th_eq, th_p).unwrap() // {p = q, p} |- q
  inspect(@kernel.thm_hyp_count(th_q), content="2")
  inspect(@kernel.term_to_string(@kernel.thm_concl(th_q).unwrap()), content="Var(q : bool)")
  // EQ_MP checks that the second theorem proves the left-hand side
  inspect(@kernel.eq_mp_checked(st, th_eq, th_eq) is Err(@kernel.AlphaMismatch), content="true")
}

等号の対称性を導出する

カーネルには対称性の規則がない。それは導出可能であり、その導出は大きな規則が基本規則からどう構築されるかを示している。Γ⊢s=t\Gamma \vdash s = t から始める。

⊢(=)=(=)REFLΓ⊢(=) s=(=) tMK_COMB with the premiseΓ⊢(s=s)=(t=s)MK_COMB with ⊢s=sΓ⊢t=sEQ_MP with ⊢s=s\begin{aligned} &\vdash (=) = (=) && \textsf{REFL} \\ &\Gamma \vdash (=)\,s = (=)\,t && \textsf{MK\_COMB} \text{ with the premise} \\ &\Gamma \vdash (s = s) = (t = s) && \textsf{MK\_COMB} \text{ with } \vdash s = s \\ &\Gamma \vdash t = s && \textsf{EQ\_MP} \text{ with } \vdash s = s \end{aligned} 
fn sym(st : @kernel.KernelState, th : @kernel.Thm) -> @kernel.Thm raise @kernel.LogicError {
  let (s, _) = @kernel.dest_eq(@kernel.thm_concl(th).unwrap_or_error()).unwrap_or_error()
  let ty = @kernel.type_of(s).unwrap()
  let eq = @kernel.mk_const("=", @kernel.fun_ty(ty, @kernel.fun_ty(ty, @kernel.bool_ty())))
  let refl_eq = @kernel.refl_checked(st, eq).unwrap_or_error()
  let th1 = @kernel.mk_comb_rule_checked(st, refl_eq, th).unwrap_or_error()
  let refl_s = @kernel.refl_checked(st, s).unwrap_or_error()
  let th2 = @kernel.mk_comb_rule_checked(st, th1, refl_s).unwrap_or_error()
  @kernel.eq_mp_checked(st, th2, refl_s).unwrap_or_error()
}

test "derived symmetry" {
  let st = @kernel.empty_kernel_state()
  let a = @kernel.mk_tyvar("A")
  let x = @kernel.mk_var("x", a)
  let y = @kernel.mk_var("y", a)
  let th = @kernel.assume_checked(st, @kernel.mk_eq(x, y).unwrap()).unwrap() // {x = y} |- x = y
  let flipped = sym(st, th) // {x = y} |- y = x
  let (l, r) = @kernel.dest_eq(@kernel.thm_concl(flipped).unwrap()).unwrap()
  inspect(@kernel.term_to_string(l) + " = " + @kernel.term_to_string(r), content="Var(y : A) = Var(x : A)")
  inspect(@kernel.thm_hyp_count(flipped), content="1")
  // a premise that is not an equation makes sym raise
  let not_eq = @kernel.assume_checked(st, @kernel.mk_var("p", @kernel.bool_ty())).unwrap()
  let r = try sym(st, not_eq) catch { e => Err(e) } noraise { th => Ok(th) }
  inspect(r is Err(@kernel.NotAnEquality), content="true")
}

unwrap_or_error は Err を送出される LogicError に変換するため、前提が等式でなければ sym は NotAnEquality できれいに失敗する。中間の定理はすべてカーネルが検査しており、sym 自体は信頼を必要としない。logic パッケージはこの規則を logic_eq_sym として提供している。

β 簡約と抽象で計算する

BETA は redex がその縮約に等しいことを証明し、ABS は束縛変数がどの仮定にも自由に現れない限り、等式を束縛子の下へ持ち上げる。

test "beta and abs" {
  let st = @kernel.empty_kernel_state()
  let a = @kernel.mk_tyvar("A")
  let x = @kernel.mk_var("x", a)
  let y = @kernel.mk_var("y", a)
  let k = @kernel.mk_abs(x, @kernel.mk_abs(y, x)) // λx. λy. x
  // BETA: (λx. λy. x) y = λ_. y; the inner binder is renamed, not captured
  let th = @kernel.beta_rule_checked(st, @kernel.mk_comb(k, y)).unwrap()
  let (_, rhs) = @kernel.dest_eq(@kernel.thm_concl(th).unwrap()).unwrap()
  inspect(@kernel.term_to_string(rhs), content="Abs(Var(_b0 : A), Var(y : A))")
  // ABS over x: |- λx. x = λx. x from |- x = x
  let th_abs = @kernel.abs_rule_checked(st, x, @kernel.refl_checked(st, x).unwrap()).unwrap()
  inspect(@kernel.thm_hyp_count(th_abs), content="0")
  // but not over a variable that a hypothesis mentions
  let th_h = @kernel.assume_checked(st, @kernel.mk_eq(x, y).unwrap()).unwrap()
  inspect(@kernel.abs_rule_checked(st, x, th_h) is Err(@kernel.VarFreeInHyp), content="true")
}

定数を宣言し、スコープを観察する

定数はスコープ付きシグネチャの中に存在する。定理は自身の各定数がどの宣言を指すかを記録しており、その宣言が有効なものでない場所では、カーネルはその定理の使用を拒否する。

test "scopes" {
  let st0 = @kernel.empty_kernel_state()
  let bool = @kernel.bool_ty()
  let st1 = @kernel.ks_add_const(st0, "c", bool).unwrap()
  let c = @kernel.ks_mk_const(st1, "c").unwrap()
  let th = @kernel.refl_checked(st1, c).unwrap() // |- c = c, about c#1
  // an inner scope declares another c
  let st2 = @kernel.ks_add_const(@kernel.ks_push_scope(st1), "c", bool).unwrap()
  inspect(@kernel.thm_is_admissible(st2, th), content="false")
  inspect(@kernel.trans_checked(st2, th, th) is Err(@kernel.InvalidInstantiation), content="true")
  // after popping the scope the theorem is usable again
  let st3 = @kernel.ks_pop_scope(st2).unwrap()
  inspect(@kernel.trans_checked(st3, th, th) is Ok(_), content="true")
}

定数を定義する

定義は、定数をその定義定理とともに導入する。ゲートは、その定義が理論を矛盾させえないことを検査する。

test "define" {
  let st0 = @kernel.empty_kernel_state()
  let bool = @kernel.bool_ty()
  let x = @kernel.mk_var("x", bool)
  let (st1, def_th) = @kernel.ks_define_const_thm(
    st0,
    "id_bool",
    @kernel.fun_ty(bool, bool),
    @kernel.mk_abs(x, x),
  ).unwrap()
  // |- id_bool = λx. x
  let (lhs, _) = @kernel.dest_eq(@kernel.thm_concl(def_th).unwrap()).unwrap()
  inspect(@kernel.term_to_string(lhs), content="Const(id_bool#1 : fun(bool, bool))")
  // the definition is recorded for audit
  let (gate, heads, _) = @kernel.ks_extension_cert_at(st1, 0).unwrap()
  inspect(gate is @kernel.DefOK && heads == ["id_bool"], content="true")
  // a right-hand side with a free variable is refused
  inspect(@kernel.ks_define_const(st0, "bad", bool, x) is Err(@kernel.DefinitionNotClosed), content="true")
}

さらに進む

導出規則を関数として構築する。 上の sym はあらゆる導出規則のパターンである。すなわち、基本規則を呼び出し、そのエラーを Result を返すか unwrap_or_error で送出することで伝播する、定理から定理への MoonBit 関数である。logic パッケージはそのような関数のライブラリであり、logic_eq_sym、logic_apply_fun_eq、logic_beta_normalize_eq、そして logic API にある命題規則を含む。同じように書けば、自作の規則を健全性の観点でレビューする必要はなく、有用性だけを見ればよい。

具体化する。 INST_TYPE と INST は一般的な定理を特殊化する。型変数 A について証明された定理は、状態が許容するあらゆる型で成り立つ。

test "instantiate" {
  let st = @kernel.empty_kernel_state()
  let a = @kernel.mk_tyvar("A")
  let x = @kernel.mk_var("x", a)
  let th = @kernel.refl_checked(st, x).unwrap() // |- x = x  at A
  let th_bool = @kernel.inst_type(st, [("A", @kernel.bool_ty())], th).unwrap()
  let p = @kernel.mk_var("p", @kernel.bool_ty())
  let x_bool = @kernel.mk_var("x", @kernel.bool_ty())
  let th_p = @kernel.inst_checked(st, [(x_bool, p)], th_bool).unwrap() // |- p = p
  inspect(@kernel.term_alpha_eq(@kernel.thm_concl(th_p).unwrap(), @kernel.mk_eq(p, p).unwrap()), content="true")
  // a type the state does not know is refused
  let bad = @kernel.inst_type(st, [("A", @kernel.mk_tyapp("nat", []))], th)
  inspect(bad is Err(@kernel.InvalidInstantiation), content="true")
}

理論を拡張する。 ks_register_type_definition は既存の型の空でない部分集合から新しい型を追加し、ks_specify_const はウィットネスを与えて、ある性質で特徴付けられる定数を追加する。どちらも kernel API のページに例がある。拡張前の状態を保持しておくこと。ks_conservative_replay_ok(base, extended, th) は、拡張後に証明されたが古い言語で述べられた定理が、依然として古い理論の定理であることを検査する。

エラーを扱う。 すべての失敗は LogicError または SigError の値である。特定の失敗に対応するには is でマッチし、LogicError を送出する関数からは unwrap_or_error で伝播させる。

上の層へ進む。 規則を一つずつ使って証明を書くのはカーネルをテストする方法であって、証明を書くための方法ではない。tactics チュートリアルはゴールから後ろ向きに進み、prover チュートリアルは、ここで示したのとまったく同じ規則で検査される定理スクリプトを実行する。

よくある落とし穴

  • 項を構造的に比較する。 定理から読み戻した項には _b0 のような生成された束縛名が付いている。比較には term_alpha_eq、定数の同一性が異なりうる場合は term_logical_eq を使い、決して term_to_string を使わないこと。
  • mk_const で定数を構築する。 mk_const は定数を未解決のままにし、規則は状態が宣言していない定数を拒否する（TypeMismatch）。同一性とスキーマを状態から取得する ks_mk_const または ks_mk_const_instance を使うこと。等号定数 = は例外で、組み込みである。
  • 束縛名を別の型で再利用する。 mk_abs(mk_var("x", A), mk_var("x", B)) は de Bruijn 境界で拒否される（BoundaryFailure）。異なる名前を使うこと。
  • 状態をまたいで定理を使う。 定理は各規則に渡された状態に対して検査される。定数をシャドーイングした後は、スコープがポップされるまで、外側の定数に関する古い定理は InvalidInstantiation で失敗する。
  • 命題でないものを仮定する。 ASSUME、ADD_ASSUM、EQ_MP は型 bool の項を必要とし、そうでなければ NotBoolTerm を返す。
  • unwrap を安全だと思い込む。 例では簡潔さのために unwrap を使っている。ライブラリのコードでは Result に対してマッチすべきである。

次のステップ

  • kernel API には、すべての関数がその正確な失敗条件とともに列挙されている。
  • kernel 設計は、これらの規則が健全である理由と、定理型が抽象的である理由を説明する。
  • logic チュートリアルは、カーネルの上に命題結合子を構築する。
  • 形式仕様は、すべての規則の規範的な定義である。