Think Stitch
  最近の更新


操作的意味論と帰納的定義

前回「MUパズル」で定理証明支援系 Isabelle による帰納的定義とその性質に関する証明をやってみました.

帰納的定義の応用例として,今回はプログラミング言語の操作的意味論を取り上げて,その上でささやかな定理を証明してみたいと思います.参考にする教科書は Glyn Winskel さんのThe Formal Semantics of Programming Languesです.

この本の2章に小さな命令型言語 IMP の操作的意味論が解説されています.この意味の上で,2つの指令,つまりプログラムが等価(同値, equivalent)であるとはどういうことか,という定義がなされます.その例として

\[ \mathbf{while}\ b\ \mathbf{do}\ c \sim \mathbf{if}\ b\ \mathbf{then}\ c;\, (\mathbf{while}\ b\ \mathbf{do}\ c)\ \mathbf{else}\ \mathbf{skip}\]

という等価性の証明が出ています.これを Isabelle でやってみます.

式の定義

プログラミング言語 IMP では3種類の構文要素が出てきます.算術式 $\mathbf{Aexp}$, 論理式$\mathbf{Bexp}$, そして指令$\mathbf{Com}$です.各構文要素は BNF で定義されています.たとえば算術式はこんな感じです.

\[a ::= n\ |\ X\ |\ a_0 + a_1\ |\ a_0 - a_1\ |\ a_0 \times a_1\]

これを代数的データ型で定義します.尚,少し手抜きをして演算子などは減らしました.

datatype aexp = Lit nat | Loc loc | Add aexp aexp
datatype bexp = Btrue | Bfalse | Le aexp aexp | Bnot bexp | Band bexp bexp
datatype com = CSkip | CAssign loc aexp | CSeq com com | CIf bexp com com | CWhile bexp com

ここで loc はロケーション,つまり変数を表す型です.具体的な値は使わないので,次のように抽象的に定義しておきます.

typedecl loc

式“評価”の表現

式の評価は,各変数の値を定める状態(あるいは環境) $\sigma$ を使って

\[ \langle a, \sigma \rangle \rightarrow n \]
\[ \langle b, \sigma \rangle \rightarrow t \]

と表されます.前者は算術式,後者は論理式です.

Isabelle ではこれらを単なる3つ組で表すことにします.

(a, s, n)
(b, s, t)

指令“実行”の表現

指令の実行は状態の変換とみなされます.

\[ \langle c, \sigma \rangle \rightarrow \sigma' \]

Isabelle ではこれも3つ組で表すことにします.

(c, s, s')

推論規則の表現

算術式,論理式,指令の各推論規則は,可能な評価あるいは実行(つまり3つ組)の集合を帰納的に定める規則とみることができます.ただ,MUパズルのときと違うのは,3つの集合がお互いに依存しているので,同時に定義しなければなりません.Isabelle の inductive_set では and を使って集合を並べることで複数の集合を同時並行的に定義することができます.

各集合を aconf, bconf, cconf とします.

たとえば逐次合成の規則

\[\frac{\quad\langle c_0, \sigma\rangle \rightarrow \sigma'' \quad \langle c_1, \sigma'' \rangle \rightarrow \sigma'}{\langle c_0; c_1, \sigma\rangle \rightarrow \sigma'}\]

これはつぎのようになります:

[| (c0, s0, s1) : cconf; (c1, s1, s2) : cconf |] ==> (CSeq c0 c1, s0, s2) : cconf

全体の定義は以下のとおりです.

inductive_set
 aconf :: "(aexp * (loc => nat) * nat) set" and
 bconf :: "(bexp * (loc => nat) * bool) set" and
 cconf :: "(com * (loc => nat) * (loc => nat)) set"
where
  aconf_lit: "(Lit n, s, n) : aconf"
| aconf_loc: "(Loc x, s, s x) : aconf"
| aconf_add: "[| (a0, s, n0) : aconf; (a1, s, n1) : aconf |] ==> (Add a0 a1, s, n0 + n1) : aconf"

| bconf_true: "(Btrue, s, True) : bconf"
| bconf_false: "(Bfalse, s, False) : bconf"
| bconf_le_true: "[| (a0, s, n0) : aconf; (a1, s, n1) : aconf; n0 <= n1 |] ==> (Le a0 a1, s, True) : bconf"
| bconf_le_false: "[| (a0, s, n0) : aconf; (a1, s, n1) : aconf; ~(n0 <= n1) |] ==> (Le a0 a1, s, False) : bconf"
| bconf_not: "(b, s, bb) : bconf ==> (Bnot b, s, ~bb) : bconf"
| bconf_and: "[| (b0, s, bb0) : bconf; (b1, s, bb1) : bconf |] ==> (Band b0 b1, s, bb0 & bb1) : bconf"

| cconf_skip: "(CSkip, s, s) : cconf"
| cconf_assign: "(a, s, m) : aconf ==> (CAssign l a, s, %x. (if x=l then m else s x)) : cconf"
| cconf_seq: "[| (c0, s0, s1) : cconf; (c1, s1, s2) : cconf |] ==> (CSeq c0 c1, s0, s2) : cconf"

| cconf_if_true: "[| (b, s, True) : bconf; (c0, s, s') : cconf |] ==> (CIf b c0 (c1::com), s, s') : cconf"
| cconf_if_false: "[| (b, s, False) : bconf; (c1, s, s') : cconf |] ==> (CIf b (c0::com) c1, s, s') : cconf"
| cconf_while_false: "(b, s, False) : bconf ==> (CWhile b (c::com), s, s) : cconf"
| cconf_while_true: "[| (b, s, True) : bconf; (c, s, s'') : cconf; (CWhile b c, s'', s') : cconf |] ==> (CWhile b c, s, s') : cconf"

これで操作的意味の定義ができました.

指令の等価性

指令の等価性は次のように定義されています.

\[c_0 \sim c_1 \quad\mathrm{iff}\quad \forall \sigma, \sigma'. \langle c_0, \sigma\rangle \rightarrow \sigma' \Longleftrightarrow \langle c_1, \sigma\rangle \rightarrow \sigma' \]

帰納的定義の逆規則

証明をはじめる前にもう1つだけ準備をします.MUパズルのところで,帰納的集合を定義すると帰納法のための規則が生成されるということをお話ししました.実は他にもいくつか規則が自動生成されるのですが,ここでは逆規則というものを使います.

例として先にあげた逐次合成の推論規則をみてみます.

\[\frac{\quad\langle c_0, \sigma\rangle \rightarrow \sigma'' \quad \langle c_1, \sigma'' \rangle \rightarrow \sigma'}{\langle c_0; c_1, \sigma\rangle \rightarrow \sigma'}\]

逐次合成に関する規則はこれだけです.したがってもし $\langle c_0; c_1, \sigma\rangle \rightarrow \sigma'$ という実行があるならば,逆に考えてある $\sigma''$ が存在して,$\langle c_0, \sigma\rangle \rightarrow \sigma''$ かつ $\langle c_1, \sigma'' \rangle \rightarrow \sigma'$ となるはずです.なぜなら規則以外で入り込む要素はない(最小!)だからです.これを表したものが逆規則です.

Isabelle はすべての規則について考慮した逆規則を1つだけ生成します.たとえば算術式の評価の集合 aconf の場合はこんなふうです:

[| (?a1.0, ?a2.0, ?a3.0) : aconf;
   !!n s. [| ?a1.0 = Lit n; ?a2.0 = s; ?a3.0 = n |] ==> ?P;
   !!x s. [| ?a1.0 = Loc x; ?a2.0 = s; ?a3.0 = s x |] ==> ?P;
   !!a0 s n0 a1 n1.
      [| ?a1.0 = Add a0 a1; ?a2.0 = s; ?a3.0 = n0 + n1;
         (a0, s, n0) : aconf; (a1, s, n1) : aconf |] ==> ?P |]
==> ?P

これだと使いにくいところがあるので,各規則ごとに抽出した規則を作るコマンド inductive_cases というものがあります.たとえば

inductive_cases x2: "((CSeq c0 c1), s, s') : cconf"

とすると,逐次合成だけに関する逆規則

[| (CSeq ?c0.0 ?c1.0, ?s, ?s') : cconf;
    !!s1. [| (?c0.0, ?s, s1) : cconf;
             (?c1.0, s1, ?s') : cconf |] ==> ?P |]
==> ?P

が生成されます.

ここでは4つの逆規則を準備しておくことにします.

inductive_cases x0: "((CWhile b c), s, s') : cconf"
inductive_cases x1: "((CIf b c0 c1), s, s') : cconf"
inductive_cases x2: "((CSeq c0 c1), s, s') : cconf"
inductive_cases x3: "(CSkip, s, s') : cconf"

while の展開定理

以下の定理を証明します.

\[ \mathbf{while}\ b\ \mathbf{do}\ c \sim \mathbf{if}\ b\ \mathbf{then}\ c;\, (\mathbf{while}\ b\ \mathbf{do}\ c)\ \mathbf{else}\ \mathbf{skip}\]

証明はほぼ一本道です.

lemma "(CWhile b c, s, s') : cconf <-> (CIf b (CSeq c (CWhile b c)) CSkip, s, s') : cconf"
apply(rule iffI)
(* --> *)
apply(erule x0)
apply(erule cconf_if_false)
apply(simp)
apply(rule cconf_skip)
apply(erule cconf_if_true)
apply(erule cconf_seq)
apply(assumption)
(* <-- *)
apply(erule x1)
apply(erule x2)
apply(erule cconf_while_true)
apply(assumption)
apply(assumption)
apply(erule x3)
apply(simp)
apply(erule cconf_while_false)
done

おおまかには,ある実行があるならば逆に考えてこれこれこういう導出があったはずで,その部品を再利用して組み立て方を変えると結論が導ける,そんな感じです.

ふだん直観的にしか理解していないプログラミング言語の意味やプログラムの振る舞いについて,このように厳密に表現して議論できるととてもすっきりした気分になれます.正しさに対する信頼度合いの次元が違います.

ビールを飲みながらやっても証明さえできれば結論に間違いはないですね.前提を書くときに飲んではいけませんけど :P

2016/07/23

© 2013,2014,2015 PRINCIPIA Limited