国立大学法人東北大学電気通信研究所公式ウェブサイト|Research Institute of Electrical Communication Tohoku University

コンピュータサイエンス研究会

研究会名:コンピュータサイエンス研究会
開催日:平成20年12月18日(木)15:00~17:00
テーマ:計算論的ルディクス
講師:照井 一成(京都大学数理解析研究所)
開催場所:東北大学電気情報系3号館201号室


コンピュータサイエンス研究会 講演会の御案内

コンピュータサイエンス研究会
主査  小林 直樹

下記のようにコンピュータサイエンス研究会の講演会を開催いたしますので, ご案内申し上げます.

  • 日時:2008年12月18日(木)15:00~17:00
  • 場所:東北大学 電気情報系3号館 201号室
  • 題目:計算論的ルディクス
  • 話者:照井 一成(京都大学数理解析研究所)
  • 概要:ルディクスとは、1990年代後半にJ.-Y. Girardにより提案された野心的な研究プログラムである。それは論理から証明を導き出すのではなく、証明から論理を導き出し、それにより様々な論理・計算現象を解明しようという構想である。 もう少し詳しくいえば、証明の正規化、チャーチ・ロッサー、ベームの分離定理などの周知の道具立てをふんだんに駆使し、“証明”に相当する下部構造(おおざっぱに言って線形π計算の部分体系)から“論理”に相当する上部構造(おおざっぱに言って極性つき線形論理)を導き出そうというのである。ゲーム意味論、Krivine流実現可能性理論などとも密接に関連している。
    ルディクスには、“受肉の神秘”、“内在的完全性”など斬新なアイデアが豊富に含まれるが、フレームワークの未整備から(Curien, Faggian一派などを除いて)あまり研究が進められていないのが現状である。特に妨げとなっているのは、示唆的ながらも煩雑なシンタックス、伝統的な計算論とのギャップにあるように思われる。それゆえ本発表では、π計算風の簡潔なシンタックスを導入した上で、伝統的なラムダ計算との橋渡しを行い、その上でルディクスの基本的アイデアを計算論的な観点から解説し、最後に将来の展望について論じる予定である。

問い合わせ先

小林  直樹

内線:7177