Isabelle Tutorial その21

7.4 Case Study: A Context Free Grammer

ここでは、HopcroftとUllmanによる文脈自由文法の例*1を取り上げます。生成規則は次のようになっており、これはaとbの数が同じ文字列を生成します。

$S \rightarrow \epsilon | bA | aB$
$A \rightarrow aS | bAA$
$B \rightarrow bS | aBB$

まず、アルファベットを定義します。

datatype alpha = a | b

便宜上、次の定理を証明しておきます。

lemma [simp]: "(x ~= a) = (x = b) & (x ~= b) = (x = a)"
by(case_tac x, auto)

生成規則は相互帰納で定義します。

inductive_set S :: "alpha list set" and
              A :: "alpha list set" and
              B :: "alpha list set"
where
"[] : S" |
"w : A ==> b#w : S" |
"w : B ==> a#w : S" |
"w : S ==> a#w : A" |
"[| v : A; w : A |] ==> b#v@w : A" |
"w : S ==> b#w : B" |
"[| v : B; w : B |] ==> a#v@w : B"

Sに含まれる文字列は、aとbの数が同じであることを証明します。相互帰納で定義しているので、Aに含まれる文字列はaの数がbよりも一つ多いこと、Bに含まれる文字列はbの数がaよりも一つ多いことを同時に証明します。

lemma correctness:
"(w : S --> size[x<-w. x=a] = size[x<-w. x=b]) &
 (w : A --> size[x<-w. x=a] = size[x<-w. x=b] + 1) &
 (w : B --> size[x<-w. x=b] = size[x<-w. x=a] + 1)"
by(rule S_A_B.induct, auto)

上の補題の中でリスト上の関数filterを使用しており、[x<-xs. P x]はfilter P xsと同じです。驚くかもしれませんが、証明はS_A_Bに関する規則帰納とautoだけで完了します。

健全性の証明は簡単ですが、完全性、aとbの数が同じ文字列は全てSに含まれていることの証明は複雑です。この証明には次の補題、aの数がbより二つ多い文字列は、aの数がbより一つ多い二つの文字列に分けることができるということを必要とします。これは、次のように考えます。すなわち、左端からaとbの数の差を数えていくと、最初は0、最後は2になり、その途中の1になる箇所で分けることができます。形式的には、次の定理を利用します。

[| ALL i<?n. abs (?f (i + 1) - ?f i) <= 1; ?f 0 <= ?k; ?k <= ?f ?n |]
==> EX i<=?n. ?f i = ?k　　　　　　　　　　　　　　　　　　　(nat0_intermed_int_val)

まず、左から右へ一つ動くごとに、aとbの数の差が一つずつ変わることを証明します。ただし、aとbに関する汎用的なプロパティPについての定理として証明します。

lemma step1: "ALL i < size w.
  abs((int(size[x<-take (i + 1) w. P x]) - int(size[x<-take (i + 1) w. ~P x]))
      - (int(size[x<-take i w. P x]) - int(size[x<-take i w. ~P x]))) <= 1"
apply(induct_tac w)
apply(auto simp add: abs_if take_Cons split: nat.split)
done

intは自然数から整数へ変換する関数であり、差を計算するために必要です。takeはリストに関する関数として定義されており、take i xsはxsの先頭から長さi分だけ取り出す関数です。またdrop i xsはxsの先頭から長さi分だけ取り出した残りを返す関数です。

先ほどの補題の証明に移ります。

lemma part1:
"size[x<-w. P x] = size[x<-w. ~P x] + 2 ==>
 EX i <= size w. size[x<-take i w. P x] = size[x<-take i w. ~P x] + 1"
apply(insert nat0_intermed_int_val[OF step1, of "P" "w" "1"])
by force

part1はプレフィックスtake i wに関する補題ですので、サフィックスdrop i wに関しても証明します。

lemma part2:
"[| size[x<-take i w @ drop i w. P x] =
    size[x<-take i w @ drop i w. ~P x] + 2;
    size[x<-take i w. P x] = size[x<-take i w. ~P x] + 1|]
 ==> size[x<-drop i w. P x] = size[x<-drop i w. ~P x] + 1"
by(simp del: append_take_drop_id)

append_take_drop_idは次のような定理です。

take ?n ?xs @ drop ?n ?xs = ?xs　　　　(append_take_drop_id)

これを使用すると証明がうまくいかないので、無効にしています。代わりに次の定理が使われ、証明がうまくいきます。

filter ?P (?xs @ ?ys) = filter ?P ?xs @ filter ?P ?ys　　　　(filter_append)

以降の証明では、明らかな場合を自動的に証明させるため、次のルールを単純化規則として宣言しておきます。

declare S_A_B.intros[simp]

完全性の証明は手順のみを示し、詳細は省略します。

theorem completeness:
"(size[x<-w. x=a] = size[x<-w. x=b] --> w : S) &
 (size[x<-w. x=a] = size[x<-w. x=b] + 1 --> w : A) &
 (size[x<-w. x=b] = size[x<-w. x=a] + 1 --> w : B)"
apply(induct_tac w rule: length_induct)
apply(rename_tac w)
apply(case_tac w)
apply(simp_all)
apply(rename_tac v)
apply(rule conjI)
apply(clarify)
apply(frule part1[of "% x. x=a", simplified])
apply(clarify)
apply(drule part2[of "% x. x=a", simplified])
apply(assumption)
apply(rule_tac n1 = i and t = v in subst[OF append_take_drop_id])
apply(rule S_A_B.intros)
apply(force simp add: min_less_iff_disj)
apply(force split add: nat_diff_split)
apply(clarify)
apply(frule part1[of "% x. x=b", simplified])
apply(clarify)
apply(drule part2[of "% x. x=b", simplified])
apply(assumption)
apply(rule_tac n1 = i and t = v in subst[OF append_take_drop_id])
apply(rule S_A_B.intros)
apply(force simp add: min_less_iff_disj)
apply(force split add: nat_diff_split)
done

*1:John E. Hopcroft and Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.