証明譜とは

証明譜 (proof score) とは、ある仕様において、ある表明が成立することを CafeOBJ に証明させるための指示を記述したテキストである。証明譜には、主に次のようなことを記述する:

• 証明に使用するモジュールの指定
• あるソート上の任意の要素を表す定数 (＝変数のように振舞う)
• 場合分け
• 補題
• (帰納法を用いるならば) 帰納法の仮定
• 簡約の指示

さらに付け加えると、証明譜では特にコメントが重要である。証明譜を用いた証明の正しさは、証明者 (人) が責任を負う。従って、証明譜には十分なコメントを記述し、人にとっての読みやすさを考慮する必要がある。コメントの書き方などは各自が工夫してほしい。

例として、自然数の仕様において、+ に結合律が成立することを証明する証明譜は、以下の通りである:

-- CLAIM: associativity over _+_
--        \forall i, j, k \in Nat: (i + j) + k = i + (j + k)
-- will be proven by induction on i.

-- PROOF:

open NAT+ + EQL .

-- declaring three arbitrary numbers i,j and k on the sort Nat:
ops i j k : -> Nat .

-- base step:
red ((0 + j) + k) = (0 + (j + k)) .
--> should be true.

-- induction hypothesis:
eq (i + j) + k = i + (j + k) .
-- inductive step:
red ((s(i) + j) + k) = (s(i) + (j + k)) .
--> should be true.

close

-- Q.E.D.

証明譜の詳しい説明は後にまわし、まずは証明譜を実行させた時の様子を見ることにする。この証明譜を simple-nat-proof-assoc.mod としてファイルに保存し、in コマンドで読み込ませて実行すると、次のような結果が得られる:

CafeOBJ> in simple-nat-proof-assoc.mod
processing input : /Users/seino/simple-nat-proof-assoc.mod_*
-- opening module NAT+ + EQL.. done._*
-- reduce in %NAT+ + EQL : (0 + j) + k = 0 + (j + k)
true : Bool
(0.003 sec for parse, 3 rewrites(0.002 sec), 11 matches)
--> should be true.*
-- reduce in %NAT+ + EQL : (s(i) + j) + k = s(i) + (j + k)
true : Bool
(0.004 sec for parse, 5 rewrites(0.003 sec), 26 matches)
--> should be true.
CafeOBJ> 

基底と帰納段階の推論を行う 2回の簡約のいずれも期待した結果 (true) が得られたので、+ には結合律が成立することが証明できたことがわかる。

[Next] 組み込み述語 =

Original Copyright © Takahiro Seino, all rights reserved.