bookの仕様
bookにはいろいろなデータが並びます。
wordの紹介に続いてその定義となるPropが置かれることは頻出します。
word,PropなどはDBにあるものを置くのが通常ですが、オリジナルのものを置くこともできます。
hiddenデータと呼ばれる、web上には表示させないデータを置くことも多々あります。
あるThmに対しその証明を記述したものはPrfと呼ばれ、hiddenでかなり長くなることがあります。
book内で使用される自動変数もあります。
例えば \(\mathbb{W}\) は「そこまでで、\(\mathbb{W}\)( , ) … の形で紹介されたすべてのwordの列」です。
set\({\tt n}\) がbookで紹介されると、その時点で \(\mathbb{W}\) は無限列になります。
\(\mathbb{W}.\) は「\({\tt w}.\) (\({\tt w}\)は\(\mathbb{W}\)) のすべての列」です。\({\tt P}\) ◀ \(\mathbb{W}.\) は「定義から\({\tt P}\)が示される」と読まれます。
bookを作成する際はソースファイルに記述します。拡張子は .book です。
それをコンパイルするとweb形式の表示が得られ、「査読ボタン」も出てきます。
bookの書法については、こちら。
book査読器
book査読器はこのシステムで最も偉いソフトになります。
それはデータの並びに不整合な所がないかをチェックします。
例えば「未紹介のwordがないか」「ThmのPrfは正しいか」などです。
book査読器はbookを上から読んでいきデータを記憶していきますが、book内変数も保持します。
なお、bookには好みで「説明」を入れて良いですが、査読器では無視されます。
各bookは独立し自己完結していなければなりません。
例えばPrfチェックでは「そのbook内にあるものだけで通るか？」を見ます。
PrfはThmの列になります。ただし ◀ ではなく、P◀, V◀, H◀ などが使われます。
これは「Prfのチェック時に何に投げるか」も記述したものです。
上のものは Prover9, Vampire, Hyperion に投げること意味します。
Prover9, Vampireは一階論理による推論をします。Hyperionはメタ推論をします。
ThmとそのPrfの例①
「和集合の定義」 は次です。∪. … \(X \cup Y = \{ x \mid x \in X \mathbin{\rm o\!r} x \in Y \}\)
一般には \(\mathbb{W}.\) は無限列になるので次のThm単独でチェックを通すことはできません。
\(X \cup X = X\) ◀ \(\mathbb{W}.\)
しかし、次の3行のPrfはチェックを通せます。
goal := \(X \cup X = X\)
goal P◀ =. , cup.
goal H◀ \(\mathbb{W}.\)
1行目はPrf内変数 goal の宣言です。
2行目に対しては、次が返ってきます。 % Length of proof is 16.\(\dagger\)
3行目に対しては、=. と ∪. が\(\mathbb{W}.\)に入っていることを確かめられれば、2行目の結果と合わせて OK が返ってきます。
ThmとそのPrfの例②
「\({\tt w}\)の定義による展開」を行う / \({\tt w}\). が証明において有用です。\(X \cup X = X\) / =. = \(\forall x \, ( x \in X \cup X \Leftrightarrow x \in X )\)
\(X \cup X = X\) / =. / ∪. = \(\forall x \, ( x \in X \mathbin{\rm o\!r} x \in X \Leftrightarrow x \in X )\)
この計算は、具体的にどのwordの定義を使うかを記述せず // \(\mathbb{W}.\) としても実行されます。
上のThmのPrfは、次の3行にした方が良いです。
goal := \(X \cup X = X\)
goal // \(\mathbb{W}.\) P◀ O
goal H◀ \(\mathbb{W}.\)
2行目に対しては、次が返ってきます。 % Length of proof is 6.
一般にProver9にはsosが少ないThmを投げた方が良いです。
Hyperionは goal ◀ goal // \(\mathbb{W}.\) , \(\mathbb{W}.\) というThmの生成ができ、最初のPrfより速く3行目を処理するでしょう。
終わりに
Prfチェックはbook査読の中で最も重要で、文字通り「機械的に」行われます。「Thmが正しいか」について、人手では追い切れない規模と精度で検査できます。\(\dagger\)
Matheliaとエージェントを使えば、全く新しい数学を作ることも夢ではないはずです。
使ってみたい方はぜひ 代表：須田智彦[t@mshk1201.com]まで。