「数学観」が技術を動かす
【「数学観」が技術を動かす -- 可哀想な数学 】
前回は、数学の基礎と計算機科学を直接結びつける重要な数学的発見が、1930~40年代にあったものの、肝心のコンピュータは、存在していなかったというという話をしました。今回はその後の時代の話です。
【 20世紀後半での数学と計算機科学の接点 -- 「形式手法」と「従属型理論」】
20世紀の後半コンピュータが登場し、1960年代にはその利用が急速に拡大する中で、数学と計算機科学の接点を探ろうという研究は活発になります。
1970年代には、二つの研究の流れが独立に生まれます。
一つは、計算機科学の側から生まれた、具体的なプログラムの分析を通じて、計算機科学の数学的基礎づけを目指す動きです。「形式手法」と呼ばれています。
もう一つは、論理学＝数学の側から生まれた、新しい「型の理論」である「従属的型理論」を構築して、プログラムとその実行の数学的特徴を捉えようとする動きです。
前者の「形式手法」の代表はホーアやダイクストラです。彼らは、代入文やif文、シーケンシャルな実行や繰り返しのWhile文といった具体的なプログラムの構成と論理との関係を研究しました。
後者の「従属的型理論」の代表は、ハワードやマーチン・レフです。彼らは、「型の理論」を作り上げ、抽象的ですが、プログラムの実行は、ある定理の証明に他ならないという認識にたどり着きました。
両者のアプローチは異なっていましたが、「プログラムと論理」という問題意識は共通のものでした。 ただ、 20世紀の段階では、「プログラムと論理」という問題を扱うには、両者共に、いろいろな困難がありました。
論理学＝数学からのアプローチではある「従属型理論」は、現実のコンピュータ技術や具体的なプログラム言語との接点は明確ではありませんでした。そのスキマを埋めるのには、実際には、前回見たように 30年から40年の時間が必要でした。
計算機科学からのアプローチでは、論理の多様な性質への理解を欠いていました。実践的には、彼らの理論を実行する強力な「証明マシン」は存在しませんでした。ただ、それ以上の「障壁」があったように、僕は感じています。それが、今回のセッションの一つのテーマです。
今回のセッションでは、ホーア、ダイクストラ、ランポートらの「形式手法」の登場と挫折を取り上げます。
【 20世紀の「形式手法」の登場と挫折 -- ホーアとダイクストラ 】
「形式手法」は、1969年のホーアの "An axiomatic basis for computer programming （コンピュータ・プログラミングの公理的基礎）" という論文を嚆矢とします。
この論文執筆の動機を、彼は次のように説明しています。
「コンピュータ・プログラミングは、正確な科学である。その中では、プログラムの全ての性質と、どんな環境の下でそれが実行されたとしても、その実行の結果は、原理的には、プログラム自身のテキストから、純粋に演繹的推論の手段で見つけ出すことができる。」
彼の問題提起は大きな波紋を呼び、「形式手法」はダイクストラや若いランポートをはじめとする優秀な研究者を結集して大きな勢力に成長します。そのままの勢いで進んでいたら、数学と計算機科学の統一は、彼等の手で成し遂げられていたかもしれません。
ただ、20世紀の「形式手法」は、その勢いを失っていきます。直接のきっかけは、「形式手法」のムーブメントを牽引していた「ツートップ」のホーアとダイクストラのうちの一人であるホーアが「形式手法」を放棄し、やがて、「形式手法」批判の陣営に加わったことです。
のちの 1996年には、ホーアは次のようなタイトルの論文を発表しています。証明なしでも安全なプログラムは作れるという立場です。"How did software get so reliable without proof ? （いかにして、ソフトウェアは証明抜きでも、こんなに安全なものになったのか）"
ダイクストラは、2002年に亡くなるのですが、最後まで「形式手法」の立場に立っていました。最晩年の2001年に彼があらわした 「ライプニッツの夢の魔力の下で」 ”Under the spell of Leibniz‘s Dream” は、いわば彼の21世紀への「遺言」ともいえる文書です。「形式手法」の「思想」に興味ある方は、ぜひ、お読みください。
【 転換点となった一つの論文 】
こうした変化の転換点に、一つの論文がありました。
1979年、ACMは、その論文誌CACMに、形式的手法を「失敗するように定められている」と一方的に断罪する論文を掲載しました。
タイトルは、“Social Processes and Proofs of Theorems and Programs” というものです。 https://www.cs.umd.edu/~gasarch/BLOGPAPERS/social.pdf
「この論文では、プログラムの形式的検証は、たとえそれが得られたとしても、計算機科学とソフトウェア・エンジニアリングにおいては、数学での証明と同じ役割は果たす事はないと議論される。」
「プログラムの検証者たちの間に、数学と比較できるような社会的プロセスが存在しないのだから、プログラムの検証は、失敗するように定められていると、我々は信じている。」
この露文のキーワードは、タイトルにもある "Social Process" なのですが、このキーワードとの関連で、彼等は次のような「数学観」を展開します。
「数学では、証明の目的は、ある定理の正しさに対する人の確信を増大させることである。... しかし、事実はそうではない。彼らが使う証明は、全く別の生き物なのだ。証明は、問題を解決さえしない。 」
「証明は、その名が示唆するものとは逆に、確信に向かう一つのステップにすぎないのだ。結局のところ、数学者がある定理に確信を持つか否かを決定するのは、社会的プロセスなのだと我々は信じている。」
数学論的には、全くの愚論です。ただ、こうした「数学観」が、人々に大きな影響力を持ち、「形式手法」は役に立たないという立場に立たせ、技術を動かすのです。
【 かわいそうな数学 】
以下は、全くの私見です。読み飛ばしてもらっても構いません。
ではなぜ、こうした愚論に、人々は従ったのでしょうか？ それは先の論文が説得力を持って、優れた数学論を展開していたからではないと僕は思います。
それ以前に、「プログラミングに数学はいらない」という経験に根ざした感覚が根強くあって、「形式手法」を受け入れられない人が多数存在していて、そうした立場を補強する「理論」なら、なんでもよかったのではないかと思います。
実際には、そうした意識・感情は、「日常の生活に数学はいらない」というもっと大きな意識・感情と陸続きにつながっています。
かわいそうなのは数学です。多くの人に、「俺には、お前はいらない」「俺の仕事には、お前は役に立たない」と思われているのです、
そうした、数学に対する人々の意識の状況は、ChatGPT等が、「数学ができない」という「人工知能」技樹としては、大きな弱点を持っているにもかかわらず、「何か役に立ちそうだ」と称賛されている奇妙な現実を説明するものだと、僕は考えています。
-------------------------------------
「 「数学観」が技術を動かす -- 80年代の「形式手法の後退」を振り返る」を公開しました。
https://youtu.be/2SyqsnXIjZY?list=PLQIrJ0f9gMcMMwP2zBgMe3LbaDnKGG_zw
資料pdf
https://drive.google.com/file/d/10a2vW-JBG780P1rsKS3QcKEDC4Ubn4ga/view?usp=sharing
blog：「 「数学観」が技術を動かす -- 可哀想な数学 」
https://maruyama097.blogspot.com/2023/03/blog-post_16.html
まとめページ
https://www.marulabo.net/docs/aimath/
コメント
コメントを投稿