当事者のIT技術者に見えにくい「リンク」
【 当事者のIT技術者に見えにくい「リンク」】
先に、”Proof as Program プログラムとしての証明” という認識が、Curry-Howard対応の発見や従属型理論の登場の中で、生まれてきたことを述べてきました。
それは、論理的＝数学的証明は機械のプログラムで実行できるということ、ひるがえって言えば、機械は論理的＝数学的推論能力を持つという認識に他なりません。
この認識は、人工知能論にとって本質的に重要な認識であると、僕は考えています。
このセッションでは、改めて、「計算」＝「証明」＝「プログラム」という認識がどのように形成されてきたのかを、 振り返りたいと思います。
「計算」「証明」「プログラム」という三つの言葉は、もともと別の意味を持っています。それは今でも同じです。そして それぞれがそれぞれの歴史を持っています。
この三つの言葉の中で、「計算」の起源が一番古いものです。4000年以上前の古代バビロニアでは、2の平方根の値も知っていたし、ピタゴラスの定理で直角三角形の斜辺の長さを計算する「計算表」も持っていたといいます。人間は、具体的な「計算」を通じて数学の世界の扉を開きました。
「証明」の概念の起源は、2300年前のユークリッドに帰してもいいと思います。古代ギリシャ人は、具体的な数の「計算」とは異なる数学の世界があることに気づきました。プラトンは彼のアカデミアの門に、「幾何学を知らざるものこの門入るべからず」と掲げたと言われています。彼らにとって、「数学的証明」は「真理」に到達する、重要な方法だと認識されていたと思います。残念なことに、ギリシャ数学の伝統は中世ヨーロッパでは途絶します。
この中で、「プログラム」という概念が一番新しいものです。その起源は、コンピュータが登場した1950年代を遡ることはないのは明らかですので。
このセッションは、機械の能力を人間がどう認識してきたかを、「計算」「証明」「プログラム」という三つの概念の関係の認識の歴史をメイン・ストーリーにして述べたものです。
さきに、概略を述べておきましょう。（以前のセッションと内容的には重なっています。）
まず、「計算」と「証明」が、本質的には同じものであるという認識が生まれます。1930年代のことです。
それから40年ほど経って、「プログラム」は「証明」とみなせるという認識が生まれます。1970年代のことです。
理論的には、この二つの発見で、三項の関係は明確になりました。「コンピュータは、プログラムの実行という形で、証明を計算する」ものなのです。
「計算」＝「証明」＝「プログラム」というテーゼの中では、IT技術者には、「プログラム」＝「計算」というのが、一番わかりやすいように思います。 「プログラム」＝「アルゴリズム」＝「計算」と考えればいいのですから。
この認識は、コンピュータの普及と、ITビジネスがコンシューマ中心にシフトして成功する中で、また、多くの人がIT技術者になる中で自然に拡大しました。
ただ、こんな問題もあります。
現代では、誰もが「コンピュータはプログラムで動く」ことを知っています。ただ、コンピュータは、万能の「情報処理機械」とみなされていて、それが「計算する機械」であることを意識する人は少ないのです。
インターネットにしろYoutubeにしろFacebookにしろ、そのサービスを実現するソフトウェアが存在することを、多くの人は知っています。ただ、その基礎が、足し算や掛け算、電卓と同じ「計算」であることに、思いはいたっていません。
サービスを開発するIT技術者自身、数値計算でもしない限り、自分たちの仕事が「計算」の領域に属するという意識は薄いように思います。
「プログラム」＝「計算」という、IT技術者にはわかりやすいはずのリンクにしても、こうした状況がありますので、「計算」＝「証明」、「証明」＝「プログラム」というリンクは、見えにくい「リンク」なのかもしれません。
「チャーチ=チューリングのテーゼ」や「カリー=ハワード対応」に言及することなく、これらのリンクを理解することは可能でしょうか？
僕は、「プログラムの行っていることは、基本的には、計算である」ということが腑に落ちれば、十分可能だと思っています。
なぜなら、ラムダ計算もチューリング・マシンも、人間が行う計算の、プリミティブだが忠実なモデルに他ならないからです。それは、コンピュータが行なっている計算と同じものです。計算に関して言えば、人間とコンピュータに違いはないのです。
-------------------------------------
https://ai-math.peatix.com/
コメント
コメントを投稿