型推論１（単相型） 2007.

Presentation on theme: "　型推論１（単相型） 2007."— Presentation transcript:

1 　型推論１（単相型） 2007

2 型推論へ１ 強い型付言語の記述上の煩瑣さを軽減

3 型推論へ２

4 型推論へ３

5 型推論の形式的体系について 形式的な記号の集まりからなる論理体系 プログラムの文面を含んだ体系(cf. Hoare logic)
体系の重要な要件 （１）　健全性　（２）　完全性　 （３）推論アルゴリズムの有用性　→ a)決定性 b)効率 「値」の正当性と「型」の正当性の比較　

6 型推論規則のアイデア（例） E0, E1, E2を式として、 もし E0が bool式であることが示され
　　　　かつ　E1の型がTであることが示され 　　　　かつ　E2の型がTであることが示されたなら 　その時、式if E0 then E1 else E2は型Tをもつことが示される これを 形式化して 与えられた式がある型をもつことを証明する(prove) 与えられた式がもつ型を見つける/推論する(find/infer)

7 言語の型システムを与えるとは 言語Lの構文規則を与える （言語Lの意味論を与える） 言語Lの型式の構文（規則）を与える
型推論規則で使われる記法 E : T -　式（または文）Eが型Tを持つという命題 A -　型環境（前提）と呼ぶ。式の中に現われる変数や定数が持つ型を与える.　A(x) = T は型環境Aにおいては、変数（または名前）xは型Tを持つ。 A |- E : T 型判定(type judgment)と呼ばれ、Aのもとで式Eが型Tをもつことを表明・主張する。

8 If-then-else式の型推論規則 E0,E1,E2を式として、 もし E0がbool型の値をもつことが示され
　　　　かつ　E1の型がTであることが示され 　　　　かつ　E2の型がTであることが示されたなら 　その時　if E0 then E1 else E2は型Tをもつことが示される これを 形式化して 　A |- E0 : bool, A |- E1 : T, A |- E2 : T A |- (if E0 then E1 else E2) : T

9 単相型(monomorphic type) の推論規則を持つ言語L

10 Lの型式と記法 L　

11 Lの型推論規則

12 型推論の例１

13 型推論の例２ int>

14 　型推論２（多相型の序）

15 多相型の型推論に向けて 主型(principal type) λ計算に型推論を入れる例 多相型の型推論規則を考える上での注意点
・　型理論λ→ 主型の3性質 型を持つことの特性 多相型の型推論規則を考える上での注意点

16 主型 型多相(type polymorphism, polymorphic type)を許す言語の型推論を説明する上で重要な概念。
　　次の１）、２）　が成立すること。 |- ｔ： T 　が成立。 任意のT1 に対して、|- ｔ：T1　が成立するなら、Tの中の型変数に対する適当な代入σが必ず存在して、 　　　T1≡Tσ　となる。

17 λ式の型 一般のλ式（項）に型を導入する 閉じたλ式は一般に関数に対応するから、 その型は、関数型である。
　λ式の型 一般のλ式（項）に型を導入する 閉じたλ式は一般に関数に対応するから、　その型は、関数型である。 例えば、 λx.x （恒等関数）の定義域の型をTとすると、その値域の型はやはりTである。よって、 λx.x　：　T　→　T　となることは明らか。

18 型理論λ→ λ→における項：（term、式)を次のように定義する： λ→における型式（型のsyntax, 記法）：
変数は項である。　 （x,y,z等の文字を使って表す） ｔ１、ｔ２が項のとき、ｔ１ｔ２も項である。 xが変数、ｔが項のとき、λx.ｔは項である。 λ→における型式（型のsyntax, 記法）： 変数（ α、β、、、）は型式である。　 T1,T2が型式のとき、T1→T2も型式である。 項の並び

19 λ→の型推論規則 A |- x : T 但しA(x)＝Tのとき。 A |- f : T1→T2 A |- a : T1
　　 A |- f a : T2 A + x : T1 |- t : T2 　A |- λx.t : T1 →T2

20 複数の型付けと型変数 K ≡ λxy.x の型は このようにKの型として整合する型は複数あり得る。
　T1→T2→T1 　(T1→T2)→T3→ (T1→T2) 　… このようにKの型として整合する型は複数あり得る。 　一般に型を値とする型変数α、βなどの文字を用いて、 　Kの型を　　K : α→β→α　　 　と表し、このα、βに任意の型を代入すると、Kに整合する全ての型が得られる。 すると、α→β→αがKの主型と考えてよい。

21 λ→の型に関する特徴 主型性(principal type properties)ーー Hindley&Seldan
　λ→の型に関する特徴 主型性(principal type properties)ーー Hindley&Seldan 項　ｔ　が型をもつなら、ｔ　は主型を持つ。 項　ｔ　の主型は計算可能である。（計算するアルゴリズムがある。） 主型を計算するO（ｎ）のアルゴリズムが存在する。 ある項が型を持つ（型付け可能である）ことは、その項は以下の“良い”性質を持つ。 |- t : T （型をもつならば）かつ　t　-*-> s ならば、　|- s : T |- t : T　ならば（型をもつならば）、どの戦略によっても、簡約は停止し、 　　　　　　t　は正規形を持つ。(strong normalizability) 3．　|- t : T1　かつ　|- s : T2　なら（どちらも型付け可能なら） 　　　　　t  s 　か否かを判定する問題は決定可能である。 型を持つλ式は限られていて、既に正規形となっている式でも、型を持たないものもある。　 たとえば, λx. xx は型をもたない。（自己適用など） 　　　課題：これ以外に型を持たない正規系をもつ例は？？