IT練習ノート

IT関連で調べたこと(実際は嵌ったこと)を書いています。

コンピュータは数学者になれるのか

感想が書けるほど知見がないし、理解しているわけでもないので、メモです。

この本を読んで一つだけ言えるとしたら、「証明はプログラムである」が実感できる本だと思います。

以下メモ

すなわち公理とは推論規則の特別な場合に過ぎないことになる 。

→特別なのか。

小学校で足し算や掛け算を教わるときには 、九九を覚えたり繰り上げのやり方を習ったりするが 、人工数学者の記法を用いれば 、足し算掛け算はたった 4つの規則で済ますことができる 。これは十進法ではなく一進法を採用しているからである 。

→確かに、2進法や60進法があるなら、1進法もあり。

たった 1つの (ただし任意の ) yについて検証することにより 、無限に多くの xについての検証が完了する 。これはすごいことではないだろうか 。

→任意と全ての違いがわからない

このように擬人化して理解しておくと 、次章で出てくる第二不完全性定理の議論が格段にわかりやすくなる 。

→なんと!

ここでの意図は現代へのつながりにある 。とくに 1 9 7 0 − 8 0年代には 、計算の時間的制約のもとで 1 9 3 0年代と同様の試みが繰り返されるも 、その悉くが失敗するという事態が生じている 。

→マシンパワーが飛躍的に進展した今はどうなるか

チュ ーリング機械がハ ードウェアレベルの計算の基礎となったのに対し 、エルブラン ・ゲ ーデル ・チャ ーチ ・クリ ーネらの研究はソフトウェアレベルの計算の基礎となったのである 。

→ハードとソフトの基礎づけは出自が異なっていた。

「人間が紙と鉛筆を使って計算する物理的プロセス 」を抽象化したのがチュ ーリング機械 ( 2 . 3節 )なら 、 「数学者が関数を作ったり使ったりする数学的プロセス 」を抽象化したのがラムダ計算である 。

→同じことを5章でもいっている。

2つのラムダ項 Mと Nの対 (ペア )を作るには 〈 M , N 〉 : = λ a . a M N

→aに射が入る

チャ ーチが 1 9 3 2年にラムダ計算を導入した意図は 、集合論に代わる数学の基礎とすることであった (もちろん即座に矛盾が生じて使いものにならなかったのであるが ) 。

→チャーチが今のプログラミング言語のラムダをみたら何を思うのか?

同じ対角線論法を使うのでも 、ラッセルのパラドックスは厄介事でしかなかったが 、これが不動点となると途端に有用になる 。

→おぉ

次に 「証明はプログラムである 」…要は証明図をラムダ項で表そうということに尽きる 。

→ラムダ項=プログラム=証明図

では出発点である公理や仮定にはどのようなラムダ項を割り当てればよいだろうか ?公理に対しては 、適当にラムダ項を割り振る 。

→適当?

一般に論理式は 、ラムダ項を分類する型と見なすことができる 。

→ ラムダ項:論理式 を ラムダ項:型 と見なす

かくして証明はプログラムと対応し 、証明の書き換えはプログラムの実行 ( β簡約 )と対応し 、さらに論理式は型と見なすことができる 。以上を合わせてカリ ー ・ハワ ード対応 ★ 9という (図 5 . 6 )

→対応するものが3個ある。

応用上実際に求められているのは 、証明からプログラムを抽出すること (プログラム抽出 )なのである 。

→はい。

a ^ b が有理数となる2つの無理数a,bが存在する。

→非構成的証明の例

二重否定律 ¬ ¬ A → Aである 。 A → ¬ ¬ Aは構成的に証明できるのだが 、その逆がいえない 。

→なんで?

構成性を巡る真にエキサイティングでチャレンジングな問題は 、非構成的な証明から構成的情報を引き出すことなのである 。

→種がないのになにかを生み出すと。

あなたは魔法使いとの対話を通して自分のカ ードを更新していく 。これは機械学習理論的な意味での “学習 ”に他ならない 。

→ここではなにを学習しているのだろう?

ラムダ計算のような純粋関数型言語に...のような制御演算子を追加するのは 、直観主義論理を古典論理に拡張するのに等しいことになる 。

→そもそも難しいことをしているのか。

C P S変換によりcall/ccと同じ効果がcall/ccを用いずとも達成できる

→ふーん。

C P S変換の論理的意味は必要な分だけ二重否定をつけることなのである 。

→二重否定だから結局同じこととみなして良いかどうか。

「十分に精度が高い出力を得るには 、十分に精度が高い入力を与えればよい 」という連続性の特質

圏論で出てくる連続がつながってる感が感じられなかったが、つながるイメージより、近似の精度の良さのイメージをもったほうが良さそう。その近似は今考えている文脈によると。

線形代数について簡単におさらいしておこう 。

→他にもおさらいが必要なものが沢山あるけど…。

線形論理は 、ノンポリだ 。世の中に古典主義者や直観主義者はいても 、 (提唱者ジラ ールを含めて )線形主義者というのは存在しないのである 。

→ ほう。

直観主義論理を分解してみたら 、なんか古典論理っぽいものが出てきた !

→ 理論を構築するのではなく分解してく方向性がなんとも。

とにかく "指数関数"やばい

→ 初めて聞いた。

ゲ ーデルの定理やチュ ーリングの定理によって徹底的にひねくれてしまった数学基礎論の研究者には 、なかなか容易なことではない 。

→ちょいちょい刺す。

たとえば 「数独 」 、 「お絵かきロジック 」 、 「テトリス 」 、 「ぷよぷよ 」などは全部ある意味で N P完全問題と見なすことができる

→人気あるゲームの必要条件はNP完全といえるか

2 0世紀後半のコンピュ ータ科学には先行する数学基礎論のアイデアが多数流入している 。

→プログラミングとはそれだけ難しいことが詰まっている。プログラミングは本来的に難しいということか。