構造化定理

構造化定理（こうぞうかていり、英: Structure theorem）とは、任意の一入力・一出力関数は、順次（sequence）、選択（ifthenelse）、繰り返し（whiledo）の３つの基本制御構造からなる関数と等価であることを主張する定理である。構造化プログラム定理（structured program theorem） あるいは ベーム-ヤコピーニの定理（Böhm-Jacopini theorem）とも呼ばれる。

goto文を除去することを正当化する内容を持ち、ミルズの構造化プログラミングにおいて基本となる定理である。

概要

1970年代にIBMの研究員ハーラン・ミルズは、自身の構造化プログラミングにおいて、構造化されたプログラム（structured program）と呼ばれるものを基本的なプログラム｛順次（sequence）、選択（ifthenelse）、反復（whiledo）｝の組み合わせたものとして定義した。基本プログラムの中には任意の分岐を作り出し複雑な制御構造をもたらすgoto文は含まれないが、そのgoto文を除いて任意のプログラムが構成できることを正当化する根拠がこの構造化定理（the structure theorem）である。

この定理はコラド・ベーム（Corrado Böhm）とジュゼッペ・ヤコピーニ（Giuseppe Jacopini）による1966年の論文に起源を持つと言われる。ベーム-ヤコピーニの論文は「その技巧的様式が原因で、論文は詳細に読まれるよりも明らかにより頻繁に引用されている」と評されることもあるものの、構造化プログラミングの支持者とともに「万人向けの評判」を享受した。

構造化定理の民間伝承的定理

デイヴィッド・ハレル（David Harel）は、1980年までに出版された大量の論文を再調査した結果として、ベーム-ヤコピーニの証明の内容は民間伝承的定理（folk theorem）として常に誤って伝えられてきたと主張した。ハレルはコンピューターの初期に痕跡を残す2つの論文にこの民間伝承的定理の起源を突き止めた。1つは1946年のノイマン型の説明であり、1つのwhileループを使ってどのようにプログラムカウンターを制御するのかということを説明している。ハレルは、構造化定理の民間伝承バージョンによって使われる単一のループは基本的にノイマン型コンピューターにおけるフローチャートの実行のための操作的意味論を提供しているだけであると言及している。もう一つは、ハレルがこの定理の民間伝承バージョンを追跡して見つけたより古い出典であり、1936年からのスティーヴン・コール・クリーネのNormal form theoremである。

民間伝承的定理（Folk theorem）

すべてのフローチャートは、変数を付加することを許した上で、単一のwhile-doからなるwhileプログラムと等価である。

このバージョンの定理は、元のプログラムの制御フローの全てを単一のグローバルな while ループに置き換える。このループはプログラムカウンターを模しており、元の非構造化プログラムにおける全てのラベル（フォローチャートの箱型の図形）に行くことができる。

ドナルド・クヌースは文献において、良い構造が重要なのであり、良い構造はFORTRAN, COBOL, アセンブリ言語でも記述できるとした。一方で、（構造化定理により）機械的にgotoを除去する変換を掛けたプログラムとは実際にどんなものになるのか、変換法の一例を示し、1つのループがプログラム全体の振る舞いを含んでしまうため、抽象化レベルという点では無意味であるとした。クヌースがそこで実際に示した、「機械的にgotoを除去」したコードと同様のものが以下であるが、見ればわかるようにgotoを使っていないというだけで、手続きのわかりやすい表現には全くなっていない。曰く「これですべての goto 文を除去できたわけであるが，実際にはすべての構造を失ってしまっている．」というわけである。

同様にブルース・イアン・ミルズはこの手法について「ブロック構造の精神はスタイルであり言語ではない。ノイマン型コンピューターを模することによって、ブロック構造言語の制限の範囲内であらゆるスパゲッティーコードの動きを作ることができる。このことはスパゲッティコードになることを防いでいない。」

p := 1;
while p > 0 do begin
  if p = 1 then begin
    perform step 1 from the flowchart;
    p := resulting successor step number of step 1 from the flowchart (0 if no successor);
  end;
  if p = 2 then begin
    perform step 2 from the flowchart;
    p := resulting successor step of step 2 from the flowchart (0 if no successor);
  end;
  ...
  if p = n then begin
    perform step n from the flowchart;
    p := resulting successor step of step n from the flowchart (0 if no successor);
  end;
end.

ベームとヤコピーニの証明

ベームとヤコピーニの論文の証明は、フローチャートの構造的帰納法によって行う。それはグラフ内のパターンマッチングを利用したので、ベームとヤコピーニの証明はプログラム変換アルゴリズムとして実用的ではなかった。そして、このような方向へのさらなる調査のためのドアを開けたのであった。

クリーネの標準形定理に基づく証明

$f\colon \mathbb {N} ^{n}\to \mathbb {N}$ をフローチャートによって計算可能な（一般には部分的に定義された）関数とする。これは再帰的関数になっている。クリーネの標準形定理（の弱い形）によれば、原始再帰的関数 $T\colon \mathbb {N} ^{n+1}\to \{0,1\}$ と $U\colon \mathbb {N} \to \mathbb {N}$ が存在して、

$f({\vec {x}})=U(\min\{y\in \mathbb {N} |T({\vec {x}},y)=1\})$

が成り立つ。ここで $T({\vec {x}},y)=1$ となる $y$ が存在しないとき、右辺は未定義と解釈する。

原始再帰的関数はループプログラムによって計算可能であることが知られている。ループプログラムは、基本的な算術演算、大小比較、条件分岐（if-then-else）、（変数によってループ回数を指定する）計数ループ、からなる言語であり、ジャンプ命令（goto文）やbreak文のような機構を含まない。したがって、ループプログラムで記述されるアルゴリズムは構造化定理の求める条件を満たしている。

したがって、$f$ を計算するには、次のような手続きを踏めばよい。

y := 0
t := 0
while t = 0 do begin
  t := T(x, y);
  if t = 0 then y := y+1;
end;
z := U(y).

ここで、T と U を計算する箇所は、構造化定理の条件を満たすようなアルゴリズムに置き換えられる。したがって $f$ もまた構造化定理を満たすアルゴリズムによって計算可能である。

影響と改良

ベーム-ヤコピーニの証明は、プログラムを改良するよりもプログラムを不明瞭にする可能性が高かったので、ソフトウェア開発のために構造化プログラミングを採用するかどうかという疑問を解決しなかった。

それどころか議論の始まりを告げることになった。エドガー・ダイクストラの有名な文書「Go To Statement Considered Harmful（Go to 文は有害と考えられる）」は1968年にその議論に続いた。

幾人かの研究者はベーム-ヤコピーニの結論に対して純粋な手段を取った。そして、ループの途中にある break と return ですらベーム-ヤコピーニの証明に必要とされていないので悪い実践であると主張した。したがって全てのループは単一の脱出ポイントを持つべきだと主張した。この純粋な手段はPascalプログラミング言語（1968～1969に設計）で具体化された。Pascalは1990年代中頃まで大学の入門的なプログラミングの講義をするために好まれたツールであった。

エドワード・ヨードンは、構造化プログラミングの流行が始まった時からの議論に基づいて、1970年代に非構造化プログラムを機械的に構造化プログラムに変換することに哲学的な反対があったと述べている。実用本位の対照的なこととして、そのような変換が既存のプログラムの大きなコードに役立ったということもあった。機械的変換のための最初の提案の一つは、エドワード・アッシュクロフト（Edward Ashcroft）とゾハル・マンナ（Zohar Manna）による1971年の論文であった。

ベーム-ヤコピーニの定理の直接的応用は、構造化チャートに導入されている余分なローカル変数（訳注：ループ途中脱出用のフラグのことだろうか？）といくつかの重複コードという結果になったのかもしれない。後者の問題は、この状況で loop and a half problem と呼ばれている（訳注：なぜ後者の問題なのかは英語版に書かれていない）。Pascal はこれらの問題の両方に影響されており、エリック・S・ロバーツ（Eric S. Roberts）によって引用された経験的研究に従っている。学生プログラマーであるロバーツは、いくつかの単純な問題（配列の中から1つの要素を検索する機能も含む）のために Pascal で適切な解法を公式化することに困難を感じた。ロバーツによって引用されたヘンリー・シャピロ（Henry Shapiro）による1980年の研究は、Pascal が提供する制御構造だけを使うと、適切な解法を得られた課題は20%だけだった。一方、ループの途中に return を書くことを許せば、この問題のために不適切なコードを書く課題は存在しなかった。

1973年、S.ラオ・コサラジュ（S. Rao Kosaraju）は、任意の深さで multi-level break （多重ループから複数階層を一気に脱出できる break）を使えるようにすれば、構造化プログラミングにおいて余分な変数の追加を回避できることを証明した。さらにコサラジュは「プログラムの厳密な階層が存在する。それは現在 コサラジュ階層（Kosaraju hierarchy） と呼ばれている。n はあらゆる整数である。深さ n の1つの multi-level break を含んでいるプログラムは、n よりも小さい深さの multi-level break を使ったプログラムとして書き換えることはできない」ということを証明した。コサラジュは BLISSプログラミング言語の multi-level break の仕組みを引き合いに出している。leave label という形式の multi-level break は、実際に BLISS-11 で導入されていた。最初の BLISS は single-level break （一階層しか脱出できない break）のみを採用していた。BLISS言語ファミリーは制約のない goto を提供していなかった。Javaプログラミング言語は、後に同様にこの手法を採用している。

コサラジュの論文から得られる単純な結論は、あるプログラムが2つの異なる脱出口を持つループを含んでいないときだけ（変数を追加せずに）あるプログラムを構造化プログラムへ変換できるということである。変換可能性はコサラジュによって定義された。大雑把に言うと、同一の機能を処理し、同じ「基本動作」を使い、そして元のプログラムと同様であると断言できることである。しかし、元のプログラムと異なる制御フロー構造を使うことができる（これはベーム-ヤコピーニの使ったものよりも狭い概念の変換可能性である）。この結論に触発されて、コサラジュが頻繁に引用する循環的複雑度の概念を導入した論文の第6節において、トーマス・J・マッケイブ（Thomas J. McCabe）は非構造化プログラムの制御フローグラフ（CFG : Control Flow Graph）のためのクラトフスキーの定理と類似したものを記述した。つまり、プログラムのCFGを非構造化にする最小の誘導部分グラフである。これらの部分グラフは自然言語で非常に良く説明できる。それらは以下のものである。

1. ループの外へ分岐（ループサイクルテストからの分岐以外）
2. ループの中へ分岐
3. 決定の中へ分岐（すなわち、if分岐の中へ入る）
4. 決定の外へ分岐

マッケイブはこれらの4つのグラフが部分グラフとして登場するときに独立していないことを実際に明らかにした。プログラムが非構造化になるための必要十分条件は、そのCFGがこれらの4つのグラフから3つ選んで作った部分集合のどれか1組を部分グラフとして持つことである（訳注：4つのグラフのうち3つのグラフがCFGに含まれていたら非構造化になるということ）。彼は、もしも非構造化プログラムがこれらの4つの部分グラフの1つを含んでいるならば、その非構造化プログラムは4つの部分グラフからもう1つの異なる部分グラフを含まなければならないということも明らかにした。この後者の結論は、非構造化プログラミングの制御フローが一般的にスパゲティプログラムと呼ばれるものにどのようにしてなっていくのかを説明するのに役立つ。マッケイブは、あるプログラムが与えられたとき、それが理想の構造化プログラムからどの程度かけ離れているのかを定量化する数値測定手段も考案した。マッケイブは彼の測定手段を Essential complexity と呼んだ。

マッケイブの構造化プログラミングにおける禁止グラフの特徴づけは不完全であると考えることができる。少なくともダイクストラのD構造（訳注：D構造の意味不明）は、建設用ブロックと見なされている。

1990年まで既存プログラムのほとんどの構造を維持しながら goto を削除するためにかなり多くの提案された手法が存在した。この問題への様々な手段はいくつかの等価の概念も提案した。それらの概念は上で議論された民間伝承的定理のような結果を避けるために単純なチューリングマシン等価よりも厳密である。選ばれた等価の概念の厳密性は必要とされる制御フローの最小セットを要求する。ライル・ラムショウ（Lyle Ramshaw）による1988年の JACM (Journal of the ACM) の論文は、それまでのその分野を調査しており、さらに自身の手法も提案している。ラムショウのアルゴリズムは、Java仮想マシンコードがオフセットとして表現された対象を持つ分岐命令を持つので、Javaの逆コンパイラの例のために使われた。しかし、上位レベルのJava言語だけは multi-level の break と continue 文を持っている。

Ammarguellat (1992年)は、ループの一箇所からの脱出を強制するために後戻りする変換手法を提案した。

COBOLへの応用

→「ミルズの構造化プログラミング」も参照

1980年代にIBMの研究員ハーラン・ミルズ（Harlan Mills）は、COBOL Structuring Facility の開発を監督した。COBOL Structuring Facility はCOBOLコードへの構造化アルゴリズムを応用した。ミルズの変換は各手続に対して以下の手順を必要とした。

1. 手続きの中の基本ブロック（入口と出口がそれぞれ1つしかないコード）を見つけ出す。
2. 各ブロックの入口にユニークなラベル（訳注：ここで言うラベルは数値である）を割り当てる。そして、ブロックの出口に接続するべき入口のラベルを付ける。その手続きから戻るラベルに0を使い、その手続きの入口のラベルに1を使う。
3. その手続きを基本ブロックに分解する。
4. 基本ブロックの1つしかない出口の行先が基本ブロックの場合、その出口に基本ブロックを再接続する。
5. その手続きの新しい変数を宣言する（参照のために L と呼ぶ）
6. 余っている未接続の出口のそれぞれに次の行先（入口）のラベルの値をLに設定する文を追加する。
7. 結果として生じるプログラムを組合せて、Lによって指定された入口のラベルの値に対応したプログラムを実行する選択文にする。
8. Lが0ではない限り、この選択文を実行するループを構築する（つまり、Lが0になるとループが終了し、手続きから戻ることになる）。
9. Lを1に初期化して、そのループを実行するシーケンスを構築する（前述のように1は手続きの入口を意味する）。

この構造は選択文のいくつかの選択肢をサブルーチンにすることによって改善できることに注意すること。

（訳注）この手順の目的は、複数の出口を持つプログラムを排除することである。変数Lに次の行先を指定することによって、出口を1つにしているのである。例えば、あるプログラムに出口が3つあるとして、それぞれの出口の行先が 100, 200, 300 とする。変数Lに行先の値（100, 200, 300）のどれか一つを代入する構造にすれば、出口は一つで済む。しかし、この方法は前述の単一の while ループ、この定理の民間伝承バージョンと同様である。

関連項目

• 構造化プログラミング
• チューリング完全

より詳しく知るための文献

以上で扱われていない資料：

• DeMillo, Richard A. (1980). “Space-Time Trade-Offs in Structured Programming: An Improved Combinatorial Embedding Theorem”. Journal of the ACM 27 (1): 123–127. doi:10.1145/322169.322180. 
• Devienne, Philippe (1994). “One binary horn clause is enough”. Lecture Notes in Computer Science. Lecture Notes in Computer Science 775: 19–32. doi:10.1007/3-540-57785-8_128. ISBN 978-3-540-57785-0. 

参考文献

• Richard C. Linger,Harlan D. Mills,Bernard I. Wit (1979). IBM Corporation. ed. Structured Programming: Theory and Practice. Addison-Wesley. https://trace.tennessee.edu/cgi/viewcontent.cgi?article=1008&context=utk_harlan 

外部リンク

• http://www.cs.uwlax.edu/~riley/CS421/lect8_boehm.ppt　民間伝承的定理の証明で使われた構造の多少詳細な説明。変換されたプログラムの具体的な例がある。