2002年度 講義

情報論理学(前期 火3)

プログラミング言語や仕様記述に関して重要である型理論について数学的に厳 密に説明する。(1) 型理論の基礎知識として、最も簡単な型理論である単純型 理論λ→をいろいろな角度から説明する。λ→の定義を与え、サブジェクトリ ダクション性、強正規化性、主型の存在について証明する。(2) プログラミン グ言語 ML の型理論について、型推論のアルゴリズムを説明し、その正しさを 証明する。(3) 型理論 F について、データ型の表現力を説明し、強正規化性 を証明する。(4) カリーハワードの同型対応が型理論と論理体系の自然な対応 を与えることをλ→と F を例として説明する。

情報基盤科学概論(速水, 龍田, 羽鳥, 山田, 前期 月2)

  1. 偏微分方程式を離散近似し、計算機でシミュレーションを行うための代表的な手 法として、有限差分法、有限要素法、境界要素法を数理的な面に着目して紹介する。
  2. プログラム意味論の基礎知識であるラムダ計算と一階述語論理を説明し、プログ ラムの性質を数学的に扱う方法とは何かを講義する。
  3. フーリエ変換、フーリエ級数の直交完備性、逆変換、複素表示の三角関数表示と 比べての優れた点等について考究する。
  4. ネットワークの基本的な構造や機能を紹介する。具体的にはネットワークの構成 要素、ネットワークの機能モデル、回線交換とパケット交換の相違、コネクション型 サービスとコネクションレス型サービスの相違などについて実例を交えて紹介する。

数学基礎論特論(東京大学情報理工学研究科コンピュータ科学専攻, 前期 木4)

型理論の初歩を概説する。 (1) 型理論の基礎となる最も簡単な型理論である単純型理論λ→をいろいろな 角度から説明する。 λ→の定義を与える。型理論に対して一般に定義できる性質として サブジェクトリダクション性、強正規化性、主型の存在について λ→を例に用いて説明する。 λ→に対するこれらの性質を証明する。 (2) プログラミング言語 ML の型理論について説明し、型推論のアルゴリズム を説明し、その正しさを証明する。 (3) 型理論 F を説明し、その強正規化性を証明する。 (4) 自然演繹命題論理 NJ と、自然演繹二階命題論理 NJ2 を説明する。 その証明の正規化を定義する。 カリーハワードの同型対応が型理論と論理体系の自然な対応を与えることを、 λ→とNJ, F とNJ2 を例として説明する。

2002年度 大学院セミナー

メンバー

中澤 小合 木村 安部

内容

構成的論理と型理論を中心とする理論計算機科学と数理論理学の研究討論
輪講

日時