構造化定理

構造化定理とは、任意の一入力・一出力関数は、順次、選択、繰り返しの３つの基本制御構造からなる関数と等価であることを主張する定理である。構造化プログラム定理 あるいは ベーム-ヤコピーニの定理とも呼ばれる。

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

1. 概要
-----

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

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

2. 構造化定理の民間伝承的定理
----------------

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

民間伝承的定理すべてのフローチャートは、変数を付加することを許した上で、単一の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 ; end; if p = 2 then begin perform step 2 from the flowchart; p := resulting successor step of step 2 from the flowchart ; end; ... if p = n then begin perform step n from the flowchart; p := resulting successor step of step n from the flowchart ; end; end.

2.1. ベームとヤコピーニの証明
-----------------

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

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

をフローチャートによって計算可能な関数とする。これは再帰的関数になっている。クリーネの標準形定理によれば、原始再帰的関数 と が存在して、

が成り立つ。ここで となる が存在しないとき、右辺は未定義と解釈する。

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

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

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

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

3. 影響と改良
--------

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

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

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

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

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

1973年、S.ラオ・コサラジュは、任意の深さで multi-level break を使えるようにすれば、構造化プログラミングにおいて余分な変数の追加を回避できることを証明した。さらにコサラジュは「プログラムの厳密な階層が存在する。それは現在 //コサラジュ階層// と呼ばれている。//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 のみを採用していた。BLISS言語ファミリーは制約のない goto を提供していなかった。Javaプログラミング言語は、後に同様にこの手法を採用している960–965}}。

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

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

マッケイブの構造化プログラミングにおける禁止グラフの特徴づけは不完全であると考えることができる。少なくともダイクストラのD構造は、建設用ブロックと見なされている274–275}}date=July 2014}}。

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

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

4. COBOLへの応用
------------

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

手続きの中の基本ブロックを見つけ出す。
各ブロックの入口にユニークなラベルを割り当てる。そして、ブロックの出口に接続するべき入口のラベルを付ける。その手続きから戻るラベルに0を使い、その手続きの入口のラベルに1を使う。
その手続きを基本ブロックに分解する。
基本ブロックの1つしかない出口の行先が基本ブロックの場合、その出口に基本ブロックを再接続する。
その手続きの新しい変数を宣言する
余っている未接続の出口のそれぞれに次の行先のラベルの値をLに設定する文を追加する。
結果として生じるプログラムを組合せて、Lによって指定された入口のラベルの値に対応したプログラムを実行する選択文にする。
Lが0ではない限り、この選択文を実行するループを構築する。
Lを1に初期化して、そのループを実行するシーケンスを構築する。この構造は選択文のいくつかの選択肢をサブルーチンにすることによって改善できることに注意すること。

5. 関連項目
-------

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

6. 注釈
-----

7. 出典
-----

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

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

9. 参考文献
-------

10. 外部リンク
---------

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