構造化定理のソースを表示

{{Otheruses|ベーム、ヤコピーニ、ミルズらによるソフトウェア工学的手法としての「構造化定理」| goto文論争 |goto文}}

'''構造化定理'''（こうぞうかていり、{{lang-en-short|Structure theorem}}）とは、任意の一入力・一出力関数は、順次（sequence）、選択（ifthenelse）、繰り返し（whiledo）の３つの基本制御構造からなる関数と等価であることを主張する定理である<ref>[[#StructuredProgramming(1979)|StructuredProgramming(1979)]] p.118
</ref>。'''構造化プログラム定理（structured program theorem）''' あるいは '''ベーム-ヤコピーニの定理（Böhm-Jacopini theorem）'''とも呼ばれる<ref name="kozen">{{cite journal|url= http://www.cs.cornell.edu/~kozen/papers/bohmjacopini.pdf |title=The Böhm–Jacopini Theorem Is False, Propositionally|author=[[Dexter Kozen]] and Wei-Lung Dustin Tseng|doi=10.1007/978-3-540-70594-9_11|journal=Mpc 2008|volume=5133|pages=177–192|series=Lecture Notes in Computer Science|year=2008|isbn=978-3-540-70593-2}}</ref><ref>{{cite web|url=http://www.cse.buffalo.edu/~rapaport/111F04/greatidea3.html |title=CSE 111, Fall 2004, BOEHM-JACOPINI THEOREM |publisher=Cse.buffalo.edu |date=2004-11-22 |accessdate=2013-08-24}}</ref>。

goto文を除去することを正当化する内容を持ち{{Refnest|group="注釈"|なお、goto文を除去した構造化したプログラムは、必ずしも良いデザインのプログラムになることを保証しない。ミルズらによれば、良いデザインは単純な考えに基づいているのではなく、奥深い簡潔さに基づくものである。<ref>[[#StructuredProgramming(1979)|StructuredProgramming(1979)]] p.10</ref>}}、[[ミルズの構造化プログラミング]]において基本となる定理である<ref group="注釈">なお、ここで主張されている「正当化」とは、全く同じ計算をすることを理論的に保証するという意味であり、そのように人間がプログラムを書くべきという意味ではない。たとえば近年よく使われている難読化ツール（obfuscator）がプログラムを難読化することも全く同様に「正当化」できるが、そのように人間がプログラムを書くべきという意味ではない。</ref>。
== 概要 ==
1970年代にIBMの研究員[[ハーラン・ミルズ]]は、[[ミルズの構造化プログラミング|自身の構造化プログラミング]]において、構造化されたプログラム（structured program）と呼ばれるものを基本的なプログラム｛順次（sequence）、選択（ifthenelse）、反復（whiledo）｝の組み合わせたものとして定義した<ref name="Mills">[[#StructuredProgramming(1979)|StructuredProgramming(1979)]]</ref>{{rp|118}}。基本プログラムの中には任意の分岐を作り出し複雑な制御構造をもたらすgoto文は含まれないが、そのgoto文を除いて任意のプログラムが構成できることを正当化する根拠がこの'''構造化定理'''（the structure theorem）である<ref name="Mills" />{{rp|118}}。

この定理は[[コラド・ベーム]]（Corrado Böhm）とジュゼッペ・ヤコピーニ（Giuseppe Jacopini）による1966年の論文<ref>{{cite journal|last=Bohm|first=Corrado|author2=Giuseppe Jacopini |date=May 1966|title=Flow Diagrams, Turing Machines and Languages with Only Two Formation Rules|journal=Communications of the ACM |volume=9|issue=5|pages=366–371|doi=10.1145/355592.365646}}</ref>に起源を持つと言われる<ref name="Harel">{{cite journal|last=Harel|first=David|author=David Harel|year=1980|title=On Folk Theorems|journal=Communications of the ACM|volume=23|issue=7|pages=379–389|doi=10.1145/358886.358892|url=http://www.wisdom.weizmann.ac.il/~dharel/SCANNED.PAPERS/OnFolkTheorems.pdf}}</ref>{{rp|381}}。ベーム-ヤコピーニの論文は「その技巧的様式が原因で、論文は詳細に読まれるよりも明らかにより頻繁に引用されている」と評されることもあるものの、構造化プログラミングの支持者とともに「万人向けの評判」を享受した<ref name="Harel"/>{{rp|381}}。

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

;民間伝承的定理（Folk theorem）
:すべてのフローチャートは、変数を付加することを許した上で、単一のwhile-doからなるwhileプログラムと等価である。
このバージョンの定理は、元のプログラムの制御フローの全てを単一のグローバルな <code>while</code> ループに置き換える。このループは[[レジスタ (コンピュータ)|プログラムカウンター]]を模しており、元の非構造化プログラムにおける全てのラベル（フォローチャートの箱型の図形）に行くことができる。

[[ドナルド・クヌース]]は文献<ref name="structured_programming_with_go_to_statements">{{Cite journal|id={{citeseerx|10.1.1.103.6084}} |first=D. E. |last=Knuth|authorlink=ドナルド・クヌース |title=Structured Programming with go to Statements Computing Surveys |volume= 6 |number=4 |journal=ACM, New York, NY, USA |year=1974 |pages= 261-301}}</ref>において、良い構造が重要なのであり、良い構造はFORTRAN, COBOL, アセンブリ言語でも記述できるとした。一方で、（構造化定理により）機械的にgotoを除去する変換を掛けたプログラムとは実際にどんなものになるのか、変換法の一例を示し、1つのループがプログラム全体の振る舞いを含んでしまうため、抽象化レベルという点では無意味であるとした<ref name="structured_programming_with_go_to_statements" />。クヌースがそこで実際に示した、「機械的にgotoを除去」したコードと同様のものが以下であるが、見ればわかるようにgotoを使っていないというだけで、手続きのわかりやすい表現には全くなっていない。曰く「これですべての goto 文を除去できたわけであるが，実際にはすべての構造を失ってしまっている．」というわけである。

同様にブルース・イアン・ミルズはこの手法について「ブロック構造の精神はスタイルであり言語ではない。ノイマン型コンピューターを模することによって、ブロック構造言語の制限の範囲内であらゆるスパゲッティーコードの動きを作ることができる。このことはスパゲッティコードになることを防いでいない。」<ref name="Mills2005">{{cite book|author=Bruce Ian Mills|title=Theoretical Introduction to Programming|year=2005|publisher=Springer|isbn=978-1-84628-263-8|page=279}}</ref>

<syntaxhighlight lang="Pascal">
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.
</syntaxhighlight>

=== ベームとヤコピーニの証明 ===
{{expand section|date=July 2014}}
ベームとヤコピーニの論文の証明は、フローチャートの[[構造的帰納法]]によって行う<ref name="Harel"/>{{rp|381}}。それは[[:en:Subgraph isomorphism problem|グラフ内のパターンマッチング]]を利用したので、ベームとヤコピーニの証明はプログラム変換アルゴリズムとして実用的ではなかった。そして、このような方向へのさらなる調査のためのドアを開けたのであった<ref name="amma92"/>。

=== クリーネの標準形定理に基づく証明 ===
<math>f\colon\mathbb{N}^n \to \mathbb{N}</math> をフローチャートによって計算可能な（一般には部分的に定義された）関数とする。これは[[再帰的関数]]になっている。[[クリーネの標準形定理]]（の弱い形）によれば、[[原始再帰的]]関数 <math>T\colon \mathbb{N}^{n+1}\to \{0, 1\}</math> と <math>U\colon \mathbb{N}\to\mathbb{N}</math> が存在して、
: <math>f(\vec{x}) = U(\min \{ y \in \mathbb{N} | T(\vec{x}, y) = 1 \})</math>
が成り立つ。ここで <math>T(\vec{x}, y)=1</math> となる <math>y</math> が存在しないとき、右辺は未定義と解釈する。

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

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

<syntaxhighlight lang="Pascal">
y := 0
t := 0
while t = 0 do begin
  t := T(x, y);
  if t = 0 then y := y+1;
end;
z := U(y).
</syntaxhighlight>

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

=== 可逆版 ===
可逆構造化プログラム定理<ref>{{cite journal |last1=Yokoyama |first1=Tetsuo |last2=Axelsen |first2=Holger Bock |last3=Glück |first3=Robert |title=Fundamentals of reversible flowchart languages |journal=Theoretical Computer Science |date=January 2016 |volume=611 |pages=87–115 |doi=10.1016/j.tcs.2015.07.046|doi-access=free}}</ref> は、[[可逆計算]]の分野における重要な概念である。この定理は、可逆プログラムによって達成可能な計算は、シーケンス、選択、反復といった制御フロー構造の組み合わせのみを用いる可逆プログラムによっても達成できると主張する。従来の非可逆プログラムによって達成可能な計算も、可逆プログラムを用いて達成できるが、その際には各ステップが可逆であり、追加の出力が必要となるという制約が加わる<ref>{{cite journal |last1=Bennett |first1=C. H. |title=Logical Reversibility of Computation |journal=IBM Journal of Research and Development |date=November 1973 |volume=17 |issue=6 |pages=525–532 |doi=10.1147/rd.176.0525}}</ref>。  さらに、可逆の非構造化プログラムも、追加の出力を伴わずに、1 回の反復のみで構造化された可逆プログラムを用いて実現できる。この定理は、構造化プログラミングフレームワーク内で可逆アルゴリズムを構築するための基本原理を提供するものである。

構造化プログラム定理には、局所的な証明方法<ref name="BohmJacopini"/>と大域的な証明方法<ref>{{cite journal |last1=Cooper |first1=David C. |title=Böhm and Jacopini's reduction of flow charts |journal=Communications of the ACM |date=August 1967 |volume=10 |issue=8 |pages=463 |doi=10.1145/363534.363539}}</ref>の両方が知られている。しかし、可逆版については、大域的な証明方法は知られているものの、BöhmとJacopini<ref name="BohmJacopini">{{cite journal |last1=Böhm |first1=Corrado |last2=Jacopini |first2=Giuseppe |title=Flow diagrams, turing machines and languages with only two formation rules |journal=Communications of the ACM |date=May 1966 |volume=9 |issue=5 |pages=366–371 |doi=10.1145/355592.365646}}</ref>が行ったような局所的なアプローチはまだ知られていない。この違いは、従来の計算パラダイムと比較して、可逆計算の基礎を確立する際の課題と微妙な差異を浮き彫りにする一つの例である。

== 影響と改良 ==
ベーム-ヤコピーニの証明は、プログラムを改良するよりもプログラムを不明瞭にする可能性が高かったので、ソフトウェア開発のために構造化プログラミング<ref group="注釈" name="sp">ここで言う構造化プログラミングは、[[エドガー・ダイクストラ]]の[[構造化プログラミング]]ではない。構造化定理を使ったプログラミングの意味である。</ref>を採用するかどうかという疑問を解決しなかった。

それどころか議論の始まりを告げることになった。[[エドガー・ダイクストラ]]の有名な文書「{{仮リンク|Go To Statement Considered Harmful|en|Go To Statement Considered Harmful}}（Go to 文は有害と考えられる）」は1968年にその議論に続いた<ref>{{cite journal|last=Dijkstra|first=Edsger|authorlink=Edsger W. Dijkstra|year=1968|title=Go To Statement Considered Harmful|journal=Communications of the ACM|volume=11|issue=3|pages=147–148|doi=10.1145/362929.362947|url=http://www.acm.org/classics/oct95/|deadurl=yes|archiveurl=https://web.archive.org/web/20070703050443/http://www.acm.org/classics/oct95/|archivedate=2007-07-03|df=}}</ref>。

幾人かの研究者はベーム-ヤコピーニの結論に対して純粋な手段を取った。そして、ループの途中にある <code>break</code> と <code>return</code> ですらベーム-ヤコピーニの証明に必要とされていないので悪い実践であると主張した。したがって全てのループは単一の脱出ポイントを持つべきだと主張した。この純粋な手段は[[Pascal|Pascalプログラミング言語]]（1968～1969に設計）で具体化された。Pascalは1990年代中頃まで大学の入門的なプログラミングの講義をするために好まれたツールであった。<ref name="roberts">Roberts, E. [1995] "[http://cs.stanford.edu/people/eroberts/papers/SIGCSE-1995/LoopExits.pdf Loop Exits and Structured Programming: Reopening the Debate]," ACM SIGCSE Bulletin, (27)1: 268–272.</ref>

[[エドワード・ヨードン]]は、構造化プログラミング<ref group="注釈" name="sp"/>の流行が始まった時からの議論に基づいて、1970年代に非構造化プログラムを機械的に構造化プログラムに変換することに哲学的な反対があったと述べている。実用本位の対照的なこととして、そのような変換が既存のプログラムの大きなコードに役立ったということもあった<ref name="Yourdon1979">{{cite book|author=E. N. Yourdon|title=Classics in Software Engineering|year=1979|publisher=Yourdon Press|isbn=978-0-917072-14-7|pages=49–50}}</ref>。機械的変換のための最初の提案の一つは、エドワード・アッシュクロフト（Edward Ashcroft）と{{仮リンク|ゾハル・マンナ|en|Zohar Manna}}（Zohar Manna）による1971年の論文であった<ref>{{cite journal|last=Ashcroft|first=Edward|author2=Zohar Manna |year=1971|title=The translation of go to programs to 'while' programs|journal=[[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</ref>。

ベーム-ヤコピーニの定理の直接的応用は、構造化チャートに導入されている余分なローカル変数（訳注：ループ途中脱出用のフラグのことだろうか？）といくつかの[[重複コード]]という結果になったのかもしれない<ref name="WattFindlay2004">{{cite book|author1=David Anthony Watt|author2=William Findlay|title=Programming language design concepts|year=2004|publisher=John Wiley & Sons|isbn=978-0-470-85320-7|page=228}}</ref>。後者の問題は、この状況で [[:en:loop and a half problem|loop and a half problem]] と呼ばれている（訳注：なぜ後者の問題なのかは英語版に書かれていない）<ref name="LoudenLambert2011">{{cite book|author1=Kenneth C. Louden|author2=Kenneth A. Lambert|title=Programming Languages: Principles and Practices|year=2011|publisher=Cengage Learning|isbn=1-111-52941-8|pages=422–423|edition=3}}</ref>。Pascal はこれらの問題の両方に影響されており、{{仮リンク|エリック・S・ロバーツ|en|Eric S. Roberts}}（Eric S. Roberts）によって引用された経験的研究に従っている。学生プログラマーであるロバーツは、いくつかの単純な問題（配列の中から1つの要素を検索する機能も含む）のために Pascal で適切な解法を公式化することに困難を感じた。ロバーツによって引用されたヘンリー・シャピロ（Henry Shapiro）による1980年の研究は、Pascal が提供する制御構造だけを使うと、適切な解法を得られた課題は20%だけだった。一方、ループの途中に return を書くことを許せば、この問題のために不適切なコードを書く課題は存在しなかった<ref name="roberts"/>。

1973年、{{仮リンク|S.ラオ・コサラジュ|en|S. Rao Kosaraju}}（S. Rao Kosaraju）は、任意の深さで multi-level break （多重ループから複数階層を一気に脱出できる break）を使えるようにすれば、構造化プログラミング<ref group="注釈" name="sp"/>において余分な変数の追加を回避できることを証明した。<ref name="kozen"/><ref>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 {{cite journal
 |  author = [[Donald Knuth]]
 |   title = Structured Programming with go to Statements
 | journal = Computing Surveys
 |  volume = 6
 |   issue = 4
 |    year = 1974
 |     url =
 |   pages = 261–301
 |   doi = 10.1145/356635.356640
}}</ref>さらにコサラジュは「プログラムの厳密な階層が存在する。それは現在 ''コサラジュ階層（Kosaraju hierarchy）'' と呼ばれている。''n'' はあらゆる整数である。深さ ''n'' の1つの multi-level break を含んでいるプログラムは、''n'' よりも小さい深さの multi-level break を使ったプログラムとして書き換えることはできない」ということを証明した<ref name="kozen"/>。コサラジュは [[BLISS]]プログラミング言語の multi-level break の仕組みを引き合いに出している。<code>leave ''label''</code> という形式の multi-level break は、実際に BLISS-11 で導入されていた。最初の BLISS は single-level break （一階層しか脱出できない break）のみを採用していた。BLISS言語ファミリーは制約のない goto を提供していなかった。[[Java|Javaプログラミング言語]]は、後に同様にこの手法を採用している<ref>{{cite journal | doi = 10.1002/spe.470 | title=The BLISS programming language: a history | journal=Software: Practice and Experience | date=2002 | volume=32 | issue=10 | pages=955–981 | first=Ronald F. | last=Brender | url = http://www.cs.tufts.edu/~nr/cs257/archive/ronald-brender/bliss.pdf}}</ref>{{rp|960–965}}。

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

マッケイブはこれらの4つのグラフが部分グラフとして登場するときに独立していないことを実際に明らかにした。プログラムが非構造化になるための必要十分条件は、そのCFGがこれらの4つのグラフから3つ選んで作った部分集合のどれか1組を部分グラフとして持つことである（訳注：4つのグラフのうち3つのグラフがCFGに含まれていたら非構造化になるということ）。彼は、もしも非構造化プログラムがこれらの4つの部分グラフの1つを含んでいるならば、その非構造化プログラムは4つの部分グラフからもう1つの異なる部分グラフを含まなければならないということも明らかにした。この後者の結論は、非構造化プログラミング<ref group="注釈" name="sp"/>の制御フローが一般的に[[スパゲティプログラム]]と呼ばれるものにどのようにしてなっていくのかを説明するのに役立つ。マッケイブは、あるプログラムが与えられたとき、それが理想の構造化プログラムからどの程度かけ離れているのかを定量化する数値測定手段も考案した。マッケイブは彼の測定手段を {{仮リンク|Essential complexity|en|Essential complexity}} と呼んだ<ref name="McCabe">The original paper is {{cite journal |author=Thomas J. McCabe |date=December 1976 |journal=IEEE Transactions on Software Engineering |issue=4 |pages=315–318 |title=A Complexity Measure|url=https://books.google.com/books?id=vtNWAAAAMAAJ&pg=PA3 |doi=10.1109/tse.1976.233837}} For a secondary exposition see {{cite book|author=Paul C. Jorgensen|title=Software Testing: A Craftsman's Approach, Second Edition|url=https://books.google.com/books?id=Yph_AwAAQBAJ&pg=PA150|year=2002|publisher=CRC Press|isbn=978-0-8493-0809-3|pages=150–153|edition=2nd}}</ref>。

マッケイブの構造化プログラミング<ref group="注釈" name="sp"/>における{{仮リンク|禁止グラフ|en|forbidden graph}}の特徴づけは不完全であると考えることができる。少なくともダイクストラのD構造（訳注：D構造の意味不明）は、建設用ブロックと見なされている<ref>{{cite journal | doi = 10.1093/comjnl/26.3.270 | title=Flowchart Schemata and the Problem of Nomenclature | journal=The Computer Journal | date=1983 | volume=26 | issue=3 | pages=270–276 | first=M. H. | last=Williams}}</ref>{{rp|274–275}}{{clarify|date=July 2014}}。

1990年まで既存プログラムのほとんどの構造を維持しながら goto を削除するためにかなり多くの提案された手法が存在した。この問題への様々な手段はいくつかの等価の概念も提案した。それらの概念は上で議論された民間伝承的定理のような結果を避けるために単純な{{仮リンク|チューリングマシン等価|en|Turing machine equivalents}}よりも厳密である。選ばれた等価の概念の厳密性は必要とされる制御フローの最小セットを要求する。ライル・ラムショウ（Lyle Ramshaw）による1988年の {{仮リンク|JACM (Journal of the ACM)|en|JACM}} の論文は、それまでのその分野を調査しており、さらに自身の手法も提案している<ref>{{Cite journal | doi = 10.1145/48014.48021| title = Eliminating go to's while preserving program structure| journal = Journal of the ACM| volume = 35| issue = 4| pages = 893–920| year = 1988| last1 = Ramshaw | first1 = L. }}</ref>。ラムショウのアルゴリズムは、[[Java仮想マシン]]コードがオフセットとして表現された対象を持つ分岐命令を持つので、Javaの[[逆コンパイラ]]の例のために使われた。しかし、上位レベルのJava言語だけは multi-level の <code>break</code> と <code>continue</code> 文を持っている<ref name="Nolan2004">{{cite book|author=Godfrey Nolan|title=Decompiling Java|year=2004|publisher=Apress|isbn=978-1-4302-0739-9|page=142}}</ref><ref>[https://www.usenix.org/legacy/publications/library/proceedings/coots97/full_papers/proebsting2/proebsting2.pdf Krakatoa: Decompilation in Java (Does Bytecode Reveal Source?)]</ref><ref>[http://www.openjit.org/publications/pro1999-06/decompiler-pro-199906.pdf paper.dvi] "Java バイトコードをデコンパイルするための効果的なアルゴリズム"</ref>。

Ammarguellat (1992年)は、ループの一箇所からの脱出を強制するために後戻りする変換手法を提案した<ref name="amma92">{{cite journal | doi = 10.1109/32.126773 | title=A control-flow normalization algorithm and its complexity | journal=IEEE Transactions on Software Engineering | date=1992 | volume=18 | issue=3 | pages=237–251 | first=Z. | last=Ammarguellat}}</ref>。

== COBOLへの応用 ==
{{see also|ミルズの構造化プログラミング}}
{{Refimprove section|date=August 2013}}
1980年代に[[IBM]]の研究員[[ハーラン・ミルズ]]（Harlan Mills）は、COBOL Structuring Facility の開発を監督した。COBOL Structuring Facility は[[COBOL]]コードへの構造化アルゴリズムを応用した。ミルズの変換は各手続に対して以下の手順を必要とした。

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

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

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

== 関連項目 ==
* [[構造化プログラミング]]
* [[チューリング完全]]

== 注釈 ==
{{Reflist|group="注釈"}}

== 出典 ==
{{reflist}}

== より詳しく知るための文献 ==
以上で扱われていない資料：
* {{cite journal | doi = 10.1145/322169.322180 | title=Space-Time Trade-Offs in Structured Programming: An Improved Combinatorial Embedding Theorem | journal=Journal of the ACM | date=1980 | volume=27 | issue=1 | pages=123–127 | first=Richard A. | last=DeMillo}}
* {{cite journal | doi = 10.1007/3-540-57785-8_128 | title=One binary horn clause is enough | journal=Lecture Notes in Computer Science | volume=775 | date=1994 | pages=19–32 | first=Philippe | last=Devienne| series=Lecture Notes in Computer Science | isbn=978-3-540-57785-0 }}

== 参考文献 ==
* {{cite book | title=Structured Programming: Theory and Practice | year=1979| author=Richard C. Linger,Harlan D. Mills,Bernard I. Wit | editor=IBM Corporation | url=https://trace.tennessee.edu/cgi/viewcontent.cgi?article=1008&context=utk_harlan | publisher=Addison-Wesley | ref=StructuredProgramming(1979) }}

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

{{プログラミング言語の関連項目}}

{{デフォルトソート:こうそうかていり}}
[[Category:ソフトウェア工学]]
[[Category:プログラミングパラダイム]]