ATTAPL輪講 (第４回) 続 Dependent Types

Presentation on theme: "ATTAPL輪講 (第４回) 続 Dependent Types"— Presentation transcript:

1 ATTAPL輪講 (第４回) 続 Dependent Types
2006/06/21 稲葉 一浩

2 今日の内容 Dependent Types と多相型 Dependent Types を使ったプログラミング
Calculus of Construction (2.6) λ-cube (2.7) Dependent Types を使ったプログラミング DML (2.8)

3 Calculus of Construction (CC)
λLF の拡張 t ::= x | λx:T.t | t t | all x:T.t T ::= X | Πx:T.T | T t | Prop | Prf K ::= * | Πx:T.K Γ├ Prop :: * Γ├ Prf :: Πx:Prop.* Γ├ T :: * Γ,x:T ├ t : Prop Γ├ all x:T.t : Prop Γ├ T :: * Γ,x:T ├ t : Prop________ Γ├ Prf(all x:T.t) ≡ Πx:T.(Prf t) :: *

4 Calculus of Construction (CC)
おおまかな気持ち 型 Prop を持つ term とは 命題 データ型 型 Prf p を持つ term とは 命題 p の証明 データ型 p のメンバ

5 例 自然数のエンコーディング 自然数というデータ型を項 nat として表現 zero = λz.λs.z : ∀X. (X→(X→X)→X)
one = λz.λs. s z : ∀X. (X→(X→X)→X) succ = λm.λz.λs. s (m s z) : 略 自然数というデータ型を項 nat として表現 nat : Prop all a:Prop. all z:Prf a. all s:Prf a→Prf a. a Prf nat ≡ Πa:Prop. Πz:Prf a Πs:Prf a→Prf a. Prf a

6 例 Prf nat 型をもつ項 zero : Prf nat succ : Prf nat → Prf nat
λa:Prop. λz:Prf a. λs:Prf a→Prf a. z succ : Prf nat → Prf nat λn:Prf nat. λa:Prop. λz:Prf a. λs:Prf a→Prf a s (n a z s)

7 CCのできること さまざまなAbstraction λx:T. t 項に依存する項 λ→ Πx:T. T 項に依存する型 λLF
ふつうのλ抽象 Πx:T. T 項に依存する型 λLF Dependent Types ΛX::*.t 型に依存する項 F ∀X::*.T 型に依存する型 F 多相型 id = ΛX::*.λx:X. x : ∀X.X→X ΛX::K. t 高階の型に依存する項 Fω ∀X::K. T 高階の型に依存する型 Fω 高階の多相型 λx:Prop. t all x:Prop. T λx:Prop→Prop. t 等 all x:Prop→Prop. T 等

8 論理結合子と推論規則の表現 and = λp:Prop. λq:Prop. all a:Prop. all pair:Prf p→Prf q→Prf a. a left : Prf(and p q) → Prf(p) λx:Prf(and p q). (x p) (λa.λb.a) right: Prf(and p q) → Prf(q) λx:Prf(and p q). (x q) (λa.λb.b)

9 論理結合子と推論規則の表現 eq = λa:Prop. λx:Prf a. λy:Prf a all p:Prf a→Prop. all h:Prf (p x). p y eqRefl : Πa:Prop. Πx:Prf a. Prf (eq a x x) λa:Prop. λx:Prf a. λp:Prf a→Prop. λh:Prf(p x). h eqSym : Πa:Prop. Πx:Prf a. Πy:Prf a Prf (eq a x y) → Prf (eq a y x) eqRefl : 略

10 いろいろ Algorithmic Typing Strong Normalization of Well-Typed Terms
67ページ Strong Normalization of Well-Typed Terms Fω に帰着して証明するなど CC + Sigma Types T ::= ... | Σx:S.T × 「ex y:T.t : Prop」 「Prf(ex y:T.t) ≡ Σy:T.Prf t」 ○ 「σy:Prf s.t : Prop」 「Prf(σy:Prf s.t)≡Σy:Prf s.Prf t」

11 Calculus of Inductive Construction
さっきのやり方では、「数学的帰納法」が「証明」できない 以下の型をもつterm natIndが構成できない natInd : Πp:Prf nat→Prop Prf (p zero) →Πx:Prf nat. (Prf (p x) → Prf (p succ(x)) →Πx:Prf nat. Prf (p x)

12 CIC プリミティブとして、帰納法を表すtermを追加 nat:Prop 自動的に宣言 zero : Prf nat
succ : Prf nat → Prf nat natInd : Πp:Prf nat→Prop Prf (p zero) →Πx:Prf nat. (Prf (p x) → Prf (p succ(x)) →Πx:Prf nat. Prf (p x) natInd p hz hs zero ≡ hz natInd p hz hs (succ n) ≡ hs n (nadInt p hz hs n) 自動的に宣言

13 CIC 任意の帰納的なPropに対しても同様
list : Prop nil: Prf list cons: Prf nat → Prf list → Prf list listInd : Πp:Prf list→Prop Prf (p nil) → Πx:Prf nat. Πy:Prf list (Prf (p y) → Prf (p (cons x y)) →Πx:Prf list. Prf (p x) listInd p hn hc nil ≡ hn listInd p hn hc (cons x y) ≡hc x (listInd p hn hc y) 自動的に宣言

14 注： 帰納法と再帰関数 Strong Normalization を保証する言語では、任意の再帰関数は定義できない（停止しない可能性があるため） CICでは、Induction termを使ってある程度の再帰関数は記述できる

15 Coq (Barras et al., 1997) CICに基づく T ::= .. | Prop | Set
CC の Prop を「Prop」と「Set」に分割 命題として使うところではProp データ型として使うところではSet を使う あとでProp部分を除いてSet部分だけ残したプログラムを抽出すると、普通の関数型言語のプログラムが抽出できる

16 λ-cube さまざまなAbstraction Fω CC F ・ ・ λ→ λP

17 Pure Type Systems t ::= s | x| λx:t.t | t t | Πx:t.t s ::= * | □
Γ├ S : * Γ,x:S├ t:T Γ├λx:S.t : Πx:S.T Γ├t1 :Πx:S.T Γ├t2:S Γ├t1 t2 : [x→t2]T Γ├t:T T≡S Γ├S:s Γ├ t: S Γ├ S : si Γ,x:S ├ T : sj Γ├Πx:S.T : sj where (si, sj) ∈ {(*,*)} λ← {(*,*) (*,□)} λP {(*,*) (□, *)} F {(*,*) (□, *), (□,□)} Fω {(*,*) (*,□) (□, *), (□,□)} CC

18 今日の内容 Dependent Types と多相型 Dependent Types を使ったプログラミング
Calculus of Construction (2.6) λ-cube (2.7) Dependent Types を使ったプログラミング DML (2.8)

19 Dependent Typesを導入した言語
古くは Pebble (Lampson and Burstall, 1988) Quest(Cardelli and Longo, 1991) 最近では Cayenne (Augustsson, 1998) Haskell ベース Dependent ML (Xi and Pfenning, 1998) SML ベース Caml ベースの実装 (de Caml) もあり

20 問題点と解決策 Dependent Types の型チェックはtermのequality検査が必要
一般の言語では、termのreductionは止まらないことがある 停止性は決定不能 Cayenne 任意のtermへの依存を許す 十分長い時間走らせて計算が止まらなければ型エラー Dependent ML 依存できるtermを制限して、 効率的にequalityを決定可能な範囲に限る

21 Dependent ML (Simplified)
依存できるtermを、 整数の線形な部分集合に限る I ::= int | {x:I | P} P ::= P ∧ P | i≦i i ::= x | q | qi | i + i (q∈Z) t ::= x | λx:I.t | λx:T.t | t[i] | t t T ::= X | Πx:I.T | T→T

22 Dependent ML 例 append brake