構造化定理

出典: フリー百科事典『ウィキペディア(Wikipedia)』
ナビゲーションに移動 検索に移動

構造化定理(Structure theorem)構造化プログラム定理(structured program theorem) あるいは ベーム-ヤコピーニの定理(Böhm-Jacopini theorem)とも呼ばれる定理は,[1][2] プログラミング言語理論英語版の結論である。この定理は、もしも3つだけの手段(制御構造)で手続きを構築するならば、制御フローグラフの一分類(歴史的にフローチャートと呼ばれる)があらゆる計算可能関数を表現できることを述べている。

3つだけの手段(制御構造)は、以下のものである。

  1. ある一つの手続きを実行し、それからもう一つの手続きを実行する(順次)
  2. ブール演算式の値に従って2つの手続きのどれか1つを実行する(選択)
  3. ブール演算式が真である限り、手続きを繰り返し実行する(反復)

しかしながら、これらの制約に従う構造化チャートは、オリジナルプログラムがプログラムの位置によって表現する情報を追跡するためにビット形式の追加変数(整数の変数)を使うかもしれない。この構造はベーム(Böhm)のプログラミング言語 P′′ に基づいている。

(訳注)P′′はチューリングマシンと同様に磁気テープをメモリとして使用する。P′′の変数は1つしかなく磁気ヘッドの位置を記憶しており、暗黙的な存在である。P′′はこの変数に値を代入できず、磁気ヘッドをデータ単位毎に左右に動かすことしかできない。そのため、3つの制御構造だけでP′′の動きを表現することはできないということだろう。現在では、P′′のことを考慮する必要はないので、この追加変数のことも考慮する必要はない。

起源と変遷[編集]

この理論はコラド・ベーム(Corrado Böhm)とジュゼッペ・ヤコピーニ(Giuseppe Jacopini)による1966年の論文[3]に功績があると一般的に思われている[4]:381。デイヴィッド・ハレル(David Harel)は、ベーム-ヤコピーニの論文が特に構造化プログラミング[注釈 1]の支持者とともに「万人向けの評判」を享受したと1980年に書いた[4]:381。ハレルは「その論文の技巧的様式が原因で「1966年のベーム-ヤコピーニの論文」は詳細に読まれるよりも明らかにより頻繁に引用されている」[4]:381とも言及した。そして、1980年までに出版された大量の論文を再調査した後、ハレルはベーム-ヤコピーニの証明の内容は民間伝承的定理(folk theorem)として常に誤って伝えられてきたと主張した。民間伝承的定理は本質的に単純化された結論を含んでおり、ジョン・フォン・ノイマン(John von Neumann)とクリーネ(Kleene)の論文の近代的コンピューター理論の初期にさかのぼることができる[4]:383

ハレルは、より一般的な名前は1970年代初頭に構造化定理(The Structure Theorem)としてH.D.ミルズ(H.D. Mills)によって提案されたとも書いている[4]:381

単一の while ループ、この定理の民間伝承バージョン[編集]

このバージョンの定理は、元のプログラムの制御フローの全てを単一のグローバルな while ループに置き換える。このループはプログラムカウンターを模しており、元の非構造化プログラムにおける全てのラベル(フォローチャートの箱型の図形)に行くことができる。ハレルはコンピューターの初期に痕跡を残す2つの論文にこの民間伝承的定理の起源を突き止めた。1つは1946年のノイマン型の説明であり、1つのwhileループを使ってどのようにプログラムカウンターを制御するのかということを説明している。ハレルは、構造化定理の民間伝承バージョンによって使われる単一のループは基本的にノイマン型コンピューターにおけるフローチャートの実行のための操作的意味論を提供しているだけであると言及している。もう一つは、ハレルがこの定理の民間伝承バージョンを追跡して見つけたより古い出典であり、1936年からのスティーヴン・コール・クリーネNormal form theoremである[4]:383

ドナルド・クヌースは、元のプログラムの構造がこの変換によって完全に失われていることを指摘することによってこの形式を批判した。この形式は以下のような擬似コードになるだけである[5]:274。同様にブルース・イアン・ミルズはこの手法について「ブロック構造の精神はスタイルであり言語ではない。ノイマン型コンピューターを模することによって、ブロック構造言語の制限の範囲内であらゆるスパゲッティーコードの動きを作ることができる。このことはスパゲッティコードになることを防いでいない。」[6]

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.

ベームとヤコピーニの証明[編集]

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

影響と改良[編集]

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

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

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

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

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

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

コサラジュの論文から得られる単純な結論は、あるプログラムが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つの異なる部分グラフを含まなければならないということも明らかにした。この後者の結論は、非構造化プログラミング[注釈 1]の制御フローが一般的にスパゲティプログラムと呼ばれるものにどのようにしてなっていくのかを説明するのに役立つ。マッケイブは、あるプログラムが与えられたとき、それが理想の構造化プログラムからどの程度かけ離れているのかを定量化する数値測定手段も考案した。マッケイブは彼の測定手段を Essential complexity英語版 と呼んだ[16]

マッケイブの構造化プログラミング[注釈 1]における禁止グラフ英語版の特徴づけは不完全であると考えることができる。少なくともダイクストラのD構造(訳注:D構造の意味不明)は、建設用ブロックと見なされている[17]:274–275[要説明]

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

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

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 ループ、この定理の民間伝承バージョンと同様である。

関連項目[編集]

出典[編集]

  1. ^ a b c Dexter Kozen and Wei-Lung Dustin Tseng (2008年). “The Böhm–Jacopini Theorem Is False, Propositionally”. Mpc 2008. Lecture Notes in Computer Science 5133: 177–192. doi:10.1007/978-3-540-70594-9_11. ISBN 978-3-540-70593-2. http://www.cs.cornell.edu/~kozen/papers/bohmjacopini.pdf. 
  2. ^ CSE 111, Fall 2004, BOEHM-JACOPINI THEOREM”. Cse.buffalo.edu (2004年11月22日). 2013年8月24日閲覧。
  3. ^ Bohm, Corrado; Giuseppe Jacopini (1966年5月). “Flow Diagrams, Turing Machines and Languages with Only Two Formation Rules”. Communications of the ACM 9 (5): 366–371. doi:10.1145/355592.365646. 
  4. ^ a b c d e f g Harel, David (1980年). “On Folk Theorems”. Communications of the ACM 23 (7): 379–389. doi:10.1145/358886.358892. http://www.wisdom.weizmann.ac.il/~dharel/SCANNED.PAPERS/OnFolkTheorems.pdf. 
  5. ^ Donald Knuth (1974年). “Structured Programming with go to Statements”. Computing Surveys 6 (4): 261–301. doi:10.1145/356635.356640. 
  6. ^ Bruce Ian Mills (2005). Theoretical Introduction to Programming. Springer. p. 279. ISBN 978-1-84628-263-8. 
  7. ^ a b Ammarguellat, Z. (1992年). “A control-flow normalization algorithm and its complexity”. IEEE Transactions on Software Engineering 18 (3): 237–251. doi:10.1109/32.126773. 
  8. ^ Dijkstra, Edsger (1968年). “Go To Statement Considered Harmful”. Communications of the ACM 11 (3): 147–148. doi:10.1145/362929.362947. オリジナルの2007-07-03時点によるアーカイブ。. https://web.archive.org/web/20070703050443/http://www.acm.org/classics/oct95/. 
  9. ^ a b Roberts, E. [1995] "Loop Exits and Structured Programming: Reopening the Debate," ACM SIGCSE Bulletin, (27)1: 268–272.
  10. ^ E. N. Yourdon (1979). Classics in Software Engineering. Yourdon Press. pp. 49–50. ISBN 978-0-917072-14-7. 
  11. ^ Ashcroft, Edward; Zohar Manna (1971年). “The translation of go to programs to 'while' programs”. Proceedings of IFIP Congress.  The paper, which is difficult to obtain in the original conference proceedings due to their limited distribution, was republished in Yourdon's 1979 book pp. 51-65
  12. ^ David Anthony Watt; William Findlay (2004). Programming language design concepts. John Wiley & Sons. p. 228. ISBN 978-0-470-85320-7. 
  13. ^ Kenneth C. Louden; Kenneth A. Lambert (2011). Programming Languages: Principles and Practices (3 ed.). Cengage Learning. pp. 422–423. ISBN 1-111-52941-8. 
  14. ^ KOSARAJU, S. RAO. "Analysis of structured programs," Proc. Fifth Annual ACM Syrup. Theory of Computing, (May 1973), 240-252; also in J. Computer and System Sciences, 9, 3 (December 1974), doi:10.1016/S0022-0000(74)80043-7 cited by Donald Knuth (1974年). “Structured Programming with go to Statements”. Computing Surveys 6 (4): 261–301. doi:10.1145/356635.356640. 
  15. ^ Brender, Ronald F. (2002年). “The BLISS programming language: a history”. Software: Practice and Experience 32 (10): 955–981. doi:10.1002/spe.470. http://www.cs.tufts.edu/~nr/cs257/archive/ronald-brender/bliss.pdf. 
  16. ^ The original paper is Thomas J. McCabe (1976年12月). “A Complexity Measure”. IEEE Transactions on Software Engineering (4): 315–318. doi:10.1109/tse.1976.233837. https://books.google.com/books?id=vtNWAAAAMAAJ&pg=PA3.  For a secondary exposition see Paul C. Jorgensen (2002). Software Testing: A Craftsman's Approach, Second Edition (2nd ed.). CRC Press. pp. 150–153. ISBN 978-0-8493-0809-3. https://books.google.com/books?id=Yph_AwAAQBAJ&pg=PA150. 
  17. ^ Williams, M. H. (1983年). “Flowchart Schemata and the Problem of Nomenclature”. The Computer Journal 26 (3): 270–276. doi:10.1093/comjnl/26.3.270. 
  18. ^ Ramshaw, L. (1988年). “Eliminating go to's while preserving program structure”. Journal of the ACM 35 (4): 893–920. doi:10.1145/48014.48021. 
  19. ^ Godfrey Nolan (2004). Decompiling Java. Apress. p. 142. ISBN 978-1-4302-0739-9. 
  20. ^ https://www.usenix.org/legacy/publications/library/proceedings/coots97/full_papers/proebsting2/proebsting2.pdf
  21. ^ http://www.openjit.org/publications/pro1999-06/decompiler-pro-199906.pdf

注釈[編集]

  1. ^ a b c d e f ここで言う構造化プログラミングは、エドガー・ダイクストラ構造化プログラミングではない。構造化定理を使ったプログラミングの意味である。

より詳しく知るための文献[編集]

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

  • 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. 

外部リンク[編集]