10月24日(木)と10月25日(金)に神奈川大学の松田直祐助教に数学基礎論(証明論・計算論)の入門的な講演を行ってもらいます．
学部生の方も奮ってご参加ください．なお，24日と25日で教室が異なりますのでご注意ください．
10月24日(木) 14:30~17:30 総合研究棟2階講義室
題目： 証明論・計算論入門
内容：
以下の3部に分けて，証明論・計算論の導入をする．
- 証明論入門
- 計算論入門
- 証明と計算の関係
証明論とは，数学の証明などの論証を形式化し，その形式体系を研究する学問である．
本講演では，構成的な数学の証明の中で用いられる直観主義論理と呼ばれる論理について説明し，その論理の形式化について解説する．
計算論とは，「計算とは何か」という問いに対する研究である．
「計算」という概念に対する数理モデルは様々なものが提唱されているが，本講演では現在関数型プログラミング言語の基礎となっているラムダ計算という計算モデルを紹介する．
証明と計算の間には，Curry-Howard対応と呼ばれる関係が知られており，現在ではこの関係を利用してプログラミング言語を利用して数学の証明の支援などが行われている．
本講演では，Curry-Howard対応について簡単な紹介を行う．
10月25日(金) 16:10~17:40 7号館2階209室
題目：束縛変数回避入門
内容：
ラムダ計算の計算を実装する際に考慮するべき問題の一つに，束縛変数をどのように扱うべきかという問題がある．
本講演では，束縛変数の問題を回避するためのいくつかのアイディアを紹介する．
特に，コンビネータという定数を用いる手法を中心に解説する．