HOL Lightの実装を理解したい(0)
理解したい。問題は、OCaml読めないことと、HOL Lightが、どういうものか微塵も分からんので、とりあえず、HOL Lightを動かしてみたメモ。ソースコード落とすと、中にTutorialがあるので適当に見れば良い気がする。
Coqと双璧をなすかどうかは知らないけど、HOL系のproof assistantは、よく見かける。Isabelle/HOLというのが一番(？)有名っぽい。こいつは
seL4という、マイクロカーネルタイプOSの形式検証
https://github.com/seL4/l4v
とかいう実績があるらしい。
HOL Lightは、
Kepler予想の証明を形式化したflyspeckプロジェクト
https://github.com/flyspeck/flyspeck
で使われたらしい。
HOL Light開発の経緯として
https://en.wikipedia.org/wiki/HOL_(proof_assistant)
には、'The second current implementation is HOL Light. This started as an experimental "minimalist" version of HOL. Although it has subsequently grown into another mainstream HOL variant, its logical foundations remain unusually simple.'と書いてある。Isabelleで書かれた証明とHOL Lightの証明は、全く似てなかったりするけど、できることは、基本的に同じと考えて、差し支えなさそう？
Towards self-verification of HOL Light
https://www.cl.cam.ac.uk/~jrh13/papers/holhol.html
の冒頭には"The HOL Light prover is based on a logical kernel consisting of about 400 lines of mostly functional OCaml, whose complete formal verification seems to be quite feasible."という一文がある。別にformal verificationしたいとは思わないのだけど、400行なら、なんか理解する気になると思った(あと、apt-get install hol-lightってしたらインストールされたので)
# HOL Lightのソースは
The HOL Light theorem prover (moved from Google code)
https://github.com/jrh13/hol-light
で公開されている。この中のfusion.mlが、『400行程度のlogical kernel』に相当する部分っぽい？コメント入れて670行くらい。冒頭で、lib.mlというのが、参照されているっぽいけど、curryだのuncurryだのの関数とか、リスト操作関連関数が定義されているだけ。Wikipediaの
HOL Light#Logical Foundations
https://en.wikipedia.org/wiki/HOL_Light#Logical_foundations
にあるのと、同じ名前の関数が定義されている(REFLとかMK_COMBとかetc.)。大体わかった(適当
HOL LightとCoqで、どういう差があるのか、よく分かってないけど、HOL Lightでは
・命題はただのブール値であり排中律が成立する
・functional exntensionalityが成立する
・選択公理も成立する(?)
・依存型はない
という感じであるらしい。
HOL Lightの例1。
# let thp= ASSUME `p:bool`;; val thp : thm = p |- p # let thq = ASSUME `q:bool`;; val thq : thm = q |- q # let thpq = CONJ thp thq;; val thpq : thm = p, q |- p /\ q
何をしてるかは見ればわかる。`...`は、何かtermというものになるっぽい
# let t0 = `x+1`;; val t0 : term = `x + 1` # `1+2`;; val it : term = `1 + 2`
実数(というか浮動小数点数？)はダメらしい
# `3.4`;; Exception: Failure "Unparsed input following term".
何もつけないと
# 3;; val it : int = 3
となる。簡単な計算もできる
# (NUM_REDUCE_CONV `2 + 2`);; val it : thm = |- 2 + 2 = 4
fusion.ml見ても、ASSUMEはあるけど、CONJはないし、NUM_REDUCE_CONVもない。CONJはbool.mlに定義されている
let CONJ =
let f = `f:bool->bool->bool`
and p = `p:bool`
and q = `q:bool` in
let pth =
let pth = ASSUME p
and qth = ASSUME q in
let th1 = MK_COMB(AP_TERM f (EQT_INTRO pth),EQT_INTRO qth) in
let th2 = ABS f th1 in
let th3 = BETA_RULE (AP_THM (AP_THM AND_DEF p) q) in
EQ_MP (SYM th3) th2 in
fun th1 th2 -> substitute_proof (
let th = INST [concl th1,p; concl th2,q] pth in
PROVE_HYP th2 (PROVE_HYP th1 th))
(proof_CONJ (proof_of th1) (proof_of th2));;なるほど、よく分からん。これの少し上の方に
let AND_DEF = new_basic_definition `(/\) = \p q. (\f:bool->bool->bool. f p q) = (\f. f T T)`;;
というのがある。やりたいことはわかる
termの型はtype_ofで取れる
# type_of `1`;; val it : hol_type = `:num` # type_of `1=2`;; val it : hol_type = `:bool` # type_of `[1,2,3]`;; val it : hol_type = `:(num#num#num)list`
hol_typeはfusion.mlで定義されている
type hol_type = Tyvar of string
| Tyapp of string * hol_type listだと思う
自然数は最初から組み込まれているが、自分で定義する場合は、以下のようにするとできる。
# let nat_ind , nat_rec = define_type "Nat = Zero | Suc Nat";; val nat_ind : thm = |- !P. P Zero /\ (!a. P a ==> P (Suc a)) ==> (!x. P x) val nat_rec : thm = |- !f0 f1. ?fn. fn Zero = f0 /\ (!a. fn (Suc a) = f1 a (fn a))
これで、
# type_of `Zero`;; val it : hol_type = `:Nat` # type_of `Suc Zero`;; val it : hol_type = `:Nat`
とか、使えるようになる。
一方、組みこまれてる奴は
# type_of `SUC`;; val it : hol_type = `:num->num` # mk_comb(`SUC`,`0`);; val it : term = `SUC 0`
という感じ。
組み込みのnumの方は
# NUM_REDUCE_CONV `(SUC 0)`;; val it : thm = |- SUC 0 = 1
勝手に、human-friendlyな方に正規化してくれる。
帰納法。HOL LightにもCoq同様、tacticがある。forall(x:num),x+0=xは
# let thm0 = prove(`!x.x+0=x`,INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES]);; val thm0 : thm = |- !x. x + 0 = x
のように書ける(!はforallを表す)。proveは以下の型を持つ関数
# prove;; val it : term * tactic -> thm = <fun>
ほとんどの(多分全ての)人類は極めてIQが低く愚かなので、複雑なケースではtacticを一発で書くのは難しい。Coqのように、subgoalを確認しながら進める場合
# g `!x.x+0=x`;; val it : goalstack = 1 subgoal (1 total) `!x. x + 0 = x` # e INDUCT_TAC;; val it : goalstack = 2 subgoals (2 total) 0 [`x + 0 = x`] `SUC x + 0 = SUC x` `0 + 0 = 0` # e (ASM_REWRITE_TAC[ADD_CLAUSES]);; val it : goalstack = 1 subgoal (1 total) 0 [`x + 0 = x`] `SUC x + 0 = SUC x` # e (ASM_REWRITE_TAC[ADD_CLAUSES]);; val it : goalstack = No subgoals # let thm1 = top_thm();; val thm1 : thm = |- !x. x + 0 = x
numはnums.mlで定義されている
let NUM_REP_RULES,NUM_REP_INDUCT,NUM_REP_CASES =
new_inductive_definition
`NUM_REP IND_0 /\
(!i. NUM_REP i ==> NUM_REP (IND_SUC i))`;;
let num_tydef = new_basic_type_definition
"num" ("mk_num","dest_num")
(CONJUNCT1 NUM_REP_RULES);;
let ZERO_DEF = new_definition
`_0 = mk_num IND_0`;;
let SUC_DEF = new_definition
`SUC n = mk_num(IND_SUC(dest_num n))`;;だと思う。
# num_tydef;; val it : thm * thm = (|- mk_num (dest_num a) = a, |- NUM_REP r <=> dest_num (mk_num r) = r)
nums.mlのもうちょっと下の方を見ると
# prove(`_0 = 0`,REWRITE_TAC[NUMERAL]);; val it : thm = |- _0 = 0
みたくできるのがわかる。NUMERALの定義は
# NUMERAL;; val it : thm = |- !n. NUMERAL n = n # type_of `NUMERAL`;; val it : hol_type = `:num->num`
となっている。紛らわしいけど、項としてのNUMERALは、numからnumへの関数で、定理NUMERALは、単にそれが恒等関数であることを主張している。
let NUMERAL =
let num_ty = type_of(lhand(concl ZERO_DEF)) in
let funn_ty = mk_fun_ty num_ty num_ty in
let numeral_tm = mk_var("NUMERAL",funn_ty) in
let n_tm = mk_var("n",num_ty) in
new_definition(mk_eq(mk_comb(numeral_tm,n_tm),n_tm));;なので、 `!n. NUMERAL n = n`は実際にはNUMERALの定義なのだと思う。で、`0`は内部的には`NUMERAL _0`として扱われているっぽい
tactic嫌いな人間は
# INST [`_0` ,`n:num`] (List.hd(mk_rewrites false NUMERAL []));; val it : thm = |- 0 = _0
のようにやる。
線形代数をやることを考える。Multivariate/vector.mlに色々定義がある。realという型は、起動時点で作られている。
# needs "Multivariate/vectors.ml";;
とか打つと、何か一杯出てきて使えるようになる。で
# `!x:real^N. x dot x >= real(0)`;; val it : term = `!x. x dot x >= real 0`
と書けるようになる。しかしNってなんだ。どっから来たんだって感じである
# types();;
val it : (string * int) list =
[("4", 0); ("3", 0); ("2", 0); ("finite_sum", 2); ("cart", 2);
("finite_image", 1); ("int", 0); ("real", 0); ("hreal", 0); ("nadd", 0);
("char", 0); ("list", 1); ("option", 1); ("sum", 2); ("recspace", 1);
("num", 0); ("ind", 0); ("prod", 2); ("1", 0); ("bool", 0); ("fun", 2)]を見てもいない。
別に、Nじゃなくてもいいらしい
# `!x:real^M. x dot x >= real(0)`;; val it : term = `!x. x dot x >= real 0` # `!x:real^hoge. x dot x >= real(0)`;; val it : term = `!x. x dot x >= real 0`
以下は、正しくない命題だが
# `!x:real^N.x dot x < real (dimindex(:N)) `;; val it : term = `!x. x dot x < real (dimindex (:N))`
とか書ける。HOL Lightは依存型とかがないので、"forall (n:num) (u v:real^n),...."みたいなことが書けない。代わりに、(実)n次元ベクトル空間を{1,2,...,n} -> realみたいな関数と同一視する。"forall (X:Type) (u v:X->real),..."みたいには書けないけど、HOL Lightでは、forall (u v :X->real),...みたいに書いてあると、Xは型なんだなと推論してくれる仕組みがあるっぽい？(嘘かも)。考えてみると、リストを操作する関数とかで、こういう多相関数を許す仕組みがないと、辛いことになる
fusion.mlにあるmk_vartypeというのを使うと
# mk_vartype "X";; val it : hol_type = `:X`
というのが作れる。内部的には、(Tyvar "X")という風になっているはず。"HOL Light: an overview"という論文に"HOL Light's logic is simple type theory with polymorphic type variables"と書いてあって、polymorphic type variablesというのは、このTyvarを指しているっぽい。
dimindexはcart.mlで定義されているけど
let dimindex = new_definition `dimindex(s:A->bool) = if FINITE(:A) then CARD(:A) else 1`;;
みたいに書いてある。dimindexとかFINITEとか、直接、型を引数に取ることはできないのだけど、sets.mlで
# UNIV;; val it : thm = |- (:A) = (\x. T)
みたいのが定義されている。で、printer.ml見ると
(* Print the universal set UNIV:A->bool as "(:A)". *)
とか書いてあったり。なんか、そういうtrickが使われている
そんなわけで
# `!f:A->B x:A.f(x)=f(x)`;; val it : term = `!f x. f x = f x`
もOK.
自明だけど証明してみる
# g`!f:A->B x:A.f(x)=f(x)`;; val it : goalstack = 1 subgoal (1 total) `!f x. f x = f x` # e STRIP_TAC;; val it : goalstack = 1 subgoal (1 total) `!x. f x = f x` # e STRIP_TAC;; val it : goalstack = 1 subgoal (1 total) `f x = f x` # e REFL_TAC;; val it : goalstack = No subgoals
まとめ。Coq使ったことある人は、あまり戸惑うこともなさそうな感じ。実装も、かなり単純で、読めば大体分かる気がする(読んだことあるproof assistantの実装が、HOL Lightとcubical interpreterしかないけど、cubical interpreterは、それほど自明じゃない感じがある)。proof assistant使ったことない人には、あまり親切とは言えないと思う(そもそも、情報が少ない)。flyspeckの人は、なぜHOL Lightを選んだのか謎である。
