授業の目的 【日本語】 | | テーマ:プログラムの意味論・型と論理
プログラミング言語は貪欲に機能を増やしていくが、ラムダ計算がそれらの機能を統一的に扱えるため、中心的な役割を得た。しかし、ラムダ計算の等式理論が比較的容易に定義できるものの、より抽象的な表示的意味論の構築が集合論の枠組みに中々収まらない。
この少人数クラスでは型なしラムダ計算および様々な型付ラムダ計算のモデルを作る方法を見ていく。圏論と領域論が具体的な枠組みを与え、そのモデルが新しいプログラムの構成法につながる。Haskellでよく使われるモナドなどがそのモデル化から生まれたものである。
具体的には、AmadioとCurienの「Domains and lambda calculi」を読んでそれを勉強する予定である。また、必要に応じて他の文献も見ていく。
Theme: Programming language semantics, types and logic
Programming languages have many functionalities. The lambda-calculus acquired its central role due to its ability of handling them in a uniform way. Yet, while the equational theory of lambda-calculus is relatively easy to define, the construction of a more abstract denotational semantics does not fit easily into the framework of set
theory.
In this small class we will study the construction of models for the untyped and typed lambda-calculus. Category theory and domain theory provide a concrete way to build models, and offer insights into programming languages. The use of monads in the language Haskell is an example of a programming construct derived from categorical models. |
|
|
授業の目的 【英語】 | | |
|
到達目標 【日本語】 | | * ラムダ計算と型理論の基礎を習う.
* モデル構築に必要な圏論の概念を習う.
* ラムダ計算に対する具体的なモデルの構築法を習う. |
|
|
到達目標 【英語】 | | |
|
授業の内容や構成 | | 基本的には本や論文の輪講という形を取る.ほとんどの資料が英語になるので,発表する人がちゃんと下調べをして,少くとも言葉が皆に理解できるように説明していただく.後期になると,個人の希望に応じて,一人で論文を読んで,報告するという形でもよい.
この少人数クラスのカリキュラムは1年間で完結するが,次の年の少人数クラスは計算と論理への少し異ったアプローチにしようと考えているので,同じ分野で続けることができる.
This course is mainly a reading seminar. The participants are expected to prepare carefuly the parts they are assigned, in order to give explanatory presentations. During the second semester, participants may also read individually chosen articles and report on them.
This course has contents for one year, but it is expected that another small class tackling logic and computation from a different point of view will be held during the next year, so that participants may complete their knowledge of this subject. |
|
|
履修条件 | | 特に何も求めていない.論理学やプログラミングの知識が少しあると楽になる.
This course basically uses Japanese as communication language.
Contact the teacher if you would like to participate in English. |
|
|
関連する科目 | | 計算機数学II 2020年後期 J. Garrigue |
|
|
成績評価の方法と基準 | | |
|
教科書・テキスト | | [1] R. Amadio and P.L. Curien. Domains and lambda calculi. Cambridge Tracts in Theoretical Computer Science 46, ISBN 0 521 62277 8, 1998.
[2] J.Y. Girard, P. Taylor, Y. Lafont. Proofs and Types. Cambridge Tracts in Theoretical Computer Science 7, ISBN 0 521 37181 3, 1989.
|
|
|
参考書 | | [3] 横内寛文, プログラム意味論, 共立出版, 1994.
[4] 大堀 淳, プログラミング言語の基礎理論, 共立出版, 1997. |
|
|
課外学習等(授業時間外学習の指示) | | |
|
注意事項 | | |
|
他学科聴講の可否 | | |
|
他学科聴講の条件 | | |
|
レベル | | |
|
キーワード | | プログラミング言語
表示的意味論
圏論
ラムダ計算
型理論
論理 |
|
|
履修の際のアドバイス | | 輪講形式では発表の準備が肝心である.
また,他人の発表のときにも積極的に講義に参加する必要がある. |
|
|
授業開講形態等 | | |
|
遠隔授業(オンデマンド型)で行う場合の追加措置 | | |
|