プレゼンテーション

目次

明示的型付けと暗黙的型付け

型判断

型付け規則と型付け導出木

型判断はp225の規則により帰納的に定義される.

型推論

暗黙的型付けに基づく単純型付きλ計算について

型推論のアルゴリズム(1/2)

型推論のアルゴリズム(2/2)

Extract

補題5.19

型割り当て\Gamma, λ項M, 型A, 型代入θに対して 「型等式の有限集合\epsilon = \text{Extract}(\Gamma, M, A), \theta\epsilon の単一化」<=> 「\theta(\Gamma) \vdash M:\theta(A)

型推論のアルゴリズムの健全性

定理5.20

主要型付け

主要型定理(定理5.21)

自然演繹(1/)

自然演繹(2/)

  1. A を仮定する
  2. B を仮定する
  3. (1),(2) より A かつ B

カリーハワードの対応(1/2)

型付きλ計算 直観主義論理
論理式
関数型A→B 含意A ⊃ B
直積型A×B 連言A∧B
直和型A+B 選言A∨B
λ項自然演繹証明

カリーハワードの対応(2/2)

関数適用 は 推論規則⊃E など置き換えれるだけでなくその上に展開される構造も対応している. λ項の正規形 は 自然演繹では カットを用いない証明に対応(章末問題5.15)

多相型

単純型付きλ計算の限界

(\lambda x . x)(\lambda x . x) は型付けできるが (\alpha \rightarrow \alpha)(\alpha \rightarrow \alpha) \rightarrow (\alpha \rightarrow \alpha) (\lambda f . ff)(\lambda x . x) はβ簡約で上の式になるが型付けできない.

多相型

(\alpha \rightarrow \alpha)(\alpha \rightarrow \alpha) \rightarrow (\alpha \rightarrow \alpha) みたいなのを全部ひっくるめたもの \forall \alpha . \alpha -> \alpha

多相型計算(1/2)

多相型計算(2/2)

依存型

Aのn個の直積を表す型  A^n など項をパラメタとする型.

依存関数型 (\Pi 型)

依存直積型 (\Sigma 型)

多相型におけるカリーハワードの対応

変数\alpha二階の変数(アリティ0)]
多相型\forall\alpha全称\forall X]

依存型におけるカリーハワードの対応