構造化定理

ウィキペディア

構造化定理

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2024/07/08 01:41 UTC 版)

この項目では、ベーム、ヤコピーニ、ミルズらによるソフトウェア工学的手法としての「構造化定理」について説明しています。goto文論争については「goto文」をご覧ください。

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

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

概要

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

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

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

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

民間伝承的定理（Folk theorem）

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

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

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

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

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.

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

この節の加筆が望まれています。 （2014年7月）

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

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

${\displaystyle f\colon \mathbb {N} ^{n}\to \mathbb {N} }$

この節は検証可能な参考文献や出典が全く示されていないか、不十分です。出典を追加して記事の信頼性向上にご協力ください。（このテンプレートの使い方）
出典検索^?: "構造化定理" – ニュース · 書籍 · スカラー · CiNii · J-STAGE · NDL · dlib.jp · ジャパンサーチ · TWL（2013年8月）

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. ^ なお、goto文を除去した構造化したプログラムは、必ずしも良いデザインのプログラムになることを保証しない。ミルズらによれば、良いデザインは単純な考えに基づいているのではなく、奥深い簡潔さに基づくものである。^[4]
2. ^ なお、ここで主張されている「正当化」とは、全く同じ計算をすることを理論的に保証するという意味であり、そのように人間がプログラムを書くべきという意味ではない。たとえば近年よく使われている難読化ツール（obfuscator）がプログラムを難読化することも全く同様に「正当化」できるが、そのように人間がプログラムを書くべきという意味ではない。
3. ^ ^{a b c d e} ここで言う構造化プログラミングは、エドガー・ダイクストラの構造化プログラミングではない。構造化定理を使ったプログラミングの意味である。

出典

1. ^ StructuredProgramming(1979) p.118
2. ^ ^{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. 
3. ^ “CSE 111, Fall 2004, BOEHM-JACOPINI THEOREM”. Cse.buffalo.edu (2004年11月22日). 2013年8月24日閲覧。
4. ^ StructuredProgramming(1979) p.10
5. ^ ^{a b} StructuredProgramming(1979)
6. ^ Bohm, Corrado; Giuseppe Jacopini (May 1966). “Flow Diagrams, Turing Machines and Languages with Only Two Formation Rules”. Communications of the ACM 9 (5): 366–371. doi:10.1145/355592.365646. 
7. ^ ^{a b c d} 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. 
8. ^ ^{a b} Knuth, D. E. (1974). “Structured Programming with go to Statements Computing Surveys”. ACM, New York, NY, USA 6 (4): 261-301. CiteSeer^x: 10.1.1.103.6084. 
9. ^ Bruce Ian Mills (2005). Theoretical Introduction to Programming. Springer. p. 279. ISBN 978-1-84628-263-8 
10. ^ ^{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. 
11. ^ Yokoyama, Tetsuo; Axelsen, Holger Bock; Glück, Robert (January 2016). “Fundamentals of reversible flowchart languages”. Theoretical Computer Science 611: 87–115. doi:10.1016/j.tcs.2015.07.046. 
12. ^ Bennett, C. H. (November 1973). “Logical Reversibility of Computation”. IBM Journal of Research and Development 17 (6): 525–532. doi:10.1147/rd.176.0525. 
13. ^ ^{a b} Böhm, Corrado; Jacopini, Giuseppe (May 1966). “Flow diagrams, turing machines and languages with only two formation rules”. Communications of the ACM 9 (5): 366–371. doi:10.1145/355592.365646. 
14. ^ Cooper, David C. (August 1967). “Böhm and Jacopini's reduction of flow charts”. Communications of the ACM 10 (8): 463. doi:10.1145/363534.363539. 
15. ^ 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/. 
16. ^ ^{a b} Roberts, E. [1995] "Loop Exits and Structured Programming: Reopening the Debate," ACM SIGCSE Bulletin, (27)1: 268–272.
17. ^ E. N. Yourdon (1979). Classics in Software Engineering. Yourdon Press. pp. 49–50. ISBN 978-0-917072-14-7 
18. ^ 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
19. ^ David Anthony Watt; William Findlay (2004). Programming language design concepts. John Wiley & Sons. p. 228. ISBN 978-0-470-85320-7 
20. ^ Kenneth C. Louden; Kenneth A. Lambert (2011). Programming Languages: Principles and Practices (3 ed.). Cengage Learning. pp. 422–423. ISBN 1-111-52941-8 
21. ^ 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. 
22. ^ 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. 
23. ^ The original paper is Thomas J. McCabe (December 1976). “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 
24. ^ 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. 
25. ^ Ramshaw, L. (1988). “Eliminating go to's while preserving program structure”. Journal of the ACM 35 (4): 893–920. doi:10.1145/48014.48021. 
26. ^ Godfrey Nolan (2004). Decompiling Java. Apress. p. 142. ISBN 978-1-4302-0739-9 
27. ^ Krakatoa: Decompilation in Java (Does Bytecode Reveal Source?)
28. ^ paper.dvi "Java バイトコードをデコンパイルするための効果的なアルゴリズム"

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

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

• 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　民間伝承的定理の証明で使われた構造の多少詳細な説明。変換されたプログラムの具体的な例がある。

表 話 編 歴 コンピュータ・プログラミング言語の関連項目
言語水準	機械語 (1G) 低水準言語 (2G) 高水準言語 (3G) 第四世代言語 第五世代言語
言語処理系	アセンブラ インタプリタ コンパイラ トランスレータ
言語分類	マルチパラダイム言語 命令型言語 宣言型言語 非構造化言語 構造化言語 非手続き型言語 手続き型言語 オブジェクト指向言語 関数型言語 論理型言語 データフロー言語 ダイナミック言語 スクリプト言語 軽量プログラミング言語 ビジュアルプログラミング言語 難解プログラミング言語
その他	ドメイン固有言語 ジョブ制御言語 問い合わせ言語 マークアップ言語 形式言語
関連項目	コンピュータ言語 プログラミング言語一覧 プログラミング言語年表 プログラミングパラダイム