発表言語 |
日本語
|
開催日 |
2011年02月01日 15時00分
|
終了日 |
2011年02月01日 16時00分
|
開催場所 | 京都大学数理解析研究所402号室 |
セミナー名 | 第36回 GCOE tea time |
タイトル |
GoI (Geometry of Interaction)とラムダ計算の意味論 |
分野 |
幾何 解析 その他
|
講演者名 | 星野 直彦 |
講演者所属 | 京大数理研 |
概要 | ラムダ計算は関数型プログラミング言語の核となる部分を形式的な形で記述したものです。
このラムダ計算に関する性質を示す方法の一つが圏論的意味論(モデル)で、
例えば、集合と関数の圏(Set)では型は集合、ラムダ項は関数として解釈されます。
Girardによって導入されたGoI(Geometry of Interaction)は(線型)ラムダ計算の意味論ですが
他のラムダ計算の圏論的意味論と異なり、ラムダ項の解釈に高階のデータ構造が現れないという
特徴を持っています。この性質はGoI解釈がInt構成によって得られるcompact closed categoryを用いて
与えられている事に由来しているという事ができ、またこの性質に着目するとGoI解釈から(線型)
ラムダ計算のある意味での実装を得る事ができます。
今回はラムダ計算のGoI解釈を構成する方法を圏論的な視点から解説したいと思います。
キーワード:Int構成、compact closed category |
備考 | 他分野の話を聞いたり、若手研究者と交流する良い機会ですので ぜひ参加してください。飲み物、おやつも用意する予定ですので、お気軽にお越しください。 |