数学の本第78巻
■ このスレッドは過去ログ倉庫に格納されています
え？数学的思考力ってプログラミングの領域で生かせらレるんだがCやJavaの入門書ぐらいはやってるよな？ プログラミングをCやJavaに短絡する香具師は
定理証明機を触ったこともない階層なんだろ
その程度が知れるねぇｗ >>148
アルゴリズムの記述は ALGOL とか
数値計算だと Fortran とか
ホーン節の論理だと Prolog とか
言語っちゅーのとは違うけど数式処理だと
MatheMatica とか
いろいろ歴史的な経緯がある。
C はシステム記述用で、マシンの性能を引き出すのに
好都合なので、有限組合せ数学とかを
ゴリゴリ計算するのによく使われた。
Java は C より見通しがいいんで、
ちょこちょこ数値実験に使われたりする
グラフィクスが充実してるんで、
マンデルブロ集合やジュリア集合の
描画にも使えて便利だけど、
中学・高校あたりの数学教育で数値実験に使うん
だったら BASIC が便利かもしれない。 >>147
> まあそんなプログラマ皆無でしょう
皆無ではないが、かなり少ないのは確かだな（笑）
ＬＩＳＰハッカーで、「日本のストールマン」と
呼ばれた竹内郁雄先生は東大の数学科出身で、
たしか竹内外史先生と同年度なので、
「ダメなほうの竹内」と呼ばれていたと
エッセーに書いていらっしゃった。 >>150
学校の授業でBasicやLisp、Prolog触ったことはあるけど、正直あんなもののどこが役に立つんだって言う印象のまま終わった
Javaに追加されるライブラリだけじゃダメなものなの？ >>149
定理照明器がCやJavaとは違った何か特別な事ってアるん？ >>152
BASIC（パソコン用じゃなくてオリジナルの方）は
行列式が扱えたので非線形多元方程式で記述される
システムの数値計算、
LISP は数式処理、
Prolog は定理証明に使われたことがある。
いちいち Java を使うより、問題向き言語やら
使いやすいアプリやらがあるから、そっちを
使ったほうが楽だよ。プログラミングが好きなら、
また別だけど。 >>153
読みやすさと直観的な解りやすさ。
同じことはアセンブラでも C でも書けるけど、
書いた本人でもなきゃ読んでわからん。
Java は C よりわかりやすいが、
たぶん数学屋が求めているのとは
別の種類の “わかりやすさ” だ。
あとは、定理証明系や将棋プログラムや
自然言語処理系は、中で疑似超並列処理を
行なってるのが違いっちゃあ違いかな？
つまり、処理の対象が有限束みたいな
構造を持ったデータだという違いがある。 CSの授業でもやると思うんだけど少し歴史をおさらいしよう。以下、長いので２回に分ける。
微積分や複素解析の発展とともに解析の基礎が数学の大きな問題となった時期があった。
その時期に活躍したのがデデキントとカントールだ。デデキントはまず実数をデデキント切断を導入して定義し、
続いて整数を公理論的に定義した。この時、五つほどの公理から推論されるように定義した。
この定義には無限集合という罠があることがカントールから指摘され、集合論を厳密に定義することが問題になった。
これに答えたのがフレーゲやラッセルだった。
ラッセルはプリンキピア・マセマティカのなかで算術を説明するためにΛ「ラムダ」記号を導入した。
このラッセルの仕事を受けてゲーデルが不完全性定理を証明した。
この仕事でゲーデル独特の定理証明機とゲーデル数による計算可能関数を導入している。
さらにゲーデルの仕事を受けて、アロンゾ・チャーチとチューリングが登場する。
チャーチはラッセルのΛをさらに洗練させたラムダ算法を構築してλ記号を導入し、
ゲーデルの計算可能関数がλ記述可能関数と同等であることを示した。
チューリングはチューリング機械を導入して、ゲーデル＆チャーチと同様に
計算可能関数が再帰関数と同等であることを示し、チューリング完全という概念を得た。
今日の一般的なプログラミング言語はチューリング完全で、ゲーデル＆チャーチ＆チューリングの仕事を基礎にしている。 戦後にはコンピュータが発展するとともに、ソフトウェアも高級言語が開発された。
ダイクストラがチューリングの手法を発展させて手続き型言語の先祖にあたるALGOL60を開発するとともに、アルゴリズムを発展させた。
またブルックスらがALGOLを発展させたFortranで初めてコンパイラを手動で書き上げた。
このFortranを簡易化して出来たのがBasic言語だ。
一方、ジョン・マッカーシーは、チャーチのラムダ算法を発展させたラムダ関数の理論を基礎に持つLisp言語を開発した。
このLispからはカール・ヒューイットのPlannerや論理型のPrologが派生した。
ケン・トンプソンとデニス・リッチーはC言語とUNIXを導入して汎用OSと記述言語の基礎を作った。
さらに時代が下るとXerox Parcのアラン・ケイがSmalltalk言語を開発してオブジェクト指向を発展させた。
最後に関数型言語が発展する。特に四色定理の証明に使われた定理証明機Coqの基盤となったOCaml言語やHaskell言語が有名。
最近ではLisp系のACL2や入門用に簡易化したJ-Bobなんかもよく使われている。
ざっと流れを書いたが、細かい間違いもあるかもしれない。請寛恕我的罪。 >>153
Javaだって最近になってLambda関数は導入されたから、SchemeのminiKanrenが容易に移植できた。
しかし、今の所はJavaで定理証明はまだ出来ない。
そのうちJavaで定理証明が出来るようになるまでここが最大の違い。
なぜってプログラムの関数を定理証明しながら書けば、間違いなくバグフリーだから。
古い言語の最大の弱点だろうね。 ちなみにJavaでも一階述語論理の定理証明までならleanTAPを移植したものが存在する。
興味があれば見てみると勉強にはなると思う。 ■ このスレッドは過去ログ倉庫に格納されています
