私的コンピュータ論義

ここでは話題として２０世紀になってから全盛期を迎えたディジタルコンピュータについての私の知識内での論議を行っていくつもりです。

前史

私が計算する機械に興味を持ったのはいわゆる珠算（以前はタマザンと呼ばれ５つ玉だったのが後に４つ玉となりシュザンと呼ばれる）つまり算盤の学習が小学校でも始まり、これに対する練習なる作業に疑問を持ったためである。
これはある意味で最も原初的な計算機械ではあるが、肝心の論理的機構は全て人間の頭脳に頼り、ここで桁上げ・桁下げのルールを記憶させそれによって計算を手早く行わせるものである。
よく計算機の元祖として挙げられる数学者パスカルが若いときに作成した計算器はこの桁上げ・桁下げの論理を機械的に行わせる機構のことで算盤の学習で訓練によって頭脳に記憶させそれを指先の運動として行わせるものをメカで実現したものである。
減算はできず、何台か作ったがあまり売れなかったとか。



写真はミュンヘンのドイツ博物館に展示のレプリカであり、当時にこの種のものは多くの人々が自分用に「発明」していたようであるが、まだ工業化以前であり、しかも徒弟制度の社会においては限定的な用いられ方しかされなかったのは自然なことで、パスカルの話も彼が歴史的に有名だったから伝わったのであろう。
後に工業化が進むにつれて質の良い素材が量産されるようになるとこの計算機はその材料を用いることで付加価値の高い機関銃、タイプライタなどと並べられる精密工業製品として市場に提供されるようになった。
これらはいずれも優れた鉄鋼材料と精度の高い加工技術の組み合わせによるもので、それによって金属部分の摩耗や変形に耐えて工業製品として受け入れられるようになっていった。
これらの計算機は置数を入力し、それに対する加減算をハンドルの回転で行うものであるが、やがてこの回転を電動機で行わせることで高速化を図った（当然に高速の回転による摩耗や発熱に耐える機構・材料面での技術革新が要求される）ものは出現し事務機械の代表のようになっていった。
１９世紀半ばに英国のチャールズ・バベッジが当時に発展中の機械技術を利用して数学的課題を解くための解析機械の作成を試みたことは有名である。
この装置は当時の動力である蒸気機関を用いてのもので技術的・資金的に挫折となり一種の文化的遺産としてカリフォルニア・マウンテンビューにはこの装置を実際に復元して動作する展示物があるそうです。



ここには詩人バイロンの妹Ada夫人がプログラム作成に参加したとのエピソードがあって、そのために１９７０年代に米国国防総省が入札により次の兵器体系に用いる言語を発注したとき提案されたプログラム言語にAdaとして名前を残しています。
この言語Adaは最初の国際的に規格化された言語として日本でもJISの標準に登録されています。しかし、現行の数多くのシステムでAdaを用いての開発が行われているのはあくまで少数派のようです。

同じく１９世紀半ばに英国のBooleが、かつてカントによって「アリストテレス以来進歩も退歩も見受けられない奇妙な学問」とまで言われた論理学に数学的記号演算の導入を試みたBool代数と言うものを提案します。
これは論理の状態を真・偽の二値として定義し、関係を機械的な演算操作により意味や解釈とは独立した形式化を行う提案でした。
この記号論理学では述語（Predicate）は真・偽のいずれかに限定され（そうでないものは対象外）、これの連言（両者が真の場合にのみ真となるAND演算）、選言（両者のいずれかが真である場合のみ真となるOR演算）、否定（結果で真・偽が入れ替わるNOT演算）として定義されます。Booleの当初の定義では選言は両者が真である場合には偽とするいわゆる排他的連言でしたが、後に現在のように改められました。
この成果は余り評価されることもなく放置されていましたが、やがて数学者が厳密な証明を定義づけるために記号論理学に注目するようになります。
このときには一般の証明に用いられる全称（全ての述語が真となる）、存在（ある述語が真となることがある）を含めての記号化により証明の過程を記号化するものです。
ここでの最初の成果として従来の言葉で記述された幾何学が形式化によって完全に記述できたのを受けて、全ての数学の分野の公理や定理を記号論理学による形式的な手続きで記述すると言う目標に世界的な数学者の多くが取り組みます。
その成果と言われるのが英国の数学者バートランド・ラッセルの「数学の原理」なのですが、後にこれが基礎を置いていた集合論には基本的問題を内包していることが判明し、その解決は２０世紀に持ち越されます。

２０世紀になってから数学的論理学は証明の形式化を厳密に行う数論の形で研究が進み、１９３０年代にChurch、Post、Turingなどの論理学者によって形式的手続き（まあ言うなればプログラミングのような手法）によって証明を記述する方法がいくつか提案されますが、そこからこの手法では証明することができない問題もあることも判明してきます。
ちなみに背景はチューリングの論文「計算可能数について──決定問題への応用」の冒頭の部分であり、この論文で仮想の計算機チューリングマシンが初めて紹介されたものです。
この手法はまだコンピュータが実用化される以前から仮想のコンピュータの上で議論が行われていたことには注目することが必要です。
この成果を統合して論理学者Kurt Goedelはこのような形式化によって証明することが不可能な問題が存在すること、つまり形式論理は証明に関して閉じていないことを述べました。
これは判りやすい言葉で述べるなら、形式的手続きの有限回の繰り返しによっては解が存在するかどうかを判定することができない種類の命題が存在すると言う事実です。
これは数学者・論理学者の間では薄々気づいていた事実なのですが、この発表は世界的に大きな反響を呼び、物理学における不確定性原理と並んで思想界にも大きな影響を与えました。

このようにまだディジタルコンピュータが開発される以前からこの種の形式化による問題解決を支援する装置に対する期待は熟成されていたのです。
しかし最初に生まれたディジタルコンピュータはこの種の期待からは遠いものでした。