ぱらぱらめくる『コンピュータは数学者になれるのか？』

コンピュータは数学者になれるのか? -数学基礎論から証明とプログラムの理論へ-

• 目次
  • 1 数学者を作ろう
  • 2 対角線上に追い詰めろ
  • 3 計算よ停まれ！
  • 4 NPの壁
  • 5 活き活きした証明
  • 6 対角線に向かう未来
• 強調されている用語を列挙し、どういう本なのかの概要を掴む
  • 論理と計算
  • 証明とプログラム
  • P対NP問題
  • 不完全性
  • 無矛盾
  • 形式系
  • カリー・ハワード
• 1 数学者を作ろう
  • 数学者は証明する
  • 証明は言語により記述される
  • 推論規則ならなる。公理も推論規則の一部
  • 自然数が出発点
  • 真偽
  • 真は見つかる、偽は確定しないことがある
  • 数学者とは形式系
  • 形式系を構成する要素としての、帰納法・再帰関数、ペアノ算術
  • 集合の力。集合の集合という階層化
  • 矛盾への対応としての型理論
  • メタ数学と形式系
• 2 対角線論法
  • 対角線論法、可算と連続体
  • 計算課題〜自然数表現
  • 「無矛盾仮定の下で、○○である」を証明する
• 3 計算の停止
  • 整列集合
  • 数学の無矛盾性と計算の停止性の関係
  • 証明とは代数的：論理を形式化することで、証明が抽象代数になった・・・？
• 4 NP
• 5 活き活きとした証明
  • カリー・ハワード対応：「証明はプログラムである」
  • ラムダ関数：「人間が紙と鉛筆を使って計算する物理的プロセスを抽象化→チューリング機械」。「(数学者が)関数を作ったり使ったりする数学的プロセスを抽象化→ラムダ計算」
  • 関数型プログラミング言語で言うところの、簡約、正規化、関数合成
  • 証明図をラムダ項で表せば、「証明はプログラムである」となる
  • 証明図の対応としてのプログラムは「１００％正しい」：構成的プログラミング