kernel API リファレンス

kernel パッケージ(Luna-Flow/QED/kernel)は QED の信頼カーネルである。HOL の型と項、抽象定理型 Thm、Thm を構築する唯一の手段である基本推論規則、スコープ付きシグネチャ、および 3 つの拡張ゲート DefOK、TypeDefOK、SpecOK を定義する。他の QED パッケージには依存しない。他のすべてのパッケージは、このページの関数を通じてのみ定理に到達する。

失敗は値である。規則は Result[Thm, LogicError] を返し、シグネチャ操作は Result[_, SigError] を返す。このページのどの操作も、不正な入力で異常終了しない。

このページの例は、パッケージを @kernel としてインポートするブラックボックステストである。規則の意味はカーネル設計ノートで説明されており、順を追った解説はカーネルチュートリアルにある。規範的な定義は形式仕様にある。

QED 形式仕様

型

`HolType`

HolType は単純型であり、型変数、または引数に適用された型コンストラクタである。

pub enum HolType {
  TyVal(String)
  TyApp(String, Array[HolType])
}

TyVal(a) は a という名前の型変数 $\alpha$ である。TyApp(c, args) はコンストラクタ c を args に適用する。組み込みのコンストラクタは bool(アリティ 0)、ind(アリティ 0)、fun(アリティ 2)であり、fun(a, b) は関数型 $a \to b$ である。他のコンストラクタは、ks_register_type_definition が受理して初めて使用可能になる。この enum はパッケージ外では読み取り専用である。パターンマッチはできるが、値の構築は以下の関数で行う。

`mk_tyvar`

mk_tyvar は、与えられた名前の型変数を構築する。

pub fn mk_tyvar(String) -> HolType

`mk_tyapp`

mk_tyapp は型コンストラクタを引数リストに適用する。

pub fn mk_tyapp(String, Array[HolType]) -> HolType

結果はシグネチャに対して検査されない。状態がそれを受理するかどうかは ks_type_is_admissible が判定する。

`bool_ty`、`ind_ty`、`fun_ty`

これらの関数は 3 つの組み込み型を構築する。bool_ty() は bool、ind_ty() は無限個体型 ind、fun_ty(a, b) は $a \to b$ である。

pub fn bool_ty() -> HolType
pub fn ind_ty() -> HolType
pub fn fun_ty(HolType, HolType) -> HolType

`dest_tyapp` と `dest_fun_ty`

dest_tyapp は型適用のコンストラクタと引数を返し、dest_fun_ty は関数型の定義域と値域を返す。どちらも、それ以外の形では None を返す。

pub fn dest_tyapp(HolType) -> (String, Array[HolType])?
pub fn dest_fun_ty(HolType) -> (HolType, HolType)?

`is_bool_ty`、`is_tyvar`、`is_tyapp`

これらの述語は型の形を検査する。

pub fn is_bool_ty(HolType) -> Bool
pub fn is_tyvar(HolType) -> Bool
pub fn is_tyapp(HolType) -> Bool

`ty_eq`

ty_eq は型の構造的等価性である。

pub fn ty_eq(HolType, HolType) -> Bool

`tyvars` と `tyvars_subset`

tyvars は型の型変数を、最初の出現順に重複なしで列挙する。tyvars_subset(a, b) は、a のすべての型変数が b に現れるときに成り立つ。

pub fn tyvars(HolType) -> Array[String]
pub fn tyvars_subset(HolType, HolType) -> Bool

`ty_is_instance_of`

ty_is_instance_of(instance, schema) は、ある型代入 $\theta$ が schema を instance に写すとき、すなわち $\mathit{schema}\,\theta = \mathit{instance}$ のときに成り立つ。

pub fn ty_is_instance_of(HolType, HolType) -> Bool

引数の順序に注意すること。インスタンスが先に来る。カーネルはこの関係を用いて、多相定数のすべての出現を宣言されたスキーマに対して検査する。

`type_subst`、`type_subst_unsafe`、`has_duplicate_ty_subst_keys`

type_subst(theta, ty) は、型変数名と型の組で与えられた型代入 theta を ty に適用する。theta が同じ変数を 2 度挙げている場合は None を返し、これは has_duplicate_ty_subst_keys で検査できる。type_subst_unsafe はその検査を省略し、繰り返された名前の最初の束縛を用いる。

pub fn type_subst(Array[(String, HolType)], HolType) -> HolType?
pub fn type_subst_unsafe(Array[(String, HolType)], HolType) -> HolType
pub fn has_duplicate_ty_subst_keys(Array[(String, HolType)]) -> Bool

`hol_type_to_string`

hol_type_to_string はテストと診断のために型を整形する。A、bool、fun(A, bool) のようになる。

pub fn hol_type_to_string(HolType) -> String

test "types" {
  let a = @kernel.mk_tyvar("A")
  let pred = @kernel.fun_ty(a, @kernel.bool_ty())
  inspect(@kernel.hol_type_to_string(pred), content="fun(A, bool)")
  inspect(@kernel.dest_fun_ty(pred) is Some((_, cod)) && @kernel.is_bool_ty(cod), content="true")
  assert_eq(@kernel.tyvars(pred), ["A"])
  let inst = @kernel.type_subst([("A", @kernel.ind_ty())], pred).unwrap()
  inspect(@kernel.hol_type_to_string(inst), content="fun(ind, bool)")
  inspect(@kernel.ty_is_instance_of(inst, pred), content="true")
  inspect(@kernel.ty_is_instance_of(pred, inst), content="false")
  inspect(@kernel.type_subst([("A", a), ("A", a)], pred) is None, content="true")
}

項

`Term`

Term は単純型付きλ計算の名前付き項である。

pub enum Term {
  Var(String, HolType)
  Const(String, HolType, Int)
  Comb(Term, Term)
  Abs(Term, Term)
}

Var(x, ty) は変数であり、名前と型の両方が一致する場合にのみ 2 つの変数は同じになる。Const(c, ty, id) は型 ty での定数 c の出現であり、id はその出現が解決された先の定数の同一性(ConstId)、未解決の場合は -1 である。Comb(f, x) は適用 $f\,x$ であり、Abs(v, body) は抽象 $\lambda v.\,\mathit{body}$ で、その束縛子 v は Var でなければならない。この enum はパッケージ外では読み取り専用である。

`mk_var`、`mk_const`、`mk_const_bound`、`mk_comb`、`mk_abs`

これらの関数は検査なしで項を構築する。mk_const は定数の同一性を未解決(-1)のままにし、mk_const_bound は明示的に設定する。

pub fn mk_var(String, HolType) -> Term
pub fn mk_const(String, HolType) -> Term
pub fn mk_const_bound(String, HolType, Int) -> Term
pub fn mk_comb(Term, Term) -> Term
pub fn mk_abs(Term, Term) -> Term

ここで構築された項は型付けできないかもしれない。type_of がそれを検査し、すべての規則は型付けできない入力を拒否する。型と同一性をシグネチャから取得する ks_mk_const と ks_mk_const_instance を使うほうがよい。

`is_var`、`is_const`、`is_comb`、`is_abs`

これらの述語は項の最外のコンストラクタを検査する。

pub fn is_var(Term) -> Bool
pub fn is_const(Term) -> Bool
pub fn is_comb(Term) -> Bool
pub fn is_abs(Term) -> Bool

`dest_var`、`dest_const`、`dest_comb`、`dest_abs`

これらの関数は項を分解し、それ以外の形では None を返す。dest_const は定数の同一性を捨てる。

pub fn dest_var(Term) -> (String, HolType)?
pub fn dest_const(Term) -> (String, HolType)?
pub fn dest_comb(Term) -> (Term, Term)?
pub fn dest_abs(Term) -> (Term, Term)?

`type_of`

type_of は項の型を計算し、項が型付けできない場合は None を返す。

pub fn type_of(Term) -> HolType?

単純型付きλ計算の型付け規則を実装している。

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

定数は、出現に書かれた型を持つ。コストは項の大きさに対して線形である。

`mk_eq` と `dest_eq`

mk_eq(l, r) は、組み込みの定数 = を型 $\tau \to \tau \to \mathit{bool}$ で用いて、等式 $l = r$ を構築する。dest_eq は等式を分解する。

pub fn mk_eq(Term, Term) -> Result[Term, LogicError]
pub fn dest_eq(Term) -> Result[(Term, Term), LogicError]

mk_eq は、片側が型付けできない、または 2 つの型が異なる場合に TypeMismatch で失敗し、片側を de Bruijn 形式に変換できない場合に BoundaryFailure で失敗する(to_db_term を参照)。dest_eq は、項が = の 2 引数への適用でない場合に NotAnEquality で失敗し、等式が型付けできない場合に TypeMismatch で失敗する。

`free_vars`、`term_is_closed`、`term_has_const_named`

free_vars は項の自由変数を、名前と型の組として重複なしで列挙する。term_is_closed は自由変数がないときに成り立つ。term_has_const_named は、与えられた名前の定数が項のどこかに現れるかを検査する。

pub fn free_vars(Term) -> Array[(String, HolType)]
pub fn term_is_closed(Term) -> Bool
pub fn term_has_const_named(Term, String) -> Bool

`term_tyvars` と `term_tyvars_subset`

term_tyvars は項のどこかに現れる型変数を列挙する。term_tyvars_subset(t, ty) は、t のすべての型変数が ty に現れるときに成り立つ。定義ゲートはこれを用いてゴースト型変数を拒否する。

pub fn term_tyvars(Term) -> Array[String]
pub fn term_tyvars_subset(Term, HolType) -> Bool

`term_apply_ty_subst` と `term_apply_ty_subst_unsafe`

これらの関数は、項の中のすべての型に型代入を適用する。検査付きの形は、型変数が 2 度挙げられている場合に None を返す。

pub fn term_apply_ty_subst(Array[(String, HolType)], Term) -> Term?
pub fn term_apply_ty_subst_unsafe(Array[(String, HolType)], Term) -> Term

`term_alpha_eq` と `term_logical_eq`

term_alpha_eq は α 同値を判定する。束縛変数の名前を付け替えれば等しくなる項である。定数の同一性を含めて de Bruijn 形式を比較する。term_logical_eq は同じ比較だが定数の同一性を無視するため、未解決の c の出現は解決済みの出現と等しくなる。どちらも、項を de Bruijn 形式に変換できない場合は false を返す。

pub fn term_alpha_eq(Term, Term) -> Bool
pub fn term_logical_eq(Term, Term) -> Bool

`term_to_string`

term_to_string は、テストと診断のために名前付きの項を構造的に整形する。

pub fn term_to_string(Term) -> String

test "terms" {
  let a = @kernel.mk_tyvar("A")
  let x = @kernel.mk_var("x", a)
  let y = @kernel.mk_var("y", a)
  let id_x = @kernel.mk_abs(x, x)
  let id_y = @kernel.mk_abs(y, y)
  inspect(@kernel.hol_type_to_string(@kernel.type_of(id_x).unwrap()), content="fun(A, A)")
  inspect(@kernel.term_alpha_eq(id_x, id_y), content="true")
  inspect(@kernel.free_vars(@kernel.mk_comb(id_x, y)).length(), content="1")
  // applying a function of type A -> A to a bool is ill-typed
  let p = @kernel.mk_var("p", @kernel.bool_ty())
  inspect(@kernel.type_of(@kernel.mk_comb(id_x, p)) is None, content="true")
  let eq = @kernel.mk_eq(x, y).unwrap()
  inspect(
    @kernel.term_to_string(eq),
    content="Comb(Comb(Const(= : fun(A, fun(A, bool))), Var(x : A)), Var(y : A))",
  )
  inspect(@kernel.mk_eq(x, p) is Err(@kernel.TypeMismatch), content="true")
  inspect(@kernel.dest_eq(p) is Err(@kernel.NotAnEquality), content="true")
}

de Bruijn 項

規則は型付きの de Bruijn 表現の上で動作するため、α 同値な項はそこでは文字どおり等しい。これらの関数は、監査とテストのためにその表現を公開する。

`DbTerm`

DbTerm は、束縛変数に de Bruijn インデックスを用いる項である。

pub enum DbTerm {
  DbBound(Int, HolType)
  DbFree(String, HolType)
  DbConst(String, HolType, Int)
  DbComb(DbTerm, DbTerm)
  DbAbs(HolType, DbTerm)
}

DbBound(i, ty) は 0 から数えて i 段外側の束縛子を指す。束縛された各出現は型を保持し、DbAbs(ty, body) は束縛子の型を保持するため、この表現は型付きである。

`to_db_term` と `from_db_term`

to_db_term は名前付きの項を de Bruijn 形式に変換する。from_db_term は逆変換を行い、項の自由な名前を避けた新しい束縛子名 _b0、_b1、… を選ぶ。

pub fn to_db_term(Term) -> DbTerm?
pub fn from_db_term(DbTerm) -> Term?

to_db_term は、抽象の束縛子が変数でない場合、または変数が外側の束縛子と同じ名前で異なる型を持つ場合(例: $\lambda (x{:}A).\,(x{:}B)$ )に None を返す。QED は、内側の x を別の自由変数として読むのではなく、そのような項を拒否する。from_db_term は、ぶら下がったインデックスや、束縛子と食い違う型ラベルがある場合に None を返す。成功した場合、from_db_term(to_db_term(t)) は t と α 同値である。

`db_term_eq`、`db_type_of`、`db_term_to_string`

db_term_eq は定数の同一性を含む de Bruijn 項の構造的等価性であり、変換された項については α 同値を判定する。db_type_of は de Bruijn 項に対する type_of である。db_term_to_string は、thm_to_string と同様に、de Bruijn 項を整形する。

pub fn db_term_eq(DbTerm, DbTerm) -> Bool
pub fn db_type_of(DbTerm) -> HolType?
pub fn db_term_to_string(DbTerm) -> String

`db_has_free`

db_has_free(t, v) は、自由変数 v(DbFree)が t に現れるかを検査する。

pub fn db_has_free(DbTerm, DbTerm) -> Bool

`db_subst_free_parallel`

db_subst_free_parallel(t, sigma) は、sigma のキーであるすべての自由変数を、その値で同時に置き換える。値は束縛子の下でシフトされるため、捕獲は起こらない。インデックス計算がオーバーフローする場合にのみ None を返す。

pub fn db_subst_free_parallel(DbTerm, Array[(DbTerm, DbTerm)]) -> DbTerm?

`db_apply_ty_subst`

db_apply_ty_subst は、de Bruijn 項のすべての型ラベルに型代入を適用する。

pub fn db_apply_ty_subst(Array[(String, HolType)], DbTerm) -> DbTerm

`db_beta_reduce_once`

db_beta_reduce_once は最上位の β リデックス $(\lambda.\,t)\,u$ を縮約し、それ以外の形では None を返す。

pub fn db_beta_reduce_once(DbTerm) -> DbTerm?

縮約は $\uparrow^{-1}_0\big(t[0 \mapsto \uparrow^{1}_0 u]\big)$ である。すなわち u を上にシフトし、インデックス 0 に代入し、結果を下にシフトする。これが捕獲を避ける理由は、カーネル設計ノートで導出されている。

test "de bruijn" {
  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
  let db = @kernel.to_db_term(k).unwrap()
  inspect(@kernel.db_term_to_string(db), content="Abs(A. Abs(A. BVar(1 : A)))")
  // (λx. λy. x) y  reduces to  λ_b. y, not to λy. y
  let redex = @kernel.to_db_term(@kernel.mk_comb(k, y)).unwrap()
  let out = @kernel.db_beta_reduce_once(redex).unwrap()
  inspect(@kernel.db_term_to_string(out), content="Abs(A. FVar(y : A))")
  inspect(
    @kernel.term_to_string(@kernel.from_db_term(out).unwrap()),
    content="Abs(Var(_b0 : A), Var(y : A))",
  )
  // a binder name reused at another type is rejected
  let x_bool = @kernel.mk_var("x", @kernel.bool_ty())
  inspect(@kernel.to_db_term(@kernel.mk_abs(x, x_bool)) is None, content="true")
}

定理

`Thm`

Thm は定理の抽象型であり、シーケント $\Gamma \vdash p$ である。有限の仮定の集合 $\Gamma$ と結論 $p$ を持ち、すべて型は bool である。

type Thm

この型は抽象的であり、パッケージ外のコードは Thm を構築も変更もできない。Thm 型の値は、基本規則または拡張ゲートがそれを生成したからこそ存在する。これがカーネル設計ノートにおける信頼論証の根拠のすべてである。仮定は α 同値類の集合として保持され、α 同値な重複は併合される。

`thm_hyps`、`thm_concl`、`thm_hyp_count`

thm_hyps は仮定を、thm_concl は結論を、名前付きの項として返す。thm_hyp_count は仮定の数を返す。

pub fn thm_hyps(Thm) -> Result[Array[Term], LogicError]
pub fn thm_concl(Thm) -> Result[Term, LogicError]
pub fn thm_hyp_count(Thm) -> Int

束縛変数は正規の名前(_b0、…)で返ってくるため、結果は構造的にではなく term_alpha_eq または term_logical_eq で比較すること。カーネルが構築した定理では、Err(BoundaryFailure) の場合は起こり得ない。

`thm_to_string`

thm_to_string は定理を de Bruijn 形式で [h1, h2] |- c の形に整形する。

pub fn thm_to_string(Thm) -> String

`thm_is_admissible` と `thm_bind_const_ids`

thm_is_admissible(state, th) は、th が state で受理可能であるときに成り立つ。すなわち、そこで言及されるすべての定数が、定理に記録された同一性で宣言されており、すべての定数の出現が宣言されたスキーマのインスタンスであり、すべての型が許容され、定義定理がなお自身の定義と一致している。thm_bind_const_ids は、th の定数の同一性を state で解決されたとおりに記録し、その後で許容性を検査する。

pub fn thm_is_admissible(KernelState, Thm) -> Bool
pub fn thm_bind_const_ids(KernelState, Thm) -> Result[Thm, LogicError]

検査付きのすべての規則は、前提と結果に対してこの検査を行う。したがって、スコープ変更の前に証明された定理は、その変更によって定数の意味が変わった後には使えない。thm_bind_const_ids は、同一性が状態と食い違う場合は InvalidInstantiation で、定数が未知の場合は TypeMismatch で失敗する。

基本規則

各規則は最初にカーネル状態を取り、前提の定理がその状態で許容されることを検査し、規則を適用して結果を検査する。以下の規則では、 $\Gamma, \Delta$ は仮定の集合、 $\equiv_\alpha$ は(定数の同一性を無視した)α 同値、 $\setminus$ は与えられた項と α 同値なすべての仮定を取り除く操作である。各規則がなぜ健全かは、カーネル設計ノートで説明されている。

`refl_checked`

refl_checked は REFL である。項がそれ自身と等しいことを証明する。

pub fn refl_checked(KernelState, Term) -> Result[Thm, LogicError]

\frac{}{\vdash t = t}\;\textsf{REFL}

t が型付けできない、または状態が宣言していない定数に言及している場合は TypeMismatch で失敗し、t を de Bruijn 形式に変換できない場合は BoundaryFailure で失敗する。

`assume_checked`

assume_checked は ASSUME である。命題をそれ自身から証明する。

pub fn assume_checked(KernelState, Term) -> Result[Thm, LogicError]

\frac{p : \mathit{bool}}{\{p\} \vdash p}\;\textsf{ASSUME}

p が型付けできるが型 bool でない場合は NotBoolTerm で失敗する。

`add_assum_checked`

add_assum_checked(state, q, th) は、命題 q を th の仮定に加える(弱化)。

pub fn add_assum_checked(KernelState, Term, Thm) -> Result[Thm, LogicError]

\frac{\Gamma \vdash p \qquad q : \mathit{bool}}{\Gamma \cup \{q\} \vdash p}\;\textsf{ADD\_ASSUM}

弱化は仕様の 10 個の規則には含まれない。ASSUME、DEDUCT_ANTISYM_RULE、EQ_MP から導出可能であり、その導出はカーネル設計ノートに示されている。q が命題でない場合は NotBoolTerm で失敗する。

`trans_checked`

trans_checked は TRANS である。2 つの等式を連鎖させる。

pub fn trans_checked(KernelState, Thm, Thm) -> Result[Thm, LogicError]

\frac{\Gamma \vdash s = t \qquad \Delta \vdash t' = u \qquad t \equiv_\alpha t'}{\Gamma \cup \Delta \vdash s = u}\;\textsf{TRANS}

前提が等式でない場合は NotAnEquality で失敗し、中間の項が異なる場合は AlphaMismatch で失敗する。

`mk_comb_rule_checked`

mk_comb_rule_checked は MK_COMB である。等しい関数を等しい引数に適用すると、等しい結果が得られる。

pub fn mk_comb_rule_checked(KernelState, Thm, Thm) -> Result[Thm, LogicError]

\frac{\Gamma \vdash f = g \qquad \Delta \vdash x = y}{\Gamma \cup \Delta \vdash f\,x = g\,y}\;\textsf{MK\_COMB}

$f, g : \sigma \to \tau$ かつ $x, y : \sigma$ でない限り、TypeMismatch で失敗する。

`abs_rule_checked`

abs_rule_checked(state, x, th) は ABS である。等式の両辺を変数について抽象する。

pub fn abs_rule_checked(KernelState, Term, Thm) -> Result[Thm, LogicError]

\frac{\Gamma \vdash s = t \qquad x \notin \mathrm{FV}(\Gamma)}{\Gamma \vdash (\lambda x.\,s) = (\lambda x.\,t)}\;\textsf{ABS}

x が仮定に自由に現れる場合は VarFreeInHyp で、x が変数でない場合は InvalidInstantiation で、前提が等式でない場合は NotAnEquality で失敗する。

`beta_rule_checked`

beta_rule_checked は BETA である。β リデックスがその縮約と等しいことを証明する。

pub fn beta_rule_checked(KernelState, Term) -> Result[Thm, LogicError]

\frac{u : \sigma}{\vdash (\lambda (x{:}\sigma).\,t)\,u = t[u/x]}\;\textsf{BETA}

代入は de Bruijn 項の上で実行されるため、捕獲回避的である。項が抽象の適用でない場合は NotTrivialBetaRedex で失敗し、引数の型が束縛子の型と異なる場合は TypeMismatch で失敗する。

`eq_mp_checked`

eq_mp_checked は EQ_MP である。命題間の等式は、左辺の証明を右辺の証明へと運ぶ。

pub fn eq_mp_checked(KernelState, Thm, Thm) -> Result[Thm, LogicError]

\frac{\Gamma \vdash p = q \qquad \Delta \vdash p' \qquad p \equiv_\alpha p'}{\Gamma \cup \Delta \vdash q}\;\textsf{EQ\_MP}

両辺が命題でない場合は NotBoolTerm で失敗し、2 つ目の前提が左辺を証明していない場合は AlphaMismatch で失敗する。

`deduct_antisym_rule_checked`

deduct_antisym_rule_checked は DEDUCT_ANTISYM_RULE である。互いを証明する 2 つの命題は等しい。

pub fn deduct_antisym_rule_checked(KernelState, Thm, Thm) -> Result[Thm, LogicError]

\frac{\Gamma \vdash p \qquad \Delta \vdash q}{(\Gamma \setminus \{q\}) \cup (\Delta \setminus \{p\}) \vdash p = q}\;\textsf{DEDUCT\_ANTISYM\_RULE}

結論が命題でない場合は NotBoolTerm で失敗する。

`inst_type`

inst_type(state, theta, th) は INST_TYPE である。定理全体にわたって型変数をインスタンス化する。

pub fn inst_type(KernelState, Array[(String, HolType)], Thm) -> Result[Thm, LogicError]

\frac{\Gamma \vdash p}{\Gamma\theta \vdash p\theta}\;\textsf{INST\_TYPE}

theta が同じ変数を 2 度挙げている、または状態が許容しない型へ写している場合は InvalidInstantiation で失敗し、インスタンス化された定数がスキーマのインスタンスでなくなった場合は TypeMismatch で失敗する。

`inst_checked`

inst_checked(state, sigma, th) は INST である。定理全体にわたって、自由変数に項を同時に代入する。

pub fn inst_checked(KernelState, Array[(Term, Term)], Thm) -> Result[Thm, LogicError]

\frac{\Gamma \vdash p}{\Gamma\sigma \vdash p\sigma}\;\textsf{INST} \qquad \sigma = [x_1 \mapsto t_1, \dots, x_n \mapsto t_n],\; x_i, t_i : \tau_i

ABS と異なり、INST は仮定にも代入を行うため、仮定に現れる変数に触れてもよい。キーが変数でない、または 2 度現れる場合は InvalidInstantiation で失敗し、値がキーと異なる型を持つ場合は TypeMismatch で失敗する。

test "primitive rules" {
  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)
  // {p} |- p
  let th_p = @kernel.assume_checked(st, p).unwrap()
  inspect(@kernel.thm_to_string(th_p), content="[FVar(p : bool)] |- FVar(p : bool)")
  // {p = q} |- p = q, then EQ_MP gives {p = q, p} |- q
  let th_eq = @kernel.assume_checked(st, @kernel.mk_eq(p, q).unwrap()).unwrap()
  let th_q = @kernel.eq_mp_checked(st, th_eq, th_p).unwrap()
  inspect(@kernel.thm_hyp_count(th_q), content="2")
  inspect(@kernel.term_to_string(@kernel.thm_concl(th_q).unwrap()), content="Var(q : bool)")
  // DEDUCT_ANTISYM on {p} |- p and {q} |- q gives {p, q} |- p = q
  let th_q0 = @kernel.assume_checked(st, q).unwrap()
  let th_pq = @kernel.deduct_antisym_rule_checked(st, th_p, th_q0).unwrap()
  inspect(@kernel.thm_hyp_count(th_pq), content="2")
  // INST renames p to q everywhere
  let th_inst = @kernel.inst_checked(st, [(p, q)], th_p).unwrap()
  inspect(@kernel.thm_to_string(th_inst), content="[FVar(q : bool)] |- FVar(q : bool)")
  // ASSUME needs a proposition
  let x = @kernel.mk_var("x", @kernel.mk_tyvar("A"))
  inspect(@kernel.assume_checked(st, x) is Err(@kernel.NotBoolTerm), content="true")
}

test "equality rules" {
  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 id = @kernel.mk_abs(x, x)
  // BETA: |- (λx. x) y = y
  let th_beta = @kernel.beta_rule_checked(st, @kernel.mk_comb(id, y)).unwrap()
  let (_, rhs) = @kernel.dest_eq(@kernel.thm_concl(th_beta).unwrap()).unwrap()
  inspect(@kernel.term_to_string(rhs), content="Var(y : A)")
  // TRANS with REFL on the right-hand side changes nothing
  let th_t = @kernel.trans_checked(st, th_beta, @kernel.refl_checked(st, y).unwrap()).unwrap()
  inspect(@kernel.thm_to_string(th_t) == @kernel.thm_to_string(th_beta), content="true")
  // ABS over y is refused: y is free in the hypothesis {x = y}
  let th_h = @kernel.assume_checked(st, @kernel.mk_eq(x, y).unwrap()).unwrap()
  inspect(@kernel.abs_rule_checked(st, y, th_h) is Err(@kernel.VarFreeInHyp), content="true")
  // INST_TYPE: instantiate A := bool
  let th_b = @kernel.inst_type(st, [("A", @kernel.bool_ty())], th_beta).unwrap()
  assert_eq(@kernel.term_tyvars(@kernel.thm_concl(th_b).unwrap()), [])
  // BETA needs a redex
  inspect(@kernel.beta_rule_checked(st, y) is Err(@kernel.NotTrivialBetaRedex), content="true")
}

カーネル状態

`KernelState`

KernelState は抽象的な論理状態であり、スコープ付きの定数シグネチャと、理論の履歴(定義、型定義、特殊化、無限性アンカー、監査証明書)から成る。

type KernelState

状態は不変の値である。状態を拡張するすべての操作は新しい状態を返し、古い状態は有効なまま残るため、以前の状態を保存性検査の基準として保持できる。

`empty_kernel_state`

empty_kernel_state は初期状態を返す。

pub fn empty_kernel_state() -> KernelState

これは定数をちょうど 1 つ、すなわち同一性 0 でスキーマ $(\alpha \to \mathit{bool}) \to \alpha$ の選択演算子 @ を宣言し、型 bool、ind、fun を許容する。等号定数 = は組み込みで宣言を必要とせず、= と @ は予約名である。

`ks_add_const`

ks_add_const(state, name, ty) は、スキーマ ty の定数を最も内側のスコープで宣言し、新しい同一性を与える。

pub fn ks_add_const(KernelState, String, HolType) -> Result[KernelState, SigError]

同じスコープで同じ名前を同じ型で再び宣言した場合は、状態は変わらずに返される。次の場合は失敗する。名前が最も内側のスコープで別の型で宣言されていれば ConstTypeConflict、= と @ に対しては ReservedSymbol、定義された定数に対しては DefinitionAlreadyExists、型定義が使っている名前に対しては TypeRepresentationAlreadyExists または TypeAbstractionAlreadyExists、ty が状態の許容しない型に言及していれば TypeMismatch。

`ks_lookup_const`、`ks_const_schema`、`ks_lookup_const_id`

ks_lookup_const と ks_const_schema はどちらも、名前の下で可視な定数の宣言されたスキーマを返し、ks_lookup_const_id はその同一性を返す。最も内側の宣言が優先される。

pub fn ks_lookup_const(KernelState, String) -> HolType?
pub fn ks_const_schema(KernelState, String) -> HolType?
pub fn ks_lookup_const_id(KernelState, String) -> Int?

`ks_mk_const` と `ks_mk_const_instance`

ks_mk_const は、可視な定数の出現をそのスキーマ型で、同一性を記録して構築する。ks_mk_const_instance は、スキーマのインスタンスでの出現を構築する。

pub fn ks_mk_const(KernelState, String) -> Result[Term, SigError]
pub fn ks_mk_const_instance(KernelState, String, HolType) -> Result[Term, SigError]

どちらも、その名前の定数がない場合は UnknownConst で失敗する。ks_mk_const_instance は、型がスキーマのインスタンスでない場合は InvalidConstInstance で、型が許容されない場合は TypeMismatch で失敗する。

`ks_push_scope` と `ks_pop_scope`

ks_push_scope は新しい最内スコープを開く。ks_pop_scope はそれを閉じ、その中で宣言されたすべての定数を捨てる。

pub fn ks_push_scope(KernelState) -> KernelState
pub fn ks_pop_scope(KernelState) -> Result[KernelState, SigError]

内側のスコープで宣言された定数は、同じ名前の外側の定数をシャドーイングし、新しい同一性を得る。ポップはシグネチャを変えるだけである。スコープ内で記録された定義、型定義、証明書は理論の履歴に残るため、それらの名前は使用済みのままになる。ks_pop_scope は最外スコープでは ScopeUnderflow で失敗する。

`ks_sig`

ks_sig は状態のシグネチャ部分を返す。

pub fn ks_sig(KernelState) -> GlobalSig

`ks_type_is_admissible` と `ks_type_subst_is_admissible`

ks_type_is_admissible は、型のすべての型コンストラクタが組み込みであるか、型定義によって正しいアリティで許容されているときに成り立つ。ks_type_subst_is_admissible は、代入のすべての型が許容されるときに成り立つ。

pub fn ks_type_is_admissible(KernelState, HolType) -> Bool
pub fn ks_type_subst_is_admissible(KernelState, Array[(String, HolType)]) -> Bool

`ks_term_in_language` と `ks_thm_is_sentence_in_language`

ks_term_in_language は、項のすべての型が許容され、すべての定数の出現が宣言された定数のスキーマのインスタンスであり、同一性が記録されている場合はそれが一致するときに成り立つ。ks_thm_is_sentence_in_language は、定理が仮定を持たず、結論が状態の言語における閉じた命題であるときに成り立つ。

pub fn ks_term_in_language(KernelState, Term) -> Bool
pub fn ks_thm_is_sentence_in_language(KernelState, Thm) -> Bool

test "scopes and constants" {
  let st0 = @kernel.empty_kernel_state()
  let a = @kernel.mk_tyvar("A")
  let st1 = @kernel.ks_add_const(st0, "c", a).unwrap()
  inspect(@kernel.term_to_string(@kernel.ks_mk_const(st1, "c").unwrap()), content="Const(c#1 : A)")
  let c_bool = @kernel.ks_mk_const_instance(st1, "c", @kernel.bool_ty()).unwrap()
  inspect(@kernel.term_to_string(c_bool), content="Const(c#1 : bool)")
  let th = @kernel.refl_checked(st1, @kernel.ks_mk_const(st1, "c").unwrap()).unwrap()
  // shadow c in an inner scope: the old theorem is no longer admissible there
  let st2 = @kernel.ks_add_const(@kernel.ks_push_scope(st1), "c", @kernel.bool_ty()).unwrap()
  assert_eq(@kernel.ks_lookup_const_id(st2, "c"), Some(2))
  inspect(@kernel.thm_is_admissible(st2, th), content="false")
  // pop the scope: the outer c is visible again and the theorem is usable
  let st3 = @kernel.ks_pop_scope(st2).unwrap()
  assert_eq(@kernel.ks_lookup_const_id(st3, "c"), Some(1))
  inspect(@kernel.thm_is_admissible(st3, th), content="true")
  inspect(@kernel.ks_pop_scope(st3) is Err(@kernel.ScopeUnderflow), content="true")
  inspect(@kernel.ks_add_const(st0, "@", a) is Err(@kernel.ReservedSymbol), content="true")
}

シグネチャ

GlobalSig は、理論の履歴を含まない、スコープ付き定数テーブルそのものである。これらの関数はそれを直接操作し、Thm は決して生成しない。

`GlobalSig` と `ConstId`

GlobalSig はスコープのスタックで、最も内側が末尾に来る。各スコープは名前、同一性、スキーマを列挙する。ConstId は宣言された定数の整数の同一性である。

pub enum GlobalSig {
  Sig(Array[Array[(String, Int, HolType)]])
}

pub type ConstId = Int

`empty_sig`、`sig_push_scope`、`sig_pop_scope_e`

empty_sig は空のスコープを 1 つ持つシグネチャであり、empty_kernel_state のシグネチャと異なり @ を含まない。sig_push_scope と sig_pop_scope_e はスコープを開閉する。最後のスコープをポップすると ScopeUnderflow で失敗する。

pub fn empty_sig() -> GlobalSig
pub fn sig_push_scope(GlobalSig) -> GlobalSig
pub fn sig_pop_scope_e(GlobalSig) -> Result[GlobalSig, SigError]

`sig_has_const`、`sig_lookup_const`、`sig_lookup_const_id`

これらの関数は、最も内側のスコープから外側へ向かって名前を検索する。

pub fn sig_has_const(GlobalSig, String) -> Bool
pub fn sig_lookup_const(GlobalSig, String) -> HolType?
pub fn sig_lookup_const_id(GlobalSig, String) -> Int?

`sig_add_const_idempotent_e`

sig_add_const_idempotent_e は、次の空き同一性で最も内側のスコープに定数を宣言する。同じ宣言がすでにある場合は、シグネチャを変えずに返す。

pub fn sig_add_const_idempotent_e(GlobalSig, String, HolType) -> Result[GlobalSig, SigError]

= と @ に対しては ReservedSymbol で、最も内側のスコープがその名前を別の型で宣言している場合は ConstTypeConflict で失敗する。

`sig_mk_const_e` と `sig_mk_const_instance_e`

これらの関数は ks_mk_const および ks_mk_const_instance と同様に、シグネチャから定数の出現を構築するが、カーネル状態の型許容性検査は行わない。

pub fn sig_mk_const_e(GlobalSig, String) -> Result[Term, SigError]
pub fn sig_mk_const_instance_e(GlobalSig, String, HolType) -> Result[Term, SigError]

`sig_define_const_e`

sig_define_const_e(sig, name, rhs) は name を rhs の型で宣言し、定義等式 $\mathit{name} = \mathit{rhs}$ を項として返す。

pub fn sig_define_const_e(GlobalSig, String, Term) -> Result[(GlobalSig, Term), SigError]

この等式は項にすぎず定理ではない。この関数は論理的な権限を持たない。定義定理を得るには ks_define_const_thm を使うこと。rhs が型付けできない場合は InvalidConstRhs で失敗する。

拡張ゲート

理論は 3 つのゲートを通じてのみ拡張される。各ゲートは副条件を検査し、新しい名前を理論の履歴に記録し、監査証明書を追加する。

`ks_define_const` と `ks_define_const_thm`

ks_define_const(state, c, ty, rhs) は定義ゲート DefOK である。定数 c : ty を宣言し、定義 $c = \mathit{rhs}$ を記録する。ks_define_const_thm は同じことを行い、定義定理 $\vdash c = \mathit{rhs}$ を返す。ks_define_const は等式を項として返す。

pub fn ks_define_const(KernelState, String, HolType, Term) -> Result[(KernelState, Term), SigError]
pub fn ks_define_const_thm(KernelState, String, HolType, Term) -> Result[(KernelState, Thm), SigError]

副条件は次のとおり。c は予約されておらず、すでに定義されておらず、型定義に使われていない(ReservedSymbol、DefinitionAlreadyExists、TypeRepresentationAlreadyExists、TypeAbstractionAlreadyExists)。rhs は閉じている(DefinitionNotClosed)。rhs は c に、直接にも先行する定義を通じても言及しない(DefinitionIsCyclic)。ty は許容され(InvalidConstRhs)、rhs の型と等しい(TypeMismatch)。rhs のすべての型変数が ty に現れる(GhostTypeVariable)。rhs のすべての定数が、そのスキーマのインスタンスで宣言されている(InvalidConstRhs)。各条件が保存性のためになぜ必要かは、カーネル設計ノートに示されている。

`ks_definition_theorem` と `ks_has_def_head`

ks_definition_theorem は、定義された定数について記録された定義定理を返す。なければ Err(UnknownConst) を返す。ks_has_def_head は、名前が定義済みかどうかを検査する。

pub fn ks_definition_theorem(KernelState, String) -> Result[Thm, SigError]
pub fn ks_has_def_head(KernelState, String) -> Bool

`ks_register_type_definition`

ks_register_type_definition(state, tycon, params, rep, pred, witness) は型定義ゲート TypeDefOK である。表現型のうち pred で切り出される部分集合と全単射になる、アリティ params.length() の新しい型コンストラクタ tycon を許容する。

pub fn ks_register_type_definition(KernelState, String, Array[String], String, Term, Thm) -> Result[KernelState, SigError]

pred は、型変数が params に含まれる $P : \mathit{bool}$ を持つ閉じた抽象 $\lambda (x{:}\rho).\,P$ でなければならず、witness は閉じた項 w についての仮定なしの定理 $\vdash P[w/x]$ でなければならない。これは部分集合が空でないことを示す。成功すると、状態は rep : tycon(params) -> ρ と Abs_<tycon> : ρ -> tycon(params) を宣言し、ks_typedef_contract が返す契約定理を記録する。失敗は、違反した条件を示す。InvalidTypeParams、InvalidTypeArity、InvalidTypeRepName、InvalidTypeAbsName、TypeConstructorAlreadyExists、TypeRepresentationAlreadyExists、TypeAbstractionAlreadyExists、InvalidTypePredicate、TypeWitnessArityMismatch、InvalidTypeWitness、TypeWitnessPredicateMismatch、InvalidTypeDefinitionProduct。

`ks_typedef_contract` と `ks_has_typedef_contract`

ks_typedef_contract(state, tycon) は型定義の 3 つの契約定理を返す。なければ Err(MissingTypeDefinitionContract) を返す。ks_has_typedef_contract はそれがあるかを検査する。

pub fn ks_typedef_contract(KernelState, String) -> Result[(Thm, Thm, Thm), SigError]
pub fn ks_has_typedef_contract(KernelState, String) -> Bool

$\mathit{abs} = \texttt{Abs\_}\mathit{tycon}$ とすると、3 つの定理は順に次のとおりである。

\vdash \mathit{abs}(\mathit{rep}\,a) = a \qquad \vdash P[\mathit{rep}\,a / x] \qquad P[r/x] \vdash \mathit{rep}(\mathit{abs}\,r) = r

`ks_has_type_witness`、`ks_has_type_rep_head`、`ks_has_type_abs_head`

ks_has_type_witness(state, tycon, arity) は、そのアリティの型コンストラクタが許容されているかを検査する。ind は最初から許容されている。他の 2 つは、名前が型定義の表現関数または抽象関数であるかを検査する。

pub fn ks_has_type_witness(KernelState, String, Int) -> Bool
pub fn ks_has_type_rep_head(KernelState, String) -> Bool
pub fn ks_has_type_abs_head(KernelState, String) -> Bool

`ks_specify_const`

ks_specify_const(state, c, ty, pred, witness) は特殊化ゲート SpecOK である。 $\vdash P[w/x]$ が与えられたとき、定数 c : ty を導入し、 $\vdash P[c/x]$ を返す。

pub fn ks_specify_const(KernelState, String, HolType, Term, Thm) -> Result[(KernelState, Thm), SigError]

このゲートは選択演算子と DefOK から導出される。ks_define_const_thm を通じて $c = (@\,\mathit{pred})$ を定義するため、状態には DefOK 証明書に続いて SpecOK 証明書が記録される。pred は ty 上の閉じた抽象で、ty の外に型変数を持ってはならず(InvalidSpecificationPredicate、SpecificationTypeVarLeak)、witness は閉じた項での述語についての仮定なしの定理でなければならない(InvalidSpecificationWitness)。ks_define_const の定義条件が c に適用される。

`ks_register_ind_infinity_axiom`、`ks_ind_infinity_axiom`、`ks_has_ind_infinity_axiom`

ks_register_ind_infinity_axiom(state, anchor) は、ind についての定理を理論の無限性アンカーとして記録する。ks_ind_infinity_axiom はそれを返す。なければ Err(MissingInfinityAnchor) を返す。ks_has_ind_infinity_axiom は記録があるかを検査する。

pub fn ks_register_ind_infinity_axiom(KernelState, Thm) -> Result[KernelState, SigError]
pub fn ks_ind_infinity_axiom(KernelState) -> Result[Thm, SigError]
pub fn ks_has_ind_infinity_axiom(KernelState) -> Bool

アンカーはすでに Thm でなければならない。すなわち、仮定を持たず、許容され、ind に言及する命題である。したがって登録は新しい定理を追加せず、どの定理が無限性の仮定の役割を担うかを示すだけである。アンカーがすでに記録されている、または定理が条件を満たさない場合は InvalidInfinityAnchor で失敗する。

test "definitions" {
  let st = @kernel.empty_kernel_state()
  let bool = @kernel.bool_ty()
  let x = @kernel.mk_var("x", bool)
  let bb = @kernel.fun_ty(bool, bool)
  let (st1, def_th) = @kernel.ks_define_const_thm(st, "idb", bb, @kernel.mk_abs(x, x)).unwrap()
  inspect(
    @kernel.thm_to_string(def_th),
    content="[] |- Comb(Comb(Const(= : fun(fun(bool, bool), fun(fun(bool, bool), bool))), Const(idb#1 : fun(bool, bool))), Abs(bool. BVar(0 : bool)))",
  )
  inspect(@kernel.ks_has_def_head(st1, "idb"), content="true")
  // a name can be defined only once, and a definition must be closed
  inspect(
    @kernel.ks_define_const(st1, "idb", bb, @kernel.mk_abs(x, x)) is Err(@kernel.DefinitionAlreadyExists),
    content="true",
  )
  inspect(@kernel.ks_define_const(st, "k", bool, x) is Err(@kernel.DefinitionNotClosed), content="true")
  // λy. y = λy. y mentions the type variable B, which the type bool does not
  let y = @kernel.mk_var("y", @kernel.mk_tyvar("B"))
  let ghost = @kernel.mk_eq(@kernel.mk_abs(y, y), @kernel.mk_abs(y, y)).unwrap()
  inspect(@kernel.ks_define_const(st, "g", bool, ghost) is Err(@kernel.GhostTypeVariable), content="true")
}

test "specification" {
  let bool = @kernel.bool_ty()
  let st0 = @kernel.ks_add_const(@kernel.empty_kernel_state(), "t0", bool).unwrap()
  let t0 = @kernel.ks_mk_const(st0, "t0").unwrap()
  let x = @kernel.mk_var("x", bool)
  let pred = @kernel.mk_abs(x, @kernel.mk_eq(x, t0).unwrap()) // λx. x = t0
  let witness = @kernel.refl_checked(st0, t0).unwrap() // |- t0 = t0
  let (st1, th) = @kernel.ks_specify_const(st0, "c", bool, pred, witness).unwrap()
  inspect(
    @kernel.thm_to_string(th),
    content="[] |- Comb(Comb(Const(= : fun(bool, fun(bool, bool))), Const(c#2 : bool)), Const(t0#1 : bool))",
  )
  inspect(@kernel.ks_extension_cert_count(st1), content="2")
}

test "type definition" {
  let bool = @kernel.bool_ty()
  let st0 = @kernel.ks_add_const(@kernel.empty_kernel_state(), "t0", bool).unwrap()
  let b = @kernel.mk_var("b", bool)
  let pred = @kernel.mk_abs(b, @kernel.mk_eq(b, b).unwrap()) // every bool
  let t0 = @kernel.ks_mk_const(st0, "t0").unwrap()
  let witness = @kernel.refl_checked(st0, t0).unwrap() // |- t0 = t0
  let st1 = @kernel.ks_register_type_definition(st0, "copy", [], "rep_copy", pred, witness).unwrap()
  inspect(@kernel.ks_type_is_admissible(st1, @kernel.mk_tyapp("copy", [])), content="true")
  assert_eq(
    @kernel.ks_lookup_const(st1, "Abs_copy").map(@kernel.hol_type_to_string),
    Some("fun(bool, copy)"),
  )
  let (abs_rep, _, _) = @kernel.ks_typedef_contract(st1, "copy").unwrap()
  inspect(
    @kernel.term_to_string(@kernel.thm_concl(abs_rep).unwrap()),
    content="Comb(Comb(Const(= : fun(copy, fun(copy, bool))), Comb(Const(Abs_copy : fun(bool, copy)), Comb(Const(rep_copy : fun(copy, bool)), Var(a : copy)))), Var(a : copy))",
  )
}

監査とリプレイ

`ExtensionGate` と `ExtensionCert`

ExtensionGate は拡張を受理したゲートを表す。ExtensionCert は 1 回の受理の監査記録であり、ゲート、導入された名前、およびウィットネスまたは定義定理のダイジェストを持つ。

pub enum ExtensionGate {
  DefOK
  TypeDefOK
  SpecOK
}

pub type ExtensionCert = (ExtensionGate, Array[String], String)

`ks_extension_cert_count` と `ks_extension_cert_at`

これらの関数は、状態の証明書を受理順に読み出す。

pub fn ks_extension_cert_count(KernelState) -> Int
pub fn ks_extension_cert_at(KernelState, Int) -> (ExtensionGate, Array[String], String)?

証明書は何が起きたかを記録するだけであり、証明オブジェクトではなく、定理に変換することもできない。

`ks_conservative_replay_ok`

ks_conservative_replay_ok(base, extended, th) は実行可能な保存性検査である。これは、th が extended で許容され、base の言語で書かれた閉じた仮定なしの文であり、かつ base でも許容される場合に成り立つ。

pub fn ks_conservative_replay_ok(KernelState, KernelState, Thm) -> Bool

回帰テストはこれを用いて、拡張の後に証明されたが旧言語で述べられた定理が、旧理論でも依然として定理であることを確認する。

test "audit" {
  let bool = @kernel.bool_ty()
  let st0 = @kernel.empty_kernel_state()
  let x = @kernel.mk_var("x", bool)
  let id = @kernel.mk_abs(x, x)
  let (st1, _) = @kernel.ks_define_const_thm(st0, "idb", @kernel.fun_ty(bool, bool), id).unwrap()
  inspect(@kernel.ks_extension_cert_count(st1), content="1")
  let (gate, heads, _) = @kernel.ks_extension_cert_at(st1, 0).unwrap()
  inspect(gate is @kernel.DefOK && heads == ["idb"], content="true")
  // |- (λx. x) = (λx. x) does not mention idb: it replays in the base theory
  let th = @kernel.refl_checked(st1, id).unwrap()
  inspect(@kernel.ks_conservative_replay_ok(st0, st1, th), content="true")
}

エラー

`LogicError`

LogicError は、項コンストラクタと基本規則によって値として送出される。

pub suberror LogicError {
  TypeMismatch
  VariableCaptured
  NotAnEquality
  NotBoolTerm
  AlphaMismatch
  InvalidInstantiation
  VarFreeInHyp
  NotTrivialBetaRedex
  BoundaryFailure
  CapacityExceeded
}

コンストラクタ	意味
`TypeMismatch`	項の型が不正である、一致すべき型が異なる、または定数が状態に未知である。
`VariableCaptured`	代入値が自由でない束縛インデックスである。名前付き項から構築された値がそうなることはない。
`NotAnEquality`	等式であるべき前提または項が等式でない。
`NotBoolTerm`	命題であるべき項が別の型を持つ。
`AlphaMismatch`	α 同値であるべき項がそうでない。
`InvalidInstantiation`	代入の形が不正である、ABS の束縛子が変数でない、または定理が状態の定数同一性に適合しない。
`VarFreeInHyp`	ABS の変数が仮定中に自由に出現する。
`NotTrivialBetaRedex`	BETA に β 冗長式でない項が渡された。
`BoundaryFailure`	項を名前付き形式と de Bruijn 形式の間で変換できなかった。
`CapacityExceeded`	de Bruijn インデックスの計算がオーバーフローする。

`SigError`

SigError は、シグネチャ操作と拡張ゲートによって値として送出される。

pub suberror SigError {
  DuplicateConstName
  ConstTypeConflict
  InvalidConstInstance
  UnknownConst
  ScopeUnderflow
  InvalidConstRhs
  ReservedSymbol
  DefinitionAlreadyExists
  DefinitionNotClosed
  DefinitionIsCyclic
  GhostTypeVariable
  InvalidTypeWitness
  InvalidTypePredicate
  InvalidTypeRepName
  InvalidTypeAbsName
  InvalidTypeParams
  InvalidTypeArity
  TypeWitnessArityMismatch
  TypeWitnessPredicateMismatch
  TypeConstructorAlreadyExists
  TypeRepresentationAlreadyExists
  TypeAbstractionAlreadyExists
  InvalidInfinityAnchor
  MissingInfinityAnchor
  InvalidTypeDefinitionProduct
  MissingTypeDefinitionContract
  InvalidSpecificationWitness
  InvalidSpecificationPredicate
  SpecificationTypeVarLeak
  TypeMismatch
}

グループ	コンストラクタ
シグネチャ	`DuplicateConstName`, `ConstTypeConflict`, `InvalidConstInstance`, `UnknownConst`, `ScopeUnderflow`, `ReservedSymbol`, `TypeMismatch`
`DefOK`	`InvalidConstRhs`, `DefinitionAlreadyExists`, `DefinitionNotClosed`, `DefinitionIsCyclic`, `GhostTypeVariable`
`TypeDefOK`	`InvalidTypeWitness`, `InvalidTypePredicate`, `InvalidTypeRepName`, `InvalidTypeAbsName`, `InvalidTypeParams`, `InvalidTypeArity`, `TypeWitnessArityMismatch`, `TypeWitnessPredicateMismatch`, `TypeConstructorAlreadyExists`, `TypeRepresentationAlreadyExists`, `TypeAbstractionAlreadyExists`, `InvalidTypeDefinitionProduct`, `MissingTypeDefinitionContract`
`SpecOK`	`InvalidSpecificationWitness`, `InvalidSpecificationPredicate`, `SpecificationTypeVarLeak`
無限性アンカー	`InvalidInfinityAnchor`, `MissingInfinityAnchor`

どちらのエラー型も値である。このページの例のように、is または match で照合する。

kernel API リファレンス

型

HolType

mk_tyvar

mk_tyapp

bool_ty、ind_ty、fun_ty

dest_tyapp と dest_fun_ty

is_bool_ty、is_tyvar、is_tyapp

ty_eq

tyvars と tyvars_subset

ty_is_instance_of

type_subst、type_subst_unsafe、has_duplicate_ty_subst_keys

hol_type_to_string

項

Term

mk_var、mk_const、mk_const_bound、mk_comb、mk_abs

is_var、is_const、is_comb、is_abs

dest_var、dest_const、dest_comb、dest_abs

type_of

mk_eq と dest_eq

free_vars、term_is_closed、term_has_const_named

term_tyvars と term_tyvars_subset

term_apply_ty_subst と term_apply_ty_subst_unsafe

term_alpha_eq と term_logical_eq

term_to_string

de Bruijn 項

DbTerm

to_db_term と from_db_term

db_term_eq、db_type_of、db_term_to_string

db_has_free

db_subst_free_parallel

db_apply_ty_subst

db_beta_reduce_once

定理

Thm

thm_hyps、thm_concl、thm_hyp_count

thm_to_string

thm_is_admissible と thm_bind_const_ids

基本規則

refl_checked

assume_checked

add_assum_checked

trans_checked

mk_comb_rule_checked

abs_rule_checked

beta_rule_checked

eq_mp_checked

deduct_antisym_rule_checked

inst_type

inst_checked