学部後期課程
過去（2020年度）の授業の情報です
学内のオンライン授業の情報漏洩防止のため，URLやアカウント、教室の記載は削除しております。
最終更新日：2024年4月22日
授業計画や教室は変更となる可能性があるため、必ずUTASで最新の情報を確認して下さい。
UTASにアクセスできない方は、担当教員または部局教務へお問い合わせ下さい。
最終更新日：2024年4月22日
授業計画や教室は変更となる可能性があるため、必ずUTASで最新の情報を確認して下さい。
UTASにアクセスできない方は、担当教員または部局教務へお問い合わせ下さい。
計算数学I
プログラミング言語の数学的基礎
言語を通して人間はお互いを理解しあう。プログラミング言語も例外ではなく，それを通してはじめて人間と計算機が交流できるようになる。だが，表面的な文法の学習にとどまらず，言語の本質的な構造を知ることは意思疎通への近道である。プログラミング言語の構造を知ることで計算機が考えていることが真に理解できるようになる。
プログラミング言語の設計・実装を支える数学的基礎を学習する。そのためには「計算」とは何かを数学的に定式化しないといけない。その一つのモデルがラムダ計算である。本講義の前半ではラムダ計算を導入し，計算体系としての数学的な性質を調べる。
後半では型の概念について論じる。多くのプログラミング言語には型が入っている。いったい何のために入っているのだろうか。その意義を数学的な観点から，および実装にからめて論じる。
プログラミング言語の設計・実装を支える数学的基礎を学習する。そのためには「計算」とは何かを数学的に定式化しないといけない。その一つのモデルがラムダ計算である。本講義の前半ではラムダ計算を導入し，計算体系としての数学的な性質を調べる。
後半では型の概念について論じる。多くのプログラミング言語には型が入っている。いったい何のために入っているのだろうか。その意義を数学的な観点から，および実装にからめて論じる。
時間割／共通科目コード
コース名
教員
学期
時限
0505062
FSC-MA3351L1
計算数学I
長谷川 立
木曜4限
マイリストに追加
マイリストから削除
講義使用言語
日本語
単位
2
実務経験のある教員による授業科目
NO
他学部履修
可
開講所属
理学部
授業計画
ラムダ計算を導入する。計算体系としてのラムダ計算の文法構造を理解し，アルファ変換・ベータ簡約により計算できるようになることが要件である。チャーチ・ロッサー性について述べる。ラムダ計算が計算体系としてよいものであることの証左である。またチューリング完全性の概念を導入し，ラムダ計算がチューリング完全であることの概略を示す。ラムダ計算が柔軟な表現力をもっていることの証である。
授業の後半では型つきラムダ計算を扱う。型判定とその導出が基本概念である。可簡約法に基づき強正規化性を示す。型を入れたことにより，さらに計算体系としてすぐれたものとなったことを意味する。また，操作的意味論を導入し実装の数学的モデル化を行う。その型安全性について述べる。実行時エラーを起こさないことを型によって保証できる。
授業の方法
講義による
成績評価方法
レポートによる。
レポート課題はITC-LMSに掲示する。締切は7月22日。
教科書
使用しない。
参考書
ラムダ計算については書籍がいろいろある。たとえば，高橋正子「計算論：計算可能性とラムダ計算」，J.R.Hindley and J.P.Selding "Lambda Calculus and Combinators"など。操作的意味論については大堀淳「プログラミング言語の基礎理論」が詳しい。
履修上の注意
予備知識は仮定しない。
