理工学研究科Graduate School of Science and Engineering
PRI500X4（情報学基礎 / Principles of informatics 500）応用論理・数理言語学特論１Applied Logic and Mathematical Linguistics １
金沢 誠Makoto KANAZAWA
授業コードなどClass code etc
| 学部・研究科Faculty/Graduate school | 理工学研究科Graduate School of Science and Engineering |
| 添付ファイル名Attached documents | |
| 年度Year | 2022 |
| 授業コードClass code | YC007 |
| 旧授業コードPrevious Class code | |
| 旧科目名Previous Class title | |
| 開講時期Term | 秋学期授業/Fall |
| 曜日・時限Day/Period | 木3/Thu.3 |
| 科目種別Class Type | |
| キャンパスCampus | 小金井 |
| 教室名称Classroom name | 各学部・研究科等の時間割等で確認 |
| 配当年次Grade | |
| 単位数Credit(s) | 2 |
| 備考（履修条件等）Notes | |
| 実務経験のある教員による授業科目Class taught by instructors with practical experience | |
| カテゴリーCategory | システム理工学専攻 |
すべて開くShow all
すべて閉じるHide All
Outline (in English)
The course covers the basics of lambda calculus.
The goals of the course are to understand the notion of reduction of lambda-terms; how various types of data may be encoded by lambda-terms; and how all recursive functions can be represented by lambda-terms.
The time required for study outside of the classes will be at least four hours per week.
The course grade will be based on assignments (40%) and the final take-home exam (60%).
授業で使用する言語Default language used in class
日本語 / Japanese
授業の概要と目的（何を学ぶか）Outline and objectives
関数型プログラミングの基礎となっているラムダ計算について基本的事項を学ぶ。
到達目標Goal
・λ項の簡約について理解する
・λ項によるいろいろなデータの表現を理解する
・λ項による再帰的関数の表現について理解する
この授業を履修することで学部等のディプロマポリシーに示されたどの能力を習得することができるか（該当授業科目と学位授与方針に明示された学習成果との関連）Which item of the diploma policy will be obtained by taking this class?
ディプロマポリシーのうち、「DP1」「DP2」「DP3」に関連
授業で使用する言語Default language used in class
日本語 / Japanese
授業の進め方と方法Method(s)（学期の途中で変更になる場合には、別途提示します。 /If the Method(s) is changed, we will announce the details of any changes. ）
板書を使った講義形式。定期的に演習問題を課す。
アクティブラーニング（グループディスカッション、ディベート等）の実施Active learning in class (Group discussion, Debate.etc.)
なし / No
フィールドワーク（学外での実習等）の実施Fieldwork in class
なし / No
授業計画Schedule
授業形態/methods of teaching：対面/face to face
※各回の授業形態は予定です。教員の指示に従ってください。
1[対面/face to face]：λ項
λ項，束縛変数・自由変数，代入，α変換・β変換・η変換
2[対面/face to face]：等号と正規化（1）
簡約，正規形，等号，Church-Rosserの定理
3[対面/face to face]：簡約と正規化（2）
ダイヤモンド特性，非停止性，最左簡約，遅延評価
4[対面/face to face]：Church-Rosserの定理
Church-Rosserの定理の証明
5[対面/face to face]：λ計算によるデータの表現（1）
ブール値，順序対，自然数，自然数に対する演算のλ項による表現
6[対面/face to face]：λ計算によるデータの表現（2）
リスト，木のλ項による表現
7[対面/face to face]：再帰的に定義された関数（1）
アッカーマン関数，不動点コンビネーターの応用
8[対面/face to face]：再帰的に定義された関数（2）
不動点コンビネーターの定義，頭部正規形
9[対面/face to face]：λ計算と計算可能性（1）
原始再帰的関数の表現，一般再帰的関数の表現
10[対面/face to face]：λ計算と計算可能性（2）
λ定義可能な関数の計算可能性，第二不動点定理，決定不能問題
11[対面/face to face]：プログラミング言語としてのλ計算
ISWIM，値呼び，対・パターンマッチング・相互再帰，SECD機械への翻訳
12[対面/face to face]：コンビネーター
グラフ簡約，コンビネーター，コンビネータにおける抽象の表現
13[対面/face to face]：λ項とコンビネーター
λ項とコンビネーターの対応
14[対面/face to face]：コンビネーターを用いたコンパイル手法
グラフとしてのコンビネーター，グラフ変換
授業時間外の学習（準備学習・復習・宿題等）Work to be done outside of class (preparation, etc.)
【本授業の準備・復習時間は、各４時間を標準とします。】
テキスト（教科書）Textbooks
指定しないが，主に下の1つ目の参考書に沿った形で授業を進める。
参考書References
Lawrence C. Paulson, Foundations of Functional Programming, 2021. https://www.cl.cam.ac.uk/~lp15/papers/Notes/Founds-FP.pdf
Michael J. C. Gordon. Programming Language Theory and Its Implementation. Prentice-Hall, 1988.
Peter Selinger, Lecture notes on the lambda calculus, 2013. https://arxiv.org/abs/0804.3434
成績評価の方法と基準Grading criteria
定期的に課す演習問題（40％）と期末のレポート（60％）の成績で評価する。
学生の意見等からの気づきChanges following student comments
特になし。