理工学部Faculty of Science and Engineering
COT200XE（計算基盤 / Computing technologies 200）関数型プログラミングFunctional programming
藤田 憲悦Kenetsu FUJITA
授業コードなどClass code etc
| 学部・研究科Faculty/Graduate school | 理工学部Faculty of Science and Engineering |
| 添付ファイル名Attached documents | |
| 年度Year | 2024 |
| 授業コードClass code | H6160 |
| 旧授業コードPrevious Class code | |
| 旧科目名Previous Class title | |
| 開講時期Term | 秋学期授業/Fall |
| 曜日・時限Day/Period | 金3/Fri.3 |
| 科目種別Class Type | |
| キャンパスCampus | 小金井 |
| 教室名称Classroom name | 小西館‐W307 |
| 配当年次Grade | 2年 |
| 単位数Credit(s) | |
| 備考（履修条件等）Notes | |
| 他学部公開科目Open Program | |
| 他学部公開（履修条件等）Open Program (Notes) | |
| グローバル・オープン科目Global Open Program | |
| 成績優秀者の他学部科目履修制度対象Interdepartmental class taking system for Academic Achievers | |
| 成績優秀者の他学部科目履修（履修条件等）Interdepartmental class taking system for Academic Achievers (Notes) | |
| 実務経験のある教員による授業科目Class taught by instructors with practical experience | |
| SDGsCPSDGs CP | |
| アーバンデザインCPUrban Design CP | |
| ダイバーシティCPDiversity CP | |
| 未来教室CPLearning for the Future CP | |
| カーボンニュートラルCPCarbon Neutral CP | |
| 千代田コンソ単位互換提供（他大学向け）Chiyoda Campus Consortium | |
| カテゴリー＜理工学部＞Category |
応用情報工学科 学科専門科目 |
すべて開くShow all
すべて閉じるHide All
Outline (in English)
The aim of this course is to help students learn basic features of functional programming languages and acquire techniques in functional programming. Moreover, students learn the advantage of functional programming and become capable of utilizing it appropriately as well. The goals of this course are to learn (1) standard method of program description in functional programming languages, (2) the concept of recursive functions and induction, (3) higher order functions, polymorphic functions, inductive types, (4) the principle of type checking and type inference, and (5) lambda-calculus with beta-reduction and the Curry-Howard isomorphism. Students will be expected to have the relevant chapters from the text. Your study time will be more than four hours for a class. Grading will be decided based on reports (50%) and/or term-end examination (50%).
授業で使用する言語Default language used in class
日本語 / Japanese
授業の概要と目的（何を学ぶか）Outline and objectives
ソフトウエア開発において重要な位置にある関数型言語の基本的な機能を学び関数型プログラミングのテクニックと基礎理論を習得する。また関数型言語の特徴を理解し効果的な利用方法を学ぶ。関数型プログラミングの実践経験を通じて問題を論理的に捉え、設計の透過性を高めるスキルを涵養する。
到達目標Goal
つぎの項目の習得をゴールとする。
(1) 関数型言語における標準的なプログラム記述方法
(2) 再帰的関数と帰納法の利用方法
(3) 高階関数の記述と利用方法
(4) 多相型関数の記述と利用方法
(5) 再帰的データ構造とストリーム（無限リスト）の記述と利用方法
(6) 型検査と型推論の方法
(7) ラムダ記法・ベータ変換と活用とカリー・ハワード同型
この授業を履修することで学部等のディプロマポリシーに示されたどの能力を習得することができるか（該当授業科目と学位授与方針に明示された学習成果との関連）Which item of the diploma policy will be obtained by taking this class?
ディプロマポリシーのうち、「DP1」と「DP2」と「DP4」に関連
授業で使用する言語Default language used in class
日本語 / Japanese
授業の進め方と方法Method(s)（学期の途中で変更になる場合には、別途提示します。 /If the Method(s) is changed, we will announce the details of any changes. ）
OCaml（Objective Caml）を初歩から学ぶことで関数型言語によるプログラミングの実際とカリー・ハワード同型（論理と型付き言語との関係）を学ぶ。OCamlは強く型付けされた言語であり、静的型システムにより実行時における型に関する安全性が保証されている。プログラミングの演習を通じてOCamlのみにとどまらず関数型言語一般に通用する技法と基礎理論を習得する。 対面での開講に変更される可能性がある。この場合の授業方法・授業計画、成績評価方法の変更などについては、課題等の提出・フィードバック等の仕方も含め学習支援システムまたは授業中に別途指示する。授業中に小問を質問することがあるので授業終了までに必ず解答のこと。
アクティブラーニング（グループディスカッション、ディベート等）の実施Active learning in class (Group discussion, Debate.etc.)
なし / No
フィールドワーク（学外での実習等）の実施Fieldwork in class
なし / No
授業計画Schedule
授業形態/methods of teaching：対面/face to face
※各回の授業形態は予定です。教員の指示に従ってください。
第1回[オンライン/online]：プログラミング言語いろいろ
プログラミング言語の役割・種類・家系図、OCamlの処理系
第2回[オンライン/online]：関数型言語の概要と基本文法
関数型言語の特徴と利点、
関数型 vs. 手続き型、
数列・漸化式（数学B）の流儀でプログラムを書く、基本データ型、束縛変数とlet式、関数型
第3回[オンライン/online]：再帰的関数とパターンマッチ
再帰的関数定義、末尾再帰と繰り返し、相互再帰、match式とパターンマッチを用いた関数定義、要素の抽出
第4回[オンライン/online]：高階関数
高階関数の定義、ラムダ式、β変換、curry、uncurry、twice、three
第5回[オンライン/online]：多相型関数と型推論
多相型関数の記述と利用方法、id、fst、snd、apply、型検査・型推論の原理と方法
第6回[オンライン/online]：再帰的データ構造
再帰的データ構造の記述と利用方法、nat、list、tree、prop、map、filter、fold
第7回[オンライン/online]：高度な話題
ストリームと無限リスト、素数列の生成、collatzの問題、フィボナッチ数列の生成
第8回[オンライン/online]：命題論理の意味論と証明論
恒真性、推論規則、証明図、コルモゴロフの埋込み、黒田の埋込み
第9回[オンライン/online]：自然演繹の形式的体系NKの健全性と完全性
ワンのアルゴリズムとトートロジー・チェッカー
第10回[オンライン/online]：ラムダ計算
ラムダ記法とβ変換、チャーチ・ロッサーの定理
第11回[オンライン/online]：型付きラムダ計算
直観主義論理の証明図の記号化と簡約
第12回[オンライン/online]：型付きラムダ・ミュー計算
古典論理の証明図の記号化と簡約
第13回[オンライン/online]：カリー・ハワード同型対応
論理式＝型、証明＝プログラム、トートロジーとinhabitation
第14回[オンライン/online]：総まとめと課題
プログラム生成・検証への応用
授業時間外の学習（準備学習・復習・宿題等）Work to be done outside of class (preparation, etc.)
【本授業の準備・復習等の授業時間外学習は、4時間を標準とする】
処理系をインストールして、スライドの課題とプログラミングに取り組む、教科書の例題などを予習復習に活用する。
テキスト（教科書）Textbooks
「数理パズルで楽しく学べる論理学」（藤田）コロナ社(2022)２章（命題論理の意味論と形式的体系）、及び４章（ラムダ計算、ラムダ・ミュー計算とカリー・ハワード同型）。https://www.coronasha.co.jp/np/isbn/9784339029239/
参考書References
「プログラミングの基礎」(浅井)サイエンス社(2007)
「すごいHaskellたのしく学ぼう!」(田中・村主訳) オーム社(2012)
「プログラミング言語の基礎概念」(五十嵐)サイエンス社(2011)
成績評価の方法と基準Grading criteria
【評価方法】
レポート(50%)と定期試験(50%)による。
【評価基準】
本科目において設定した達成目標を60%以上達成している学生を合格とする。対面での開講となった場合や全てオンラインとなった場合、成績評価の方法と基準も（レポート100%等に）変更する場合がある。その場合の具体的な方法と基準は、授業中などに提示する。
学生の意見等からの気づきChanges following student comments
特になし
学生が準備すべき機器他Equipment student needs to prepare
授業にはノートPCを持参し、OCamlをインストールすること。理論（ラムダ計算、証明論と意味論、カリー・ハワード同型）の説明には教科書を使う。
その他の重要事項Others
学習支援システムからの連絡がないかどうかの確認を怠らないこと。