数学とはなにか、という議論をする中で、「形式化」というアイデアが出てきました。形式化によって数学の完全性や無矛盾性を証明することはできませんでしたが、数学をきっちりと定義したり、機械で実行するのにはとても有用な方法で、このアイデアを応用してコンピュータが作られました。
そこで、形式化とは具体的にどういうことなのかを、その方法の一つであるチューリングマシンで見てゆきます。
ここではチューリングマシンを、列車とカードで表してみました。
数学や論理を含めて、あらかじめ定められたルールに従って記号を置き換えてゆくようなものは、すべてこのチューリング・マシンで表現ができるわけです。
ここまでを見ると、ルールは線路として決められたものになっているように見えますが、実はもっと柔軟にすることができるのです…という話を次回、万能チューリングマシンでする予定です。
参考文献
『ファインマン計算機科学』A.ヘイ、R.アレン編 岩波書店
ファインマン物理などでお馴染みのシリーズの、計算機科学版。全7章のうち、3章がチューリングマシンについて。コンピュータの実現方法や、情報理論の基礎など、計算機科学の基礎について、幅広く知りたい人におすすめ。
『計算理論の基礎1オートマトンと言語』『計算理論の基礎2計算可能性の理論』『計算理論の基礎3複雑性の理論』Michael Sipser共立出版
特に計算理論について、3冊にわたって解説したもの。2巻が、チューリングマシンと計算可能性についての解説。1巻は、チューリングマシンよりも能力の弱い、有限状態マシン(テープの書き換えをしない機械)や、プッシュダウンオートマトンについて。3巻は計算の複雑性(実際に問題を解くには、どのくらいの計算をしなくてはならないのか)についての話。
スタンフォード哲学辞典ーチューリングマシン(WEB、英語)
http://plato.stanford.edu/entries/turing-machine/