Hatena::Groupxn--272ax3f

論理と計算のしくみ5.3(後半)

論理と計算のしくみ5.3(後半)

プレゼンテーション

目次

  • 明示的型付けと暗黙的型付け
  • 型推論
  • 自然演繹
  • カリーハワードの対応
  • 多相型

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

  • 明示的型付け
    • 変数の型が全て決まってる ( つまりλ項の型を決めれる )
    • f^{A->B}x^A
  • 暗黙的型付け
    • λ項の構文と型付けの機構を分離するような型付けスタイル
    • fx , fの型は A->B, x の型は A

型判断

  • 「自由変数 x_1,\dots,x_n の型が A_1 \dots A_n として与えられたとき λ項M の型は A」
    • という三項関係
    • x_1:A,\dots,x_n:A_n \vdash M:A と記す
  • 左辺を型割り当て, 右辺を型環境と呼ぶ
    • 以下\Gamma\Delta をその記号として用いる
  • n = 0 なら左辺は省略可

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

型判断はp225の規則により帰納的に定義される.
  • 型付け導出木:=型判断を導く証明
  • 型付け規則:= 上の規則

型推論

暗黙的型付けに基づく単純型付きλ計算について
  • 型検査
    • \Gamma \vdash M:A が成り立つかどうか判定すること
    • 型付け規則はλ項の構造に関する帰納法 => 決定可能
  • 型推論
    • 型検査+どのような型をもつのか調べること.
  • 変数\alpha
    •  (\alpha -> \alpha)\[\alpha:=(\beta -> \gamma)\] = (\beta -> \gamma) -> (\beta -> \gamma)

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

  • 入力 項M
  • 出力 型A と割り当てΓ, or 「型付け不能」
  • 制約抽出手続き\text{Extract}({x_1:\alpha_1,\dots,x_n:\alpha_n}, M, \alpha) を実行
    • x_1,\dots,x_n は M の自由変数 \alpha,\alpha_1,\dots,\alpha_n は異なる型変数
    • 等式の集合\epsilonを返す.
  • \epsilon を単一化 (ref.2.2(f))
    • 成功したら単一化\sigmaから 割り当て {x_1,\sigma(\alpha_1),\dots,x_n},\sigma(\alpha_n) と 型 \sigma(\alpha) を返す.
    • 失敗したら「型付け不能」

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

Extract

  • λ式Mの構造(大きさ)に関して帰納的に定義.
    • 停止する.
  • \text{Extract}({x_1,\alpha_1,\dots,x_n,\alpha_n}, x_i, A) = {A_i = A}
  • \text{Extract}(\Gamma,\lambda x . M, C) = Extract({x:\alpha} \union \Gamma, M, \beta) \union { C = \alpha -> \beta }
  • \text{Extract}(\Gamma, MN, B) = Extract(\Gamma, M, \gamma -> B) \union Extract(\Gamma, N, \gamma) #XXX Gamma は誤り?

補題5.19

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

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

定理5.20

  • Mの自由変数x_1,\dots,x_nとし, \alpha,\alpha_1,\dots,\alpha_n を型変数
  • 等式の集合  \text{Extract}({x_1:\alpha_1,\dots,x_n:\alpha_n}, M, A) の単一化\theta が存在するなら \theta(\Gamma) \vdash M:\theta(A)

主要型付け

  • 型推論アルゴリズムによる型判断は最も一般的である.
  • 型判断\Gamma \vdash M:A が主要型付け
    • \Gamma' \vdash M:A' を満たす任意の型割り当て\Gamma', 型A' に対して\Gamma の型変数への代入\sigmaが存在して\Gamma' = \sigma(\Gamma), A'=\sigma(A)

主要型定理(定理5.21)

  • Mの自由変数x_1,\dots,x_nとし, \alpha,\alpha_1,\dots,\alpha_n を型変数
  • 等式の集合 Extract({x_1:\alpha_1,\dots,x_n:\alpha_n}, M, \alpha)が単一化可能でその最汎単一化を\thetaとする
  • \theta({x_1:\alpha_1,\dots,x_n:\alpha_n}) \vdash M:\theta(\alpha) は主要型付け

自然演繹(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)
  • 正規化定理とサブジェクトリダクション定理より「型Aにより型付けされたλ項が存在するなら型Aにより型付けされた正規形のλ項Aが存在する」
  • 「すべての証明に対してそれと同じ結論を持つカットを用いない証明が存在する」というカット除去定理に対応

単純型付きλ計算の限界

(\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)

  • A::= \alpha \mid A \rightarrow B \mid \forall \alpha . A
    • 直積とか直和は作れるので無い.
  • M ::= | x^A | \lambda x^A . M | (MN) | A\alpha M | (MA)

多相型計算(2/2)

  • 型抽象と型適用の簡約とか増える.
  • サブジェクトリダクション定理/強正規化可能性定理が成り立つことが知られている!
  • 型なしλ計算と同じように, 自然数や原始機能的関数を表すことができる.
  • 多相型λ計算で表現できる関数は原始機能的関数全体より真に大きい
    • 型なしでも真に大きい...

依存型

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

依存関数型 (\Pi 型)

  • 例えば 依存型 \Pi n : \text{NAT}.A^n を持つ項M を関数として 型 Nat の項\bar{3}適用できて  M\bar{3} の型は  A^3 となる.
  • \Pi n : \text{NAT}.A関数Nat → A と同じ

依存直積型 (\Sigma 型)

  • 双対的なもの\Sigma n : \text{NAT}.A
    • 「ある nが存在していて A^n という型」 を表す.
  • \Sigma n : \text{NAT}.A は 直積型 \text{Nat} \times A と同じ

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

  • λ項Mを型変数\alpha によりλ抽象\Lambda\alpha は次に対応
  • 命題 \forall \alpha .A証明 \Lambda\alpha .M から任意の型 B に対して  A\[x:=B\] という命題の証明を得ることができる.
変数\alpha二階の変数(アリティ0)]
多相型\forall\alpha全称\forall X]

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

  • 依存型\Pi n : \text{NAT}.A は1階の変数x に対する全称  \forall x に対応する
  • おおまかに
  • 依存型を持つ多相λ計算直観主義2階述語論理に対応.