- 1936年にアロンゾチャーチとチューリングはそれぞれ別の方法で、「一階述語論理の決定問題は解決不能」との
- 結論に至りました。この問題は純粋に数理論理学の課題を解決しただけですが、副産物としてコンピューターの「プログラム言語の祖型」を生み出すことになりました。
- 「アロンゾ・チャーチが考案したラムダ計算は、彼が一階述語論理のための一般的決定手続きが存在しないことを証明する手段となった。
- 「手続き型」あるいは「命令型」に分類される。
- ALGOLのような初期のプログラミング言語とラムダ計算の間に構造的な関係があることは、かなり以前から知られていた。ALGOLからはPASCALやCが派生し、CからはC++、JAVA、C♯といった多くの言語が派生した。
- 関数型プログラミング言語であるLISP、ALP、Haskell、Scheme、F♯等には、ラムダ計算がより直接的に影響している。
- チューチは思索の末に、λ定義可能な関数が実効的に計算可能な関数のすべてであると確信をもって提唱するに至った。(『チューリングを読む コンピューターサイエンスの金字塔を楽しもう』チャールズ・ペソルド著 日経BP社(以下チューリング)より引用)」
数理論理学は、コンピュータのプログラミング言語を産み落とし、その後の世俗社会を大きく変容させていきました。現在では、このプログラミング言語やネットワークなどにより、経済・軍事・生活などすべてのシステムが成り立つようになっています。そして、さらに急速にそれらは変革されつつあります。
人は知らず知らずのうちに、コンピューター(プログラミング)を通して、数理論理教的な精神に親和的になり、ある意味洗脳されているかもしれません。これは、プラトンが考えていた数理論理的なものによる「人間の矯正」に当たるかもしれません?
「アロンゾ・チャーチ(Alonzo Church、1903年6月14日 - 1995年8月11日)はアメリカの論理学者、数学者である。ラムダ計算の創案者や、「チャーチ=チューリングのテーゼ」の提唱者として知られる。(引用終わり)」
「チャーチ=チューリングのテーゼ (Church-Turing thesis) もしくはチャーチのテーゼ (Church's thesis) とは、「計算できる関数」という直観的な概念を、帰納的関数と呼ばれる数論的関数のクラスと同一視しようという主張である。テーゼの代わりに提唱(ていしょう)あるいは定立(ていりつ)の語が用いられることもある。このクラスはチューリングマシンで実行できるプログラムのクラス、ラムダ記法で定義できる関数のクラスとも一致する。よって簡単にはテーゼは、計算が可能な関数とは、その計算を実行できるような有限のアルゴリズムが存在するような関数、よっておおよそコンピュータで実行できる関数と同じだと主張する。
1932年にエルブラン、および1934年にゲーデルが、原始帰納的関数と呼ばれる自然数上の関数の明示的構成法を拡張して帰納的関数(もしくは一般帰納的関数)と呼ばれる関数の構成法を作り上げた。1933年から1935年ごろには、チャーチやクリーネがやはり関数の構成的な定義法であるラムダ記法を用いて定義可能な関数のクラスを定めた。さらに、1935年から1936年にかけてポストとチューリングは、チューリングマシンの概念を用いてこの理念的計算機械で実行可能なプログラムのクラスを定めた。
こうしてほぼ同時期に出現したさまざまな計算できる数論的関数のクラスは、実は互いに同じものであることが証明された。これにより、それまで非形式的に「実質的に計算できる関数」(effectively computable function) と呼び慣わされていたこのクラスをもってして「計算できる関数」とみなそうという主張がなされることになった。これがチャーチ=チューリングのテーゼと呼ばれている主張である。この意味で計算できる関数はチューリング計算可能な関数、あるいは単に計算可能関数と呼ばれるようになった。この主張自体はチャーチ、チューリング論文を参照して1943年にクリーネによってなされた。
この主張は数学的定理ではないので証明されるべき事柄ではない。「計算できる」という日常的な意味を考慮せず、純粋に形式的に考えるなら、この主張は単に計算可能関数の概念を定義したとも受け取れる。また逆に、これを「計算できる」という直観的概念に対する一種の仮説と受け取ることもできる。この最後の場合、チャーチ=チューリングのテーゼは、手続きに従って実際に行えるいかなる計算も、ここで示された帰納的関数のクラスを越えることはできないことを主張する。(引用終わり)」
「ラムダ計算(ラムダけいさん、英語: lambda calculus)は、計算模型のひとつで、計算の実行を関数への引数の評価(英語: evaluation)と適用(英語: application)としてモデル化・抽象化した計算体系である。ラムダ算法とも言う。関数を表現する式に文字ラムダ (λ) を使うという慣習からその名がある。アロンゾ・チャーチとスティーヴン・コール・クリーネによって1930年代に考案された。1936年にチャーチはラムダ計算を用いて一階述語論理の決定可能性問題を(否定的に)解いた。ラムダ計算は「計算可能な関数」とはなにかを定義するために用いられることもある。計算の意味論や型理論など、計算機科学のいろいろなところで使われており、特にLISP、ML、Haskellといった関数型プログラミング言語の理論的基盤として、その誕生に大きな役割を果たした。
ラムダ計算は1つの変換規則(変数置換)と1つの関数定義規則のみを持つ、最小の(ユニバーサルな)プログラミング言語であるということもできる。ここでいう「ユニバーサルな」とは、全ての計算可能な関数が表現でき正しく評価されるという意味である。これは、ラムダ計算がチューリングマシンと等価な数理モデルであることを意味している。チューリングマシンがハードウェア的なモデル化であるのに対し、ラムダ計算はよりソフトウェア的なアプローチをとっている。(引用終わり)」
アラン・チューリング(1912年から1954年)
「チャーチ=チューリングのテーゼと計算可能性理論への貢献が、まず真っ先に挙げられる。特に、アルゴリズムを実行するマシンを形式的に記述したものの一つである「チューリングマシン」にその名を残し、人によっては前述のテーゼを「チューリング=チャーチ」と呼称するべきであるとする者もいるほどである。また、任意のチューリングマシンを模倣(エミュレート)できる「万能チューリングマシン」は、同分野の基本的な定理のひとつである停止性問題の決定不能性定理と関係する。さらに、理論面だけではなく、実際面でもコンピュータの誕生に重要な役割を果たした[2][3]。コンピュータ科学および(チューリング・テストなどからは)人工知能の父とも言われる[4]。がっしりした体形で、声は甲高く、話好きで機知に富み、多少学者ぶったところがあったといわれている[5]。また、アスペルガー症候群を示唆する特徴の多くを示しているとの指摘もある[6]。(引用終わり)」
「計算可能性理論(けいさんかのうせいりろん、computability theory)では、チューリングマシンなどの計算模型でいかなる計算問題が解けるか、またより抽象的に、計算可能な問題のクラスがいかなる構造をもっているかを調べる、計算理論や数学の一分野である。
計算機科学の中心的課題の1つは、コンピュータを使って解ける問題の範囲を理解することでコンピュータの限界に対処することである。コンピュータは無限の計算能力を持つと思われがちだし、十分な時間さえ与えられればどんな問題も解けると想像することは易しい。しかし、多大な計算資源を与えられたとしても、見たところ単純な問題を解くことでコンピュータの能力の限界を明確に示すことは可能である。
計算可能性理論では、次の質問に答えることでコンピュータの能力を明らかにする。すなわち「ある形式言語と文字列が与えられたとき、その文字列はその形式言語に含まれるか?」である。この質問はやや難解なので、もう少し判り易く例を挙げる。まず、全ての素数を表す数字列の集合を言語として定義する。入力文字列がその形式言語に含まれるかどうかという質問は、この場合、その数が素数であるかを問うのと同じことである。同様に、全ての回文の集合や、文字 'a' だけからなる全ての文字列の集合などが形式言語の例である。これらの例では、それぞれの問題を解くコンピュータの構築の容易さが言語によって異なることは明白である。
しかし、この観測された明白な違いはどういう意味で正確なのか? ある特定の問題をコンピュータで解く際の困難さの度合いを定式化し定義できるか? その質問に答えるのが計算可能性理論の目標である。
計算可能性理論の中心課題に答えるために、「コンピュータとは何か」を形式的に定義する必要がある。利用可能な計算モデルはいくつか存在する。以下に代表例を挙げる。
- 決定性有限状態機械
- 決定性有限オートマトン(DFA)、あるいは単に有限状態機械とも呼ぶ。単純な計算モデルである。現在、実際に使われているコンピュータは、有限状態機械としてモデル化できる。この機械は状態の集合を持ち、入力列によって働く状態遷移の集合を持つ。一部の状態は受容状態と呼ばれる。入力列は一度に1文字ずつ機械に入力され、現在状態から状態遷移先への遷移条件と入力が比較され、マッチングするものがあればその状態が新たな状態となる。入力列が終了したとき機械が受容状態にあれば、全入力列が受容されたということができる。
- プッシュダウン・オートマトン
- 有限状態機械に似ているが、任意のサイズに成長可能な実行スタックを利用可能である点が異なる。状態遷移の際に記号をスタックに積むかスタックから記号を除くかを指定できる。
- チューリングマシン
- これも有限状態機械に似ているが、入力が「テープ」の形式になっていて、読むだけでなく書くこともでき、テープを送ったり巻き戻したりして読み書きの位置を決めることができる。テープのサイズは任意である。チューリングマシンは時間さえかければ、かなり複雑な問題も解くことができる。このモデルは計算機科学では最も重要な計算モデルであり、資源の限界がない計算をシミュレートしたものである。
- (引用終わり)」
1928年ヴァネバーブッシュらが微分解析機を作成、ENIAC(射撃表作成のため開発)に影響を与える。
「ヴァニーヴァー・ブッシュ(英: Vannevar/væˈniːvɑr/ Bush、1890年3月11日 - 1974年6月30日)は、アメリカの技術者・科学技術管理者。アナログコンピュータの研究者、情報検索システム構想「メメックス」(memex) 提唱者、MIT副学長、また原子爆弾計画の推進者として知られる。
- 1913年、タフツ・カレッジを卒業。
- 1917年、ハーバード大学とマサチューセッツ工科大学から工学博士号を授与される。
- 第一次世界大戦中、米国学術研究会議で働き、潜水艦を発見するための技術を開発。
- 1919年、MITの電気工学科に移籍し1923~32年の間、教授として在職。このとき、18変数の微分方程式を解くことが出来るアナログコンピュータである微分解析機を開発した。そのときの教え子クロード・シャノンはデジタル回路を生み出した。
- 1932~38年には、MIT副学長と工学部学部長を務めた。
戦時中
- 1939年、ワシントン・カーネギー研究機構の総長職となった。この研究所は権威が高く評価されていて研究資金も潤沢であった。ブッシュはアメリカ国内の研究の方向性を左右する力を得て、軍事的な方向に舵を取るとともに非公式な政府の科学顧問としても助言をする立場となった。また、アメリカ航空諮問委員会の議長も務め、政治的役割を鮮明にした。
- 1940年、アメリカ国防研究委員会(NDRC)の議長となる。ブッシュはNDRC設立を強力に推し進めた。というのも第一次世界大戦の際に科学者と軍の協力関係がうまく機能していないことを見てきたからであった。ブッシュは1940年6月12日に大統領と会談し、部局の新設についての文書を得た。ルーズベルトはそれを10分で許可したという。政府はブッシュが権力を握って政府を無視して事を進めるのを苦々しく思っていた。ブッシュは後に「その通りだった」と認めている。この軍と科学の協力関係によって第二次世界大戦に勝利したと言っても過言ではない。レーダー科学者アルフレッド・ルーミスは「1940年の夏に、あの男たちが死んでいたら、その後は大変な惨状が待っていただろう。その第一は大統領であり、二番目か三番目にDr.ブッシュが挙げられる」と言った。
- 1941年、NDRCはブッシュが局長を務める科学研究開発局の一部となり、同局はマンハッタン計画を含む戦時中の科学研究の調整・制御役を演じた。
- 1943年、アメリカ電気学会からエジソンメダルを授与された。
戦後
ヴァネバーブッシュは、巨大軍事科学のシステムを作り上げました。エリア51等で行われたマンハッタン計画の主導者でした。この時から、軍事とは巨大科学を意味することになりました。
1937年シャノン、リレーとスイッチで回路の記号論的解析
「クロード・エルウッド・シャノン(Claude Elwood Shannon, 1916年4月30日 - 2001年2月24日)はアメリカ合衆国の電気工学者、数学者。20世紀科学史における、最も影響を与えた科学者の一人である。
情報理論の考案者であり、情報理論の父と呼ばれた。情報、通信、暗号、データ圧縮、符号化など今日の情報社会に必須の分野の先駆的研究を残した。アラン・チューリングやジョン・フォン・ノイマンらとともに今日のコンピュータ技術の基礎を作り上げた人物として、しばしば挙げられる。
デジタル回路設計の創始者
1937年のマサチューセッツ工科大学での修士論文「継電器及び開閉回路の記号的解析」[2]において、電気回路(ないし電子回路)が論理演算に対応することを示した。すなわち、スイッチのオン・オフを真理値に対応させると、スイッチの直列接続はANDに、並列接続はORに対応することを示し、論理演算がスイッチング回路で実行できることを示した。これは、デジタル回路・論理回路の概念の確立であり、それ以前の電話交換機などが職人の経験則によって設計されていたものを一掃し、数学的な理論に基づいて設計が行えるようになった。どんなに複雑な回路でも、理論に基づき扱えるということはコンピュータの実現に向けたとても大きなステップの一つだったと言える。
ハーバード大学教授のハワード・ガードナー(Howard Gardner)は、この論文について「たぶん今世紀で最も重要で、かつ最も有名な修士論文」と評した。ただし、わずかな時間差であるが、中嶋章による発表の方が先行しており(論理回路#歴史を参照)、独立な成果か否かは不明とされている。
情報理論の考案
1948年ベル研究所在勤中に論文「通信の数学的理論」[3]を発表し、それまで曖昧な概念だった「情報」(information)について定量的に扱えるように定義し、情報についての理論(情報理論)という新たな数学的理論を創始した。(引用終わり)」
1948年 MARK1開発、プログラム内蔵方式コンピュータ
チューリングはプログラム面のほぼすべての責任を負う、記憶装置はCRT(陰極線管)を用いる。
1948年ノイマン、シンポジウムでオートマンの一般的・論理的理論と題して発表。
※コメント投稿者のブログIDはブログ作成者のみに通知されます