Typechecking_J: STLCの型チェッカ
STLCのhas_type関係は(あるコンテキストのもとで)項が型に属するという意味を定義します。
しかし、それ自身では、項に型付けができるかどうかの「チェック方法」は与えません。
幸いにも、has_typeを定義する規則は構文指向(syntax directed)です。 項の形にそのまま従います。このことから、 型付け規則を型チェック「関数」の節にそのまま変換することができます。 この関数は、項とコンテキストをとり、その項の型を返すか、項が型付けできないという信号を出します。
幸いにも、has_typeを定義する規則は構文指向(syntax directed)です。 項の形にそのまま従います。このことから、 型付け規則を型チェック「関数」の節にそのまま変換することができます。 この関数は、項とコンテキストをとり、その項の型を返すか、項が型付けできないという信号を出します。
最初に、2つの型の等しさを比較する関数が必要です...
Fixpoint beq_ty (T1 T2:ty) : bool :=
match T1,T2 with
| ty_Bool, ty_Bool =>
true
| ty_arrow T11 T12, ty_arrow T21 T22 =>
andb (beq_ty T11 T21) (beq_ty T12 T22)
| _,_ =>
false
end.
... そして、beq_tyが返すブール値の結果と2つの入力が等しいという論理命題との間の、
通常の双方向結合を確立します。
Lemma beq_ty_refl : ∀ T1,
beq_ty T1 T1 = true.
Proof.
intros T1. induction T1; simpl.
reflexivity.
rewrite IHT1_1. rewrite IHT1_2. reflexivity. Qed.
Lemma beq_ty__eq : ∀ T1 T2,
beq_ty T1 T2 = true → T1 = T2.
Proof with auto.
intros T1. induction T1; intros T2 Hbeq; destruct T2; inversion Hbeq.
Case "T1=ty_Bool".
reflexivity.
Case "T1=ty_arrow T1_1 T1_2".
apply andb_true in H0. destruct H0 as [Hbeq1 Hbeq2].
apply IHT1_1 in Hbeq1. apply IHT1_2 in Hbeq2. subst... Qed.
そしてこれが型チェッカです。与えられた項の構造をたどって調べ、Some T または None
を返します。
部分項の型を調べるために再帰呼び出しをするたびに、結果についてパターンマッチをして、
Noneでないことを確認します。
tm_appの場合はさらに、パターンマッチングで関数型の矢印の右側と左側を抽出します
(そして関数の型が ty_arrow T11 T12 という形ではないときは失敗します
(つまりNoneを返します))。
Fixpoint type_check (Γ:context) (t:tm) : option ty :=
match t with
| tm_var x => Γ x
| tm_abs x T11 t12 => match type_check (extend Γ x T11) t12 with
| Some T12 => Some (ty_arrow T11 T12)
| _ => None
end
| tm_app t1 t2 => match type_check Γ t1, type_check Γ t2 with
| Some (ty_arrow T11 T12),Some T2 =>
if beq_ty T11 T2 then Some T12 else None
| _,_ => None
end
| tm_true => Some ty_Bool
| tm_false => Some ty_Bool
| tm_if x t f => match type_check Γ x with
| Some ty_Bool =>
match type_check Γ t, type_check Γ f with
| Some T1, Some T2 =>
if beq_ty T1 T2 then Some T1 else None
| _,_ => None
end
| _ => None
end
end.
この型チェックアルゴリズムが正しいことを検証するため、
この関数がオリジナルのhas_type関係について健全(sound)で完全(complete)
であることを示します。
つまり、type_checkとhas_typeが同じ部分関数を定義することです。
Theorem type_checking_sound : ∀ Γ t T,
type_check Γ t = Some T → has_type Γ t T.
Proof with eauto.
intros Γ t. generalize dependent Γ.
tm_cases (induction t) Case; intros Γ T Htc; inversion Htc.
Case "tm_var"...
Case "tm_app".
remember (type_check Γ t1) as TO1.
remember (type_check Γ t2) as TO2.
destruct TO1 as [T1|]; try solve by inversion;
destruct T1 as [|T11 T12]; try solve by inversion.
destruct TO2 as [T2|]; try solve by inversion.
remember (beq_ty T11 T2) as b.
destruct b; try solve by inversion.
symmetry in Heqb. apply beq_ty__eq in Heqb.
inversion H0; subst...
Case "tm_abs".
rename i into y. rename t into T1.
remember (extend Γ y T1) as G'.
remember (type_check G' t0) as TO2.
destruct TO2; try solve by inversion.
inversion H0; subst...
Case "tm_true"...
Case "tm_false"...
Case "tm_if".
remember (type_check Γ t1) as TOc.
remember (type_check Γ t2) as TO1.
remember (type_check Γ t3) as TO2.
destruct TOc as [Tc|]; try solve by inversion.
destruct Tc; try solve by inversion.
destruct TO1 as [T1|]; try solve by inversion.
destruct TO2 as [T2|]; try solve by inversion.
remember (beq_ty T1 T2) as b.
destruct b; try solve by inversion.
symmetry in Heqb. apply beq_ty__eq in Heqb.
inversion H0. subst. subst...
Qed.
Theorem type_checking_complete : ∀ Γ t T,
has_type Γ t T → type_check Γ t = Some T.
Proof with auto.
intros Γ t T Hty.
has_type_cases (induction Hty) Case; simpl.
Case "T_Var"...
Case "T_Abs". rewrite IHHty...
Case "T_App".
rewrite IHHty1. rewrite IHHty2.
rewrite (beq_ty_refl T11)...
Case "T_True"...
Case "T_False"...
Case "T_If". rewrite IHHty1. rewrite IHHty2.
rewrite IHHty3. rewrite (beq_ty_refl T)...
Qed.
End STLCChecker.