Isabelle Tutorial その9
3.4 Advanced Datatype
3.4.1 Mutual Recursion
相互再帰するデータ型の例として、算術式とブール式を示します。算術式には条件文が含まれており、よってブール式が含まれています。またブール式には値の比較が含まれており、よって算術式が含まれています。相互再帰するデータ型の定義はandで繋げて記述します。
datatype 'a aexp = IF "'a bexp" "'a aexp" "'a aexp"
| Sum "'a aexp" "'a aexp"
| Diff "'a aexp" "'a aexp"
| Var 'a
| Num nat
and 'a bexp = Less "'a aexp" "'a aexp"
| And "'a bexp" "'a bexp"
| Neg "'a bexp"
この式の評価関数は次のように定義します。
primrec evala :: "'a aexp => ('a => nat) => nat" and
evalb :: "'a bexp => ('a => nat) => bool" where
"evala (IF b a1 a2) env = (if evalb b env then evala a1 env else evala a2 env)" |
"evala (Sum a1 a2) env = (evala a1 env + evala a2 env)" |
"evala (Diff a1 a2) env = (evala a1 env - evala a2 env)" |
"evala (Var a) env = env a" |
"evala (Num n) env = n" |
"evalb (Less a1 a2) env = (evala a1 env < evala a2 env)" |
"evalb (And b1 b2) env = (evalb b1 env & evalb b2 env)" |
"evalb (Neg b) env = (~ evalb b env)"
データ型が相互再帰しているため、評価関数も相互に参照する必要があります。よってこちらもandで繋げて記述します。
同様に、置換関数を定義します。
primrec substa :: "('a => 'b aexp) => 'a aexp => 'b aexp" and
substb :: "('a => 'b aexp) => 'a bexp => 'b bexp" where
"substa s (IF b a1 a2) = IF (substb s b) (substa s a1) (substa s a2)" |
"substa s (Sum a1 a2) = Sum (substa s a1) (substa s a2)" |
"substa s (Diff a1 a2) = Diff (substa s a1) (substa s a2)" |
"substa s (Var a) = s a" |
"substa s (Num n) = Num n" |
"substb s (Less a1 a2) = Less (substa s a1) (substa s a2)" |
"substb s (And b1 b2) = And (substb s b1) (substb s b2)" |
"substb s (Neg b) = Neg (substb s b)"
最初の引数は置換する変数から式へのマップです。置換の結果、変数の方は'aから'bに変わります。
式aをマップsで置換してから環境envで評価した結果と、式aを、全ての変数xをs(x)に置き換えた環境envで評価した結果が同じであることを証明します。もし算術式とブール式を別々に証明しようとすると、帰納ケースにおいてもう一方の定理が必要になります。従って両方の定義を同時に証明する必要があります。
lemma "evala (substa s a) env = evala a (% x. evala (s x) env) &
evalb (substb s b) env = evalb b (% x. evala (s x) env)"
apply(induct_tac a and b)
apply(simp_all)
done
相互再帰する複数の関数を帰納法で証明する場合は、例のようにそれぞれの変数をandで繋げて同時に適用します。
Exercise 3.4.1
型が'a expr => 'a exprである正規化関数normaを定義します。この関数はIF式の条件がLessのみとなるよう、AndとNegを取り除きます。次に、normaが評価結果を変えないことと、確かに正規化していることを証明します。
primrec norma :: "'a aexp => 'a aexp" and
normb :: "'a bexp => 'a aexp => 'a aexp => 'a aexp" where
"norma (IF b a1 a2) = normb b (norma a1) (norma a2)" |
"norma (Sum a1 a2) = Sum (norma a1) (norma a2)" |
"norma (Diff a1 a2) = Diff (norma a1) (norma a2)" |
"norma (Var a) = Var a" |
"norma (Num n) = Num n" |
"normb (Less a3 a4) a1 a2 = (IF (Less (norma a3) (norma a4)) a1 a2)" |
"normb (And b1 b2) a1 a2 = (normb b1 (normb b2 a1 a2) a2)" |
"normb (Neg b) a1 a2 = (normb b a2 a1)"
lemma "evala (norma a) env = evala a env &
(ALL a1 a2. evala (normb b a1 a2) env = evala (IF b a1 a2) env)"
apply(induct_tac a and b, simp_all)
done
primrec normala :: "'a aexp => bool" and
normalb :: "'a bexp => bool" where
"normala (IF b a1 a2) = (normalb b & normala a1 & normala a2)" |
"normala (Sum a1 a2) = (normala a1 & normala a2)" |
"normala (Diff a1 a2) = (normala a1 & normala a2)" |
"normala (Var a) = True" |
"normala (Num n) = True" |
"normalb (Less a1 a2) = (normala a1 & normala a2)" |
"normalb (And b1 b2) = False" |
"normalb (Neg b) = False"
lemma "normala (norma (a::'a aexp)) &
(ALL (a1::'a aexp) a2. normala a1 & normala a2 --> normala (normb b a1 a2))"
apply(induct_tac a and b, simp_all)
done
3.4.2 Nested Recursion
次に、ネストした再帰構造を見ます。例として、関数の引数をリストに変更した項を定義します。
datatype ('v, 'f)"term" = Var 'v | App 'f "('v, 'f)term list"
例えばf(x, g(y))はApp f [Var x, App g [Var y]]と表わします。'vと'fはそれぞれ変数と関数の型を示しています。
ネストした再帰的定義は相互再帰に変換して取り除くことができます。今回の例は次のように相互再帰で定義することもできます。
datatype ('v, 'f)"term" = Var 'v | App 'f "('v, 'f)term_list"
and ('v, 'f)term_list = Nil | Cons "('v, 'f)term" "('v, 'f)term_list"
元のネストした定義に戻り、置換関数を定義します。項のリストがあるため、二つの関数を同時に定義する必要があります。
primrec subst :: "('v => ('v, 'f)term) => ('v, 'f)term => ('v, 'f)term" and
substs :: "('v => ('v, 'f)term) => ('v, 'f)term list => ('v, 'f)term list" where
"subst s (Var v) = s v" |
subst_App:
"subst s (App f ts) = App f (substs s ts)" |
"substs s [] = []" |
"substs s (t#ts) = subst s t # substs s ts"
例のように、一つの等式にのみ名前を付けることができます。
項に関して帰納法で証明するには、項のリストについても同時に証明しなければなりません。例えば恒等関数で置換しても項が変わらないことを証明します。
lemma subst_id: "subst Var t = (t::('v, 'f)term) &
substs Var ts = (ts::('v, 'f)term list)"
apply(induct_tac t and ts, simp_all)
定義からわかるように、Varは変数の値を変えないため恒等関数です。また、型の指定をしなければそれぞれの式が同じ型であることを保証できないため、型の指定が必要です。
Exercise 3.4.2
合成関数による置換の分配法則はおおよそ次のようになります。
subst (f o g) t = subst f (subst g t)
oは関数の合成であり、定義はo_defで参照できます。しかしこの式は型違反ですので、修正し、証明します。
definition scomp :: "('v => ('v, 'f)term) => ('v => ('v, 'f)term) => ('v => ('v, 'f)term)" where
"scomp f g = (% x. subst f (g x))"
lemma "subst (scomp f g) t = subst f (subst g t) &
substs (scomp f g) ts = substs f (substs g ts)"
apply(induct_tac t and ts)
apply(simp_all add: scomp_def)
done
Exercise 3.4.3
全ての関数引数の順序を逆にする関数trevを定義し、trev (trev t) = tを証明します。
primrec trev :: "('v, 'f)term => ('v, 'f)term" and
tsrev :: "('v, 'f)term list => ('v, 'f)term list" where
"trev (Var v) = Var v" |
"trev (App f ts) = App f (tsrev ts)" |
"tsrev [] = []" |
"tsrev (t#ts) = (tsrev ts) @ [trev t]"
lemma [simp]: "tsrev (xs @ ys) = (tsrev ys) @ (tsrev xs)"
apply(induct_tac xs, simp_all)
done
lemma "trev (trev t) = (t::('t, 'f)term) &
tsrev (tsrev ts) = (ts::('t, 'f)term list)"
apply(induct_tac t and ts, simp_all)
done
substの定義において、substsは必要なく、Appケースは次のように定義できると考えるかもしれません。
subst s (App f ts) = App f (map (subst s) ts)
確かに正しいですが、Isabelleではこれを定義とすることができません。しかし、証明することはできます。
lemma [simp]: "subst s (App f ts) = App f (map (subst s) ts)" apply(induct_tac ts, simp_all) done
さらに、元の定義の等式による単純化を無効にすることができます。
declare subst_App [simp del]
substsをmapに置き換えることによって、mapに対して証明された多くの補題を活用することができます。残念ながらtermに対する帰納法の適用では、相変わらずsubstsの定義を用いなければなりません。これを解決するには、9.2.3で紹介する方法を使うか、あるいはprimrecではなくfunを使用して関数を定義する方法があります。funの説明はこの後登場します。
3.4.3 The Limits of Nested Recursion
HOLでは、次のような定義を作ることはできません。
datatype t = C "t => bool"
これは、型tとその冪集合t => boolが同じ濃度を持つという不可能なことを要求しているためです。同様の理由から、再帰にt setが含まれている場合にも、その定義を作ることはできません。
上の例のように再帰する型が関数の矢印の左側に出現する場合には定義できませんが、右側に出現する場合には定義できます。例として無限に枝分かれできるツリーを定義します。
datatype ('a, 'i)bigtree = Tip | Br 'a "'i => ('a, 'i)bigtree"
'aは値の型、'iは枝を選択するためのインデックスの型です。'iがboolならば二分木になります。
bigtreeの全てのラベルを変更する関数map_btを定義します。
primrec map_bt :: "('a => 'b) => ('a, 'i)bigtree => ('b, 'i)bigtree" where
"map_bt f Tip = Tip" |
"map_bt f (Br a F) = Br (f a) (% i. map_bt f (F i))"
map_btの再帰呼び出しには、サブツリーであるFしか含まれていません。よってこの関数が停止することを保証できます。% i. map_bt f (F i)をmap_bt f o Fと書けると思われるかもしれませんが、関数の停止性が明らかとは言えなくなるため、Isabelleはエラーを返します。
関数の矢印の左側にネストした再帰が必要な場合、HOLとは別の選択肢があります。Logic for Computable Functions(LCF)では、次のような型を定義できます。
datatype lam = C "lam => lam"
LCFはここではこれ以上取り上げません。
3.4.4 Case Study: Tries
ケーススタディとして、典型的な探索木であるトライを取り上げます。データ型、探索関数、更新関数を定義し、それらが正しく振る舞うことを証明します。
トライは文字列と値を関係付けます。値は最後のノードに結び付けられるため、多くのノードは値を持ちません。よってoption型を使ってモデル化します。また各ノードは文字からサブトライへの連想配列を持つとします。抽象化のため、文字と値はそれぞれ型パラメータにします。
datatype ('a, 'v)trie = Trie "'v option" "('a * ('a, 'v)trie)list"
次に、値と連想配列を取り出すための関数を定義します。
primrec "value" :: "('a, 'v)trie => 'v option" where "value (Trie ov al) = ov" primrec alist :: "('a, 'v)trie => ('a * ('a, 'v)trie) list" where "alist (Trie ov al) = al"
参照配列からの検索関数を定義します。検索が失敗する場合もあるので、結果はoption型にします。
primrec assoc :: "('key * 'val)list => 'key => 'val option" where
"assoc [] x = None" |
"assoc (p#ps) x = (let (a, b) = p in if a = x then Some b else assoc ps x)"
これで、トライに対する探索関数を定義できます。
primrec lookup :: "('a, 'v)trie => 'a list => 'v option" where
"lookup t [] = value t" |
"lookup t (a#as) = (case assoc (alist t) a of
None => None
| Some at => lookup at as)"
空のトライTrie None []に対する探索は常にNoneが返ることを証明します。証明は探索文字列の場合分けで行います。
lemma [simp]: "lookup (Trie None []) as = None" apply(case_tac as, simp_all) done
次に、更新関数を定義します。新しい文字列と値のペアを追加するか、あるいは文字列に対して値が既にある場合は上書きします。
primrec update :: "('a, 'v)trie => 'a list => 'v => ('a, 'v)trie" where
"update t [] v = Trie (Some v) (alist t)" |
"update t (a#as) v =
(let tt = (case assoc (alist t) a of
None => Trie None [] | Some at => at)
in Trie (value t) ((a, update tt as v) # alist t))"
帰納ケースではttが文字aに関連付けられたサブトライであり、これが再帰的に更新され、連想配列alist tの先頭に追加されます。古いサブトライは残ったままですが、lookupが連想配列の先頭から探索するため、アクセスされることはありません。振る舞いとしては正しいですが、このまま実装すると効率が悪いので、最適化する必要があるでしょう。最適化は後ほど取り上げます。
updateの定義にはlet式と、option型の場合分けが含まれています。そこで、updateについての性質を証明する前に、let式の展開と、option型のcase式の場合分けを自動で行うよう設定します。
declare Let_def [simp] option.split [split]
性質の証明に入ります。メインゴールは次の定理が示すように、updateとlookupが正しく振る舞うことです。
theorem "ALL t v bs. lookup (update t as v) bs =
(if as = bs then Some v else lookup t bs)"
証明はasについての帰納法から始めるため、残りの変数は限量化しています。帰納法の対象としてasとbsの二つの可能性がありますが、updateを先に単純化した方が、lookupの単純化が簡単になると思われるため、asを先とします。
apply(induct_tac as, auto)
三つのサブゴールが残りますが、基本的には同じ形をしています。
1. ... => lookup ... bs = lookup t bs 2. ... => lookup ... bs = lookup t bs 3. ... => lookup ... bs = lookup t bs
これを証明するにはbsを具象化する必要があり、そのためにはinduct_tacではなくcase_tacで場合分けする必要があります。
apply(case_tac[!] bs, auto)
これで証明が完了します。tacで終わるメソッドはそのまま使用すると最初のサブゴールにのみ適用されますが、適用するサブゴールを選択することができます。[n]とした場合はn番目のサブゴールに、[n-m]とした場合はn番目から[m]番目のゴールに、そして[!]とした場合は全てのサブゴールに適用されます。
Exercise 3.4.4
追加と削除の両方ができるようにupdateを修正し、先ほどの定理を証明します。また、可能であれば削除後にデータを圧縮するようにします。
primrec update :: "('a, 'v)trie => 'a list => 'v option => ('a, 'v)trie" where
"update t [] v = Trie v (alist t)" |
"update t (a#as) v =
(let s = (case assoc (alist t) a of
None => Trie None [] | Some at => at)
in if (v = None & s = Trie None [])
then t
else Trie (value t) ((a, update s as v) # alist t))"
declare Let_def [simp] option.split [split]
theorem "ALL t v bs. lookup (update t as v) bs =
(if as = bs then v else lookup t bs)"
apply(induct_tac as, auto)
apply(case_tac[!] bs, auto)
done
Exercise 3.4.5
前述のupdateでは上書きの際に古いサブトライが残っており無駄な領域を生んでいます。これを修正し、振る舞いが正しいことを証明し直します。
primrec replace :: "('k * 'v)list => 'k => 'v => ('k * 'v)list" where
"replace [] k v = [(k, v)]" |
"replace (p#ps) k v = (let (a, _) = p in
if a = k then (k, v)#ps else p#(replace ps k v))"
lemma [simp]: "assoc (replace xs k v) s =
(if k = s then Some v else assoc xs s)"
apply(induct_tac xs, auto)
done
primrec update :: "('a, 'v)trie => 'a list => 'v => ('a, 'v)trie" where
"update t [] v = Trie (Some v) (alist t)" |
"update t (a#as) v =
(let tt = (case assoc (alist t) a of
None => Trie None [] | Some at => at)
in Trie (value t) (replace (alist t) a (update tt as v)))"
declare Let_def [simp] option.split [split]
theorem "ALL t v bs. lookup (update t as v) bs =
(if as = bs then Some v else lookup t bs)"
apply(induct_tac as, auto)
apply(case_tac[!] bs, auto)
done
Exercise 3.4.6
文字からサブトライへのマップを連想配列(('a * ('a, 'v) trie) list)でモデル化しました。これを関数('a => ('a, 'v) trie)でモデル化します。
datatype ('a, 'v)trie = Trie "'v option" "'a => ('a, 'v)trie option"
primrec "value" :: "('a, 'v)trie => 'v option" where
"value (Trie ov al) = ov"
primrec alist :: "('a, 'v)trie => ('a => ('a, 'v)trie option)" where
"alist (Trie ov al) = al"
primrec lookup :: "('a, 'v)trie => 'a list => 'v option" where
"lookup t [] = value t" |
"lookup t (a#as) = (case (alist t) a of
None => None
| Some at => lookup at as)"
lemma [simp]: "lookup (Trie None (% x. None)) as = None"
apply(case_tac as, simp_all)
done
primrec update :: "('a, 'v)trie => 'a list => 'v => ('a, 'v)trie" where
"update t [] v = Trie (Some v) (alist t)" |
"update t (a#as) v =
(let tt = (case (alist t) a of
None => Trie None (% x. None) | Some at => at)
in Trie (value t) (% x. if x = a then Some (update tt as v) else (alist t) x))"
declare option.split [split]
theorem "ALL t v bs. lookup (update t as v) bs =
(if as = bs then Some v else lookup t bs)"
apply(induct_tac as, auto)
apply(case_tac[!] bs, auto)
done
3.5 Total Recursive Functions: fun
これまでの関数は全て原始再帰でしたが、ここからは原始再帰ではない再帰関数を扱います。全体再帰関数はfunで定義します*1。funではパターンマッチや、データ型を用いない再帰が使えます。また停止性は全ての再帰呼び出しの引数が「小さく」なっていることで証明されます。この節ではIsabelleが自動的に停止性を証明できる関数のみに限定します。停止性の証明を手動で行うこともできますが、ここでは扱いません。
3.5.1 Definition
例としてフィボナッチ関数を定義します。
fun fib :: "nat => nat" where "fib 0 = 0" | "fib (Suc 0) = 1" | "fib (Suc (Suc x)) = fib x + fib (Suc x)"
再帰呼び出しの度にfibの引数が小さくなっているため、Isabelleは停止性を自動的に証明できます。
別の例として、ある値をリスト要素の間に入れる関数を定義します。
fun sep :: "'a => 'a list => 'a list" where "sep a [] = []" | "sep a [x] = [x]" | "sep a (x#y#zs) = x # a # sep a (y#zs)"
今度はリストの長さが再帰呼び出しの度に小さくなっています。
パターンマッチが全域的になっている必要はありません。また、パターンマッチにワイルドカードを使うこともできます。
fun last :: "'a list => 'a" where "last [x] = x" | "last (_#y#zs) = last (y#zs)"
パターンマッチは定義の上から順に評価されます。よってマッチ可能なパターンが複数ある場合、最も上の等式がマッチします。
fun sep1 :: "'a => 'a list => 'a list" where "sep1 a (x#y#zs) = x # a # sep1 a (y#zs)" | "sep1 _ xs = xs"
再帰的ではない関数を定義することもできます。
fun swap12 :: "'a list => 'a list" where "swap12 (x#y#zs) = y#x#zs" | "swap12 zs = zs"
関数fをfunで定義すると、その等式(あるいは等式から導出された式)がf.simpsという名前で定理となり、さらに自動的に適用される単純化ルールにもなります。
3.5.2 Termination
funの停止性は引数のsizeに依存します。再帰関数は、すべての再帰呼び出しにおいてある引数のsizeが小さくなっていれば定義できます。
引数が複数ある場合は、サイズの辞書式の組み合わせ(lexicographic combination)も考慮されます。例えば次のようなアッカーマン関数も定義できます。
fun ack2 :: "nat => nat => nat" where "ack2 n 0 = Suc n" | "ack2 0 (Suc m) = ack2 (Suc 0) m" | "ack2 (Suc n) (Suc m) = ack2 (ack2 n (Suc m)) m"
3.5.3 Simplification
停止性の証明が終わると、等式は単純化ルールになります。しかし、これが問題を引き起こす場合があります。
fun gcd :: "nat => nat => nat" where "gcd m n = (if n = 0 then m else gcd n (m mod n))"
if式は自動的に場合分けされるため、else節にあるgcdの再帰呼び出しがその定義によって展開されます。従ってgcdについて単純化すると、展開が無限ループになってしまいます。
最も根本的な解決方法は、3.1.9で見たようにsplit_ifの自動適用を無効にすることです。しかしそうすると、他の場所にif式があったときに不便です。
gcdの定義をパターンマッチにすることで回避することもできます。例えば次のように定義できます。
fun gcd1 :: "nat => nat => nat" where "gcd1 m 0 = m" | "gcd1 m n = gcd1 n (m mod n)"
しかし、全ての場合のいてパターンマッチが使えるとは限りません。if式の代わりにcase式を使うこともできます。
fun gcd2 :: "nat => nat => nat" where "gcd2 m n = (case n = 0 of True => m | False => gcd2 n (m mod n))"
case式は自動的には場合分けされませんし、if式からcase式への置き換えは必ずできます。
最後に、単純化ルールを条件付きのものに置き換えるという方法があります。まず、次の補題を証明します。
lemma [simp]: "gcd m 0 = m" apply(simp) done lemma [simp]: "n ~= 0 ==> gcd m n = gcd n (m mod n)" apply(simp) done
条件付きなので、この単純化ルールによって無限ループになることはありません。最後に元の単純化ルールを無効にすることによって、問題はなくなります。
declare gcd.simps [simp del]
3.5.4 Induction
funで再帰関数を定義した場合も、証明は帰納法を使うのが一般的です。しかし、原始帰納関数の場合のようにうまくいくとは限りません。そこでfunは、定義した関数f毎に適した帰納ルールf.inductを定義します。例で見ていきます。
lemma "map f (sep x xs) = sep (f x) (map f xs)"
apply(induct_tac x xs rule: sep.induct)
残った三つのサブゴールはsepの三つの等式と一致しています。
1. !!a. map f (sep a []) = sep (f a) (map f [])
2. !!a x. map f (sep a [x]) = sep (f a) (map f [x])
3. !!a x y zs.
map f (sep a (y # zs)) = sep (f a) (map f (y # zs))
==> map f (sep a (x # y # zs)) = sep (f a) (map f (x # y # zs))
あとは単純化のみで証明可能です。
一般的にn個の引数を取る関数の再帰帰納法は次の形で適用します。
apply(induct_tac 変数1 ... 変数n rule: 関数名.induct)
4. Presenting Theories
この章では構文の詳細や理論ファイルの文書化について紹介されています。が、全てカットして第二部に飛びます。
*1:ProofGeneral 3.7.0ではfunも対応していません。
