このREWR_CONV(: thm -> term -> thm = )を先のdepth conversions(: conv -> conv = )のもとで用いれば，等式についてのtheoremから導ける限りのtermの書き換えが可能になります． 例えば # let tm = `(a + b) + ((c + d) + e) + f + g + h` ;; val tm : ter…

|- p ==> q と |- p から |- q を得るMP(: thm -> thm -> thm = )を用いる際 # LT_IMP_LE;; val it : thm = |- !m n. m m # MP (SPECL[`1`;`2`] it) (ARITH_RULE`1 val it : thm = |- 1 のように，SEPC(: term -> thm -> thm = )，SEPCL(: term list -> thm …

termの中に現れるtermのconversionには，個々のconvを適用する位置や回数，順序などを指定するconversional関数(: conv -> conv = )を用います． RAND_CONV conv tm における RAND_CONV は，tm内のrand tmにconvを適用します．例えば rand `1 + 2 + 3`;; val…

conversionsによる処理の優位性は，それらを制御して，より複雑なconversionを生成するconversionalと呼ばれる関数(: conv -> conv = )の存在にあります． 今回はその中でも，複数のconversionsを組み合わせるものを紹介します．■ まず，次に定義するTHENC関…

HOL Lightは，あるtermが別のtermと等価である（:numなどの場合は=，:boolの場合はで結ばれる）ことを，体系的な変形を経て示す為，様々なconversionsを提供します． conversionはterm -> thm typeの関数で，typeはARITH_RULEやMESON[]などのproverと同じで…

量化子のネストにおいて変数の依存関係に注意が必要であることは，連続と一様連続との違いを持ち出すまでもなく，明らかでしょう． さて，先に述べたトートロジーprover TAUTでは，自明でない量化された式の評価はできません，HOL Light には，model elimina…

HOL Lightの変数の束縛は，abstractionによるもののみですから，例えば，全称量化子 `(!)` も，述語Pをlambda-abstractionと見て，それが任意のxに対して，Tを返すlambda-abstraction (\x.T) と一致することとして定義されます． # FORALL_DEF;; val it : th…

(* 本章より，入力行の先頭の#記号も記しますが，それ自体は入力ではありません．*) 前の章の最初に挙げたtermの４つの目の種類，abstractionsについて述べます． 3.3で紹介したINSTのtypeは # INST;; val it : (term * term) list -> thm -> thm = なので，…

HOL Lightでは新たなconstant（固定された数や関数など）を定義することもできます．それにはnew_definition関数を用いて，その定義をtheoremにすればよいのです． let def_of_wordlimit = new_definition `wordlimit = 2 EXP 32`;; val def_of_wordlimit : …

ここでSYMがどのように定義されているかを見るため，幾つか準備します． ・先の挙げたMPの等式版関数にEQ_MPがあり，それは A |- p ⇔ q と B |- p から A∪B |- q を得るもので let e1=ARITH_RULE `1=1 1+1=2`;; val e1 : thm = |- 1 = 1 1 + 1 = 2 let e2 =A…

HOL Lightにおいて等式は，数学におけるそれよりも特に基本的です．例えば，Iffは=記号にしても構いません．ただし，結合の強さと向き，typeの推量機能のため，時に括弧が必要です． `p /\ x = 1 q`;; val it : term = `p /\ x = 1 q` `p /\ x = 1 = q`;; va…

curringは，OCamlの殆ど，HOL Lightの全ての中置き２項演算子に使われていますが，順序対がないわけではなく，OCaml，HOL Light，それぞれにおいて # 1,2;; val it : int * int = (1, 2) # type_of `1,2`;; val it : hol_type = `:num#num` のようになってい…

例えば，OCamlの加法演算子を引数なしで呼ぶと (+);; val it : int -> int -> int = 同じく，HOL Lightの加法の演算子のhol_typeを見ると type_of `(+)`;; val it : hol_type = `:num->num->num` のようと表示されます．これは例えば「x+1」が，x に対して「…

ここまでの段階でもtermはかなり複雑に見えるかも知れませんが，根本的には次の４種に過ぎません． ・Variables （`x:bool`や`n:num`など） ・Constants （`T`や`(~)`など） ・Applications （`~p`のような演算子を変数に作用させて得られるtermの組合せ）こ…

TAUTのような高い自動性をもつ規則関数と同様，HOL Lightには，繊細な推論用の「導入」と「除去」の規則関数があります． まず，２つのtheorem，A |- p，B |- qからtheorem A∪B |- p∧q を得る規則，つまり，∧を導入するのがCONJです． let thp = ASSUME `p:b…

命題論理の定理式（意味論での恒真式）のproverがTAUTであり，任意の定理式を証明してくれます． TAUT`((p==>q)==>p)==>p`;; val it : thm = |- ((p ==> q) ==> p) ==> p 書き忘れていましたが，HOL Lightは普通の数学と同じく，古典論理を採用していますの…

HOL Lightの命題論理は一般的なものであり，命題定数は F (Falsity) T (Truth) 論理記号は ~ (Not) さらに結合の強い順に /\ (And) \/ (Or) ==> (Implies) (Iff) で，同じ結合記号どうしは右結合，formula，および，truth valuesの設定もごく普通のものです…

ここまでの道具だけで，自明でない定理を証明することはやや辛いです．しかし，HOL Lightには，強力な推論規則により自明でない定理を自動的に証明するproverが実装されています． その一つ，ARITH_RULE関数は，自然数（非負整数）の代数的な順序交換と線形…

述語論理のformulaに当たるtermのhol_typeは `x+1 であり `2+2=5`;; val it : term = `2 + 2 = 5` もhol_typeがboolのtermです． これまでの例からも判る通り，HOL Lightは入力されたtermを直ちには評価しません（Mathematicaなら 2+2は4，2+2=5はFalseと返…

ところが subst[`2`,`x`]`x+1`;; Warning: inventing type variables val it : term = `x + 1` のように上手く行きません．このWarningはterm xのhol_type（というOCamlでのtype）が不明ということなので，例えば，num（自然数，非負整数）と明示すれば subs…

termの例を挙げます． `x+1`;; val it : term = `x + 1` `(x)+1`;; val it : term = `x + 1` ` x + ( 1 ) `;; val it : term = `x + 1` これらはいずれも同じtermで，その内部表現は # remove_printer print_qterm;; `x+1`;; val it : term = ... # install_…

前回お話したtoplevel loopにおいてできることの２つ目は，evaluate expressions，つまり，数や文字列の評価でした． 「HOL Lightは，これに加えて，数学的陳述や論理的主張を表す「term」と，証明済みの主張を表す「theorem」を評価するツールの集まりです…

今回からしばらく 『HOL Light Tutorial (for version 2.20)』 http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf に従って話を進めます．なお，リファレンスはこちら 『The HOL Light System REFERENCE』 (For HOL Light 2.20++ November 2, 2011…

話が前後しますが，HOL Lightの紹介です． 私の学生時代の愛読書に『数学の基礎』（日本評論社）という島内剛一先生の労作があります．これは初等超越関数までを数理論理の手法により構成したもので，現在においても類書のない一冊だと思います． 一方，計算…