- 授業のテーマと目的:
- 数学が発展してきた過程では、自然科学、社会科学などの種々の学問分野で提起される問題を解決するために、既存の数学の枠組みにとらわれない、新しい数理科学的な方法や理論が導入されてきた。また、逆に、そのような新しい流れが、数学の核心的な理論へと発展した例も数知れず存在する。このような数学と数理解析の展開の諸相について、第一線の研究者が、自身の研究を踏まえた入門的・解説的な講義を行う。
数学・数理解析の研究の面白さ・深さを、感性豊かな学生諸君に味わってもらうことを意図して講義し、原則として予備知識は仮定しない。
|
第11回 |
日時: |
2008年7月4日(金) 16:30−18:00 |
場所: |
数理解析研究所 420号室
|
講師: |
長谷川 真人 教授 |
題目: |
論理と計算の対応について
|
要約:
|
数理論理学と計算機科学は1930年代以来密接に関連しつつ発展してきました。この講義では、その核心となる話題のひとつ、Curry-Howard対応についてお話しします。Curry-Howard対応の基本的なアイデアは、おおざっぱには、下の表の左側と右側を対応づけるものです。
数理論理学 |
|
計算機科学 |
(証明論、自然演繹) |
|
(プログラミング言語、ラムダ計算) |
論理式 |
⇔ |
データ型 |
証明 |
⇔ |
プログラム |
証明の標準化 |
⇔ |
プログラムの実行 | Curry-Howard対応により、数理論理学と計算機科学の間に、さまざまな相乗効果が生まれました。たとえば、形式的な論理体系が無矛盾であることは、適当なプログラミング言語(ラムダ計算)においてプログラムの実行が必ず停止することに本質的に関連しています。また、数理論理学における高階論理や線形論理、また古典論理に関する研究は、多相型プログラミング言語、線形データ型、さらにジャンプのような非局所的制御構造など、プログラミング言語に関する多くの重要な話題と相互に影響しあいながら進展してきました。講義では、証明論と型付きラムダ計算の初歩からはじめて、Curry-Howard対応の基本事項について紹介し、時間が許せば比較的最近の進んだ話題にも触れたいと思います。
|
"http://www.kurims.kyoto-u.ac.jp/ja/special-02.html"
|