プログラムの算術的計算法（続き＆完結） - 檜山正幸のキマイラ飼育記 (はてなBlog)

昨日の続き。
※印刷の時はサイドバー消えます。
内容：

特別なプログラム文
簡潔な記法と計算法則
計算例
手順から直感へ、そしてふたたび手順へ
非決定性の繰り返し
whileの実現
計算法と図解法

前編

特別なプログラム文

A, Bなどの大文字は、プログラムの文（複文や複雑な表現も含める）を表すと約束したのですが、これらは何か特定の文ではなくて文一般を表します。それに対して、以下のIとOは特定の文を表す固有名詞として使います。

I （skip）-- 空文、何もしない
O （hang） -- 先に進めないで制御不能／無反応になる

Iはおなじみの空文です。Oのほうは、制御がつまってしまって（ささって）進めず終われずの状態になる文です。無限ループに陥る文だと思ってもいいです。記号「I」「O」は、「1」「0」に似せて選んでいるのですが、実際、Aが何であっても次の法則が成立します。

A;I = I;A = A
A;O = O;A = O
A | O = O | A = A

空文Iに関する「A;I = I;A = A」はすぐわかりますね。ただし、(A | I)とIは通常違います。A | I つまり choose A or skip endでは、Aが実行されずにskipが実行される、つまり何も起きないで次に進むことがあります。

Aが正常終了するプログラム文だとしても、A;OとO;Aは制御が戻らないでの、全体としてO（hang）だと考えます。「A | O = O | A = A」は、昨日も言った「プログラムは通れる実行経路を通ろうとする」を表現しています。非決定性の選択でも、破綻（hang状態）を回避するように行動します。

簡潔な記法と計算法則

手で計算するときは、演算記号を省略したりオーバーロードすると便利です。

正式な記法	略記
p∧q	pq
p∨q	p + q
¬p	p'
true	1
false	0
A;B	AB
A\|B	A + B
p・A	pA

略記を使って計算法則を書いておきます。

(A + B) + C = A + (B + C)
A + O = O + A = A
A + B = B + A
A + A = A
(AB)C = A(BC)
AO = OA = O
AI = IA = A
A(B + C) = AB + AC
(A + B)C = AC + BC
(pq)A = p(qA)
p(A + B) = pA + pB
(p + q)A = pA + qA
0A = O
1A = A

算数の計算と大差ないですが：

A + A = A に注意。
AB = BA は成立しない。
pA は意味を持つが、Apは未定義。
論理式に関して p∨(q∧r) = (p∨r)∧(q∨r) が成立するが、これを略記方式で書くと p + (qr) = (p + r)(q + r) と不自然になるので注意。

計算例

次の3つの表現が同値であることを計算で示してみます。if (p) then A endは、pA + p'I と書けることを思い出してください。

// その1
if (p) {
 ;
} else {
 if (q) {
  A;
 }
}

// その2
if (!p) {
 if (q) {
  A;
 }
}

// その3
if (!p && q) {A;}

/* コメント内では正式な演算記号を使うので注意！
 */
  // その1
  pI + p'(qA + q'I)      // ・と|の分配法則
= pI + p'(qA ) + p'(q'I) // ・の結合法則
= pI + (p'q)A + (p'q')I  // ｜の交換法則
= (p'q)A + pI + (p'q')I  // ・と|の分配法則
= (p'q)A + (p + (p'q'))I // 余分な括弧を除く
= (p'q)A + (p + p'q')I

  // その2
  p'(qA + q'I) + p''I    // 二重否定の除去
= p'(qA + q'I) + pI      // ・と|の分配法則
= p'(qA) + p'(q'I) + pI  // ・の結合法則
= (p'q)A + (p'q')I + pI  // ・と|の分配法則
= (p'q)A + *1I // 余分な括弧を除く
= (p'q)A + (p + p'q')I

これで、「その1」と「その2」が同値であることがわかりました。ここで、(p + p'q') を正式な記法で書いてみれば p∨(¬p∧¬q)。これもとにを計算してみると：

  p∨(¬p∧¬q)      // ∨の∧に対する分配法則
= (p∨¬p)∧(p∨¬q) // p∨¬p は常にtrue
= true∧(p∨¬q)     // true∧x はx
= p∨¬q             // 二重否定とド・モルガンの法則
= ¬(¬p∨q)         // 略記
= (p'q)'

この結果「p + p'q' = (p'q)'」を使うと：

  // その1、その2
  p'qA + (p + p'q')I
= p'qA + (p'q)'I
 // if (p'q) then A end

だから、「その1」と「その2」と「その3」も同値。

手順から直感へ、そしてふたたび手順へ

上の計算をみて、「簡単なプログラム断片の同値性を示すのに、こんな面倒な計算をするのか？」と思った人がいるでしょう。そういう人は、例示したプログラムの同値性は「ほぼ自明」に感じるだろうし、「直感でわかる」のでしょう。

しかし、事例のプログラムの同値性でさえ、それほど自明ではありませんよ。“入れ子のifが&&で書ける”なんてのが最初からわかるわけありません。一般に、経験やトレーニングを積んだ人の行動を、手順として書き下すと膨大な量になることがあります。計算も手順ですから、どうしても量は多くなります。

「自明に思えない」「直感的には把握できない」原因が、手順のどれかが納得いってないことかもしれません。「自明な事実」や「直感（or 直観）的把握」を、計算手順としてあらわに（explicitly）書き下すことは、事実の根拠や把握のメカニズムを理解する手助けになると期待できます。

もっとも、ここで採用した計算体系が直観的把握の背景であるかどうかは、かなり疑問です。どちらかというと、計算がうまくいくように選んだ定式化ですから。

非決定性の繰り返し

(I + A + A;A)という式は次のようにも書けます。

choose
  skip
or
  A
or
  A;A
end

どの選択肢が選ばれるかわからないので、実行は「何もしないか、Aが実行されるか、A;Aが実行されるか」です。これは、「Aが0回、または1回、または2回実行される」ことですね。A;A = AA = A²のような累乗指数を使うとすると、(I + A + A²)は「Aの0回以上2回以下の繰り返し」と読めます。同様に、(I + A + ... + Aⁿ)なら「Aの0回以上n回以下の繰り返し」です。

「Aの任意回の繰り返し」は(I + A + A² + ... )という無限級数形式となります。この無限級数をA*と書きます。A*は、Aを何回繰り返すか前もってわからない繰り返しなので、非決定性の繰り返しと呼びましょう。

もうお気づきだと思いますが、「;」「|」「*」は、正規表現の同様な記号（演算）と完全に対応してます（ガードを付ける「・」は正規表現にはありません）。実は、ここで説明しているプログラムの計算体系は正規表現の計算体系と同じもの（Kleene代数）です。

whileの実現

while (p) Aを、「;」「|」「・」「*」で表現してみましょう。このためには、再帰方程式を解きます。その方程式自体は、次の2つのプログラムが同値であるという事実（あるいは仮説）から導きます。

// その1
while (p) {A;}

// その2
if (p) {
 A;
 while (p) {A;}
}

while (p) Aを表す（未知の）式をXとすると、「その1」と「その2」が等しいことは：

X = p(AX) + p'I

と書けます。等式の右辺はif文の表現です。

この等式 X = p'I + p(AX) （項の順序は交換した）に自分自身を代入していきます。

// 1回代入
X = p'I + p(AX)  // 代入
  = p'I + p(A(p'I + p(AX)))
  = p'I + p(Ap'I + Ap(AX))
  = p'I + pAp'I + pAp(AX)
  = (I + pA)p'I + pAp(AX)
// 2回代入
X = p'I + pAp'I + pAp(AX) // 代入
  = p'I + pAp'I + pAp(A(p'I + p(AX)))
  = p'I + pAp'I + pAp(Ap'I + Ap(AX))
  = p'I + pAp'I + pApAp'I + pAp(AX)
  = (I + pA + pApA)p'I + pAp(AX)

しばらく代入計算をしていると一般形が予測できますが、次のような形になります。

X = (I + pA + (pA)² + ... + (pA)ⁿ)p'I + (pA)^n-1p(AX)

非常におおざっぱなことを言うと、nが大きくなるとお尻に付いている余分な項は無視できるようになるので：

X = (I + pA + (pA)² + ... )p'I

結局、while (p) Aは、(pA)*;p'I （正式な記法では(p・A)*;(¬p・I)）と書けます。

pを1（true）、AをI（skip）としてみましょう。これはwhile (true) skipですから無限ループのはず。実際、(1I)*;0I = (1I)*;O ですが、O（hang）の順次結合はプログラム全体をOとするので、while (true) skipはhangと同値です。

計算法と図解法

既に触れたように、ここで紹介した表記と計算は、正規表現のそれとほぼ同じものです。正規表現（またはそれと同等な線形文法）には、構文図（syntax diagram）という図解法があります。例えば、JSONのページの後半に描いてある図が構文図です（描き方の流儀は色々あります）。オートマトンの状態遷移図（例えば、wikipediaの項目を見よ）も事実上構文図と同じものです。

そうならば、プログラムの構造と実行フローも同様に図示できるはずですね。昔なつかしの流れ図（フローチャート）がそれですが、もうちょっと洗練された流れ図2.0（つかっちまったよ 2.0）もあります。今風流れ図の例は次の論文を（読まなくてもいいから）眺めるとお目にかかれます。

僕の記事「ETBダイアグラム」は、今風流れ図の繰り返し／ループを持たない部分の解説です。そんな図（やあんな図）を僕はよく描きます。

流れ図の構造を、現代的に解析した人にGheorghe Stefanescuがいます。流れ図が嫌われ見捨てられた時期（1980年代）に、ものすごく先進したことをやっていることに感心・感服してしまいます。

あ、そうそう、プログラムと正規表現に共通する構造を詳しく調べた人をひとりだけ挙げれば、Dexter Kozen。Kozen先生、1985年と2004年じゃ別人みたい。（で、わざわざ写真2枚ってことか？）

*1:p'q') + p)I // |の交換法則 = (p'q)A + (p + (p'q'