Records_J: STLCにレコードを追加する¶
Require Export Stlc_J.
Require Import Relations.
レコードを追加する¶
MoreStlc_J.vで、レコードを、直積のネストされた使用の構文糖衣として扱う方法を見ました。これは簡単な例にはよいです。しかし、エンコードは非形式的です。(現実的に、もしこの方法でレコードを本当に扱うならパーサ内で実行されることになりますが、パーサはここでは省いています。)そしていずれにしろ、あまり効率的ではありません。これから、レコードを言語の第一級(first-class)のメンバーとしてはどのように扱えるのか見るのも興味があるところです。
前の非形式的定義を思い出してみましょう:
構文:
t ::= 項:
| ...
| {i1=t1, ..., in=tn} レコード
| t.i 射影
v ::= 値:
| ...
| {i1=v1, ..., in=vn} レコード値
T ::= 型:
| ...
| {i1:T1, ..., in:Tn} レコード型
簡約:
ti ==> ti' (ST_Rcd)
--------------------------------------------------------------------
{i1=v1, ..., im=vm, in=tn, ...} ==> {i1=v1, ..., im=vm, in=tn', ...}
t1 ==> t1'
-------------- (ST_Proj1)
t1.i ==> t1'.i
------------------------- (ST_ProjRcd)
{..., i=vi, ...}.i ==> vi
型付け:
Gamma |- t1 : T1 ... Gamma |- tn : Tn
-------------------------------------------------- (T_Rcd)
Gamma |- {i1=t1, ..., in=tn} : {i1:T1, ..., in:Tn}
Gamma |- t : {..., i:Ti, ...}
----------------------------- (T_Proj)
Gamma |- t.i : Ti
レコードを形式化する¶
Module STLCExtendedRecords.
構文と操作的意味¶
レコード型の構文を形式化する最も明らかな方法はこうです:
Module FirstTry.
Definition alist (X : Type) := list (id * X).
Inductive ty : Type :=
| ty_base : id -> ty
| ty_arrow : ty -> ty -> ty
| ty_rcd : (alist ty) -> ty.
残念ながら、ここで Coq の限界につきあたりました。この型は期待する帰納原理を自動的には提供してくれないのです。ty_rcdの場合の帰納法の仮定はリストのty要素について何の情報も提供してくれないのです。このせいで、行いたい証明に対してこの型は役に立たなくなっています。
forall t : ty, P t
*)
(* Check ty_ind.
====>
ty_ind :
forall P : ty -> Prop,
(forall i : id, P (ty_base i)) ->
(forall t : ty, P t -> forall t0 : ty, P t0 -> P (ty_arrow t t0)) ->
(forall a : alist ty, P (ty_rcd a)) -> (* ??? *)
forall t : ty, P t
*)
End FirstTry.
より良い帰納法の原理をCoqから取り出すこともできます。しかしそれをやるための詳細はあまりきれいではありません。またCoqが単純なInductive定義に対して自動生成したものほど直観的でもありません。
幸い、レコードについて、別の、ある意味より単純でより自然な形式化方法があります。既存のlist型の代わりに、型の構文にリストのコンストラクタ(“nil”と”cons”)を本質的に含めてしまうという方法です。
Inductive ty : Type :=
| ty_base : id -> ty
| ty_arrow : ty -> ty -> ty
| ty_rnil : ty
| ty_rcons : id -> ty -> ty -> ty.
Tactic Notation "ty_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "ty_base" | Case_aux c "ty_arrow"
| Case_aux c "ty_rnil" | Case_aux c "ty_rcons" ].
同様に、項のレベルで、空レコードに対応するコンストラクタtm_rnilと、フィールドのリストの前に1つのフィールドを追加するコンストラクタtm_rconsを用意します。
Inductive tm : Type :=
| tm_var : id -> tm
| tm_app : tm -> tm -> tm
| tm_abs : id -> ty -> tm -> tm
(* レコード *)
| tm_proj : tm -> id -> tm
| tm_rnil : tm
| tm_rcons : id -> tm -> tm -> tm.
Tactic Notation "tm_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "tm_var" | Case_aux c "tm_app" | Case_aux c "tm_abs"
| Case_aux c "tm_proj" | Case_aux c "tm_rnil" | Case_aux c "tm_rcons" ].
Some variables, for examples...
いくつかの変数、例えば...
Notation a := (Id 0).
Notation f := (Id 1).
Notation g := (Id 2).
Notation l := (Id 3).
Notation A := (ty_base (Id 4)).
Notation B := (ty_base (Id 5)).
Notation k := (Id 6).
Notation i1 := (Id 7).
Notation i2 := (Id 8).
{ i1:A }
(* Check (ty_rcons i1 A ty_rnil). *)
{ i1:A->B, i2:A }
(* Check (ty_rcons i1 (ty_arrow A B)
(ty_rcons i2 A ty_rnil)). *)
Well-Formedness(正しい形をしていること、整式性)¶
レコードの抽象構文を(リストから nil/cons 構成に)一般化すると、次のような奇妙な型を書くことがができるようになります。
Definition weird_type := ty_rcons X A B.
ここでレコード型の「後部」は実際にはレコード型ではありません!
以降で型ジャッジメントを、weird_typeのようなill-formedの(正しくない形の)型が項に割当てられないように構成します。これをサポートするために、レコード型と項を識別するためのrecord_tyとrecord_tm、およびill-formedの型を排除するためのwell_formed_tyを定義します。
最初に、型がレコード型なのは、それの一番外側のレベルがty_rnilとty_rconsだけを使って構築されたもののときです。
Inductive record_ty : ty -> Prop :=
| rty_nil :
record_ty ty_rnil
| rty_cons : forall i T1 T2,
record_ty (ty_rcons i T1 T2).
同様に、項がレコード項であるのは、tm_rnilとtm_rconsから構築されたもののときです。
Inductive record_tm : tm -> Prop :=
| rtm_nil :
record_tm tm_rnil
| rtm_cons : forall i t1 t2,
record_tm (tm_rcons i t1 t2).
record_tyとrecord_tmは再帰的ではないことに注意します。両者は、一番外側のコンストラクタだけをチェックします。一方well_formed_tyは型全体がwell-formedか(正しい形をしているか)、つまり、レコードのすべての後部(ty_rconsの第2引数)がレコードであるか、を検証します。
もちろん、型だけでなく項についても、ill-formedの可能性を考慮しなければなりません。しかし、別途well_formed_tmを用意しなくても、ill-formed項は型チェックが排除します。なぜなら、型チェックが既に項の構成を調べるからです。
LATER : should they fill in part of this as an exercise? Wedidn’t give rules for it above
(訳注：この”LATER”部分が誰向けに何を言おうとしているのかはっきりしないので、訳さずに残しておきました。)
Inductive well_formed_ty : ty -> Prop :=
| wfty_base : forall i,
well_formed_ty (ty_base i)
| wfty_arrow : forall T1 T2,
well_formed_ty T1 ->
well_formed_ty T2 ->
well_formed_ty (ty_arrow T1 T2)
| wfty_rnil :
well_formed_ty ty_rnil
| wfty_rcons : forall i T1 T2,
well_formed_ty T1 ->
well_formed_ty T2 ->
record_ty T2 ->
well_formed_ty (ty_rcons i T1 T2).
Hint Constructors record_ty record_tm well_formed_ty.
置換¶
Fixpoint subst (x:id) (s:tm) (t:tm) : tm :=
match t with
| tm_var y => if beq_id x y then s else t
| tm_abs y T t1 => tm_abs y T (if beq_id x y then t1 else (subst x s t1))
| tm_app t1 t2 => tm_app (subst x s t1) (subst x s t2)
| tm_proj t1 i => tm_proj (subst x s t1) i
| tm_rnil => tm_rnil
| tm_rcons i t1 tr1 => tm_rcons i (subst x s t1) (subst x s tr1)
end.
簡約¶
次に言語の値を定義します。レコードが値であるのは、そのフィールドがすべて値であるときです。
Inductive value : tm -> Prop :=
| v_abs : forall x T11 t12,
value (tm_abs x T11 t12)
| v_rnil : value tm_rnil
| v_rcons : forall i v1 vr,
value v1 ->
value vr ->
value (tm_rcons i v1 vr).
Hint Constructors value.
レコード型またはレコード項から1つのフィールドを取り出すユーティリティ関数です:
Fixpoint ty_lookup (i:id) (Tr:ty) : option ty :=
match Tr with
| ty_rcons i' T Tr' => if beq_id i i' then Some T else ty_lookup i Tr'
| _ => None
end.
Fixpoint tm_lookup (i:id) (tr:tm) : option tm :=
match tr with
| tm_rcons i' t tr' => if beq_id i i' then Some t else tm_lookup i tr'
| _ => None
end.
step関数は(射影規則について)項レベルのlookup関数を使います。一方、型レベルのlookupはhas_typeで必要になります。
Reserved Notation "t1 '==>' t2" (at level 40).
Inductive step : tm -> tm -> Prop :=
| ST_AppAbs : forall x T11 t12 v2,
value v2 ->
(tm_app (tm_abs x T11 t12) v2) ==> (subst x v2 t12)
| ST_App1 : forall t1 t1' t2,
t1 ==> t1' ->
(tm_app t1 t2) ==> (tm_app t1' t2)
| ST_App2 : forall v1 t2 t2',
value v1 ->
t2 ==> t2' ->
(tm_app v1 t2) ==> (tm_app v1 t2')
| ST_Proj1 : forall t1 t1' i,
t1 ==> t1' ->
(tm_proj t1 i) ==> (tm_proj t1' i)
| ST_ProjRcd : forall tr i vi,
value tr ->
tm_lookup i tr = Some vi ->
(tm_proj tr i) ==> vi
| ST_Rcd_Head : forall i t1 t1' tr2,
t1 ==> t1' ->
(tm_rcons i t1 tr2) ==> (tm_rcons i t1' tr2)
| ST_Rcd_Tail : forall i v1 tr2 tr2',
value v1 ->
tr2 ==> tr2' ->
(tm_rcons i v1 tr2) ==> (tm_rcons i v1 tr2')
where "t1 '==>' t2" := (step t1 t2).
Tactic Notation "step_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "ST_AppAbs" | Case_aux c "ST_App1" | Case_aux c "ST_App2"
| Case_aux c "ST_Proj1" | Case_aux c "ST_ProjRcd"
| Case_aux c "ST_Rcd_Head" | Case_aux c "ST_Rcd_Tail" ].
Notation stepmany := (refl_step_closure step).
Notation "t1 '==>*' t2" := (stepmany t1 t2) (at level 40).
Hint Constructors step.
型付け¶
Definition context := partial_map ty.
次に型付け規則を定義します。これは上述の推論規則をほぼそのまま転写したものです。大きな違いはwell_formed_tyの使用だけです。非形式的な表記では、well-formedレコード型だけを許す文法を使ったので、別のチェックを用意する必要はありませんでした。
ここでは、has_type Gamma t Tが成立するときは常にwell_formed_ty Tが成立するようにしたいところです。つまり、has_typeは項にill-formed型を割当てることはないようにするということです。このことを後で実際に証明します。
しかしながらhas_typeの定義を、well_formed_tyを不必要に使って取り散らかしたくはありません。その代わりwell_formed_tyによるチェックを必要な所だけに配置します。ここで、必要な所というのは、has_typeの帰納的呼び出しによっても未だ型のwell-formed性のチェックが行われていない所のことです。
例えば、T_Varの場合、well_formed_ty Tをチェックします。なぜなら、Tの形がwell-formedであることを調べる帰納的なhas_typeの呼び出しがないからです。同様にT_Absの場合、well_formed_ty T11の証明を必要とします。なぜなら、has_typeの帰納的呼び出しはT12がwell-formedであることだけを保証するからです。
読者が記述しなければならない規則の中でwell_formed_tyチェックが必要なのは、tm_nilの場合だけです。
Inductive has_type : context -> tm -> ty -> Prop :=
| T_Var : forall Gamma x T,
Gamma x = Some T ->
well_formed_ty T ->
has_type Gamma (tm_var x) T
| T_Abs : forall Gamma x T11 T12 t12,
well_formed_ty T11 ->
has_type (extend Gamma x T11) t12 T12 ->
has_type Gamma (tm_abs x T11 t12) (ty_arrow T11 T12)
| T_App : forall T1 T2 Gamma t1 t2,
has_type Gamma t1 (ty_arrow T1 T2) ->
has_type Gamma t2 T1 ->
has_type Gamma (tm_app t1 t2) T2
| T_Proj : forall Gamma i t Ti Tr,
has_type Gamma t Tr ->
ty_lookup i Tr = Some Ti ->
has_type Gamma (tm_proj t i) Ti
| T_RNil : forall Gamma,
has_type Gamma tm_rnil ty_rnil
| T_RCons : forall Gamma i t T tr Tr,
has_type Gamma t T ->
has_type Gamma tr Tr ->
record_ty Tr ->
record_tm tr ->
has_type Gamma (tm_rcons i t tr) (ty_rcons i T Tr).
Hint Constructors has_type.
Tactic Notation "has_type_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "T_Var" | Case_aux c "T_Abs" | Case_aux c "T_App"
| Case_aux c "T_Proj" | Case_aux c "T_RNil" | Case_aux c "T_RCons" ].
例¶
練習問題: ★★ (examples)¶
証明を完成させなさい。
証明の中ではCoq の自動化機能を自由に使って構いません。しかし、もし型システムがどのように動作するか確信できていないなら、最初に基本機能(特にeapplyではなくapply)を使った証明を行い、次に自動化を使ってその証明を圧縮するのがよいかもしれません。
Lemma typing_example_2 :
has_type empty
(tm_app (tm_abs a (ty_rcons i1 (ty_arrow A A)
(ty_rcons i2 (ty_arrow B B)
ty_rnil))
(tm_proj (tm_var a) i2))
(tm_rcons i1 (tm_abs a A (tm_var a))
(tm_rcons i2 (tm_abs a B (tm_var a))
tm_rnil)))
(ty_arrow B B).
Proof.
(* FILL IN HERE *) Admitted.
次の事実(あるいはすぐ上の事実も!)の証明を始める前に、それが何を主張しているかを確認しなさい。
Example typing_nonexample :
~ exists T,
has_type (extend empty a (ty_rcons i2 (ty_arrow A A)
ty_rnil))
(tm_rcons i1 (tm_abs a B (tm_var a)) (tm_var a))
T.
Proof.
(* FILL IN HERE *) Admitted.
Example typing_nonexample_2 : forall y,
~ exists T,
has_type (extend empty y A)
(tm_app (tm_abs a (ty_rcons i1 A ty_rnil)
(tm_proj (tm_var a) i1))
(tm_rcons i1 (tm_var y) (tm_rcons i2 (tm_var y) tm_rnil)))
T.
Proof.
(* FILL IN HERE *) Admitted.
型付けの性質¶
このシステムの進行と保存の証明は、純粋な単純型付きラムダ計算のものと本質的に同じです。しかし、レコードについての技術的補題を追加する必要があります。
Well-Formedness¶
Lemma wf_rcd_lookup : forall i T Ti,
well_formed_ty T ->
ty_lookup i T = Some Ti ->
well_formed_ty Ti.
Proof with eauto.
intros i T.
ty_cases (induction T) Case; intros; try solve by inversion.
Case "ty_rcons".
inversion H. subst. unfold ty_lookup in H0.
remember (beq_id i i0) as b. destruct b; subst...
inversion H0. subst... Qed.
Lemma step_preserves_record_tm : forall tr tr',
record_tm tr ->
tr ==> tr' ->
record_tm tr'.
Proof.
intros tr tr' Hrt Hstp.
inversion Hrt; subst; inversion Hstp; subst; auto.
Qed.
Lemma has_type__wf : forall Gamma t T,
has_type Gamma t T -> well_formed_ty T.
Proof with eauto.
intros Gamma t T Htyp.
has_type_cases (induction Htyp) Case...
Case "T_App".
inversion IHHtyp1...
Case "T_Proj".
eapply wf_rcd_lookup...
Qed.
フィールドのルックアップ¶
補題: もしempty |- v : Tで、かつty_lookup i TがSome Tiを返すならば,tm_lookup i vはある項tiについてSome tiを返す。ただし、has_type empty ti Tiとなる。
証明: 型の導出Htypについての帰納法で証明する。ty_lookup i T = Some Tiであることから、Tはレコード型でなければならない。このこととvが値であることから、ほとんどの場合は精査で除去でき、T_RConsの場合だけが残る。
型導出の最後のステップがT_RConsによるものであるとき、あるi0、t、tr、T、Trについてt = tm_rcons i0 t trかつT = ty_rcons i0 T Trである。
このとき2つの可能性が残る。i0 = iか、そうでないかである。
i = i0のとき、ty_lookup i (ty_rcons i0 T Tr) = Some TiからT = Tiとなる。これからt自身が定理を満たすことが言える。
一方、i <> i0とする。すると
ty_lookup i T = ty_lookup i Tr
かつ
tm_lookup i t = tm_lookup i tr
となる。これから、帰納法の仮定より結果が得られる。
Lemma lookup_field_in_value : forall v T i Ti,
value v ->
has_type empty v T ->
ty_lookup i T = Some Ti ->
exists ti, tm_lookup i v = Some ti /\ has_type empty ti Ti.
Proof with eauto.
intros v T i Ti Hval Htyp Hget.
remember (@empty ty) as Gamma.
has_type_cases (induction Htyp) Case; subst; try solve by inversion...
Case "T_RCons".
simpl in Hget. simpl. destruct (beq_id i i0).
SCase "i is first".
simpl. inversion Hget. subst.
exists t...
SCase "get tail".
destruct IHHtyp2 as [vi [Hgeti Htypi]]...
inversion Hval... Qed.
進行¶
Theorem progress : forall t T,
has_type empty t T ->
value t \/ exists t', t ==> t'.
Proof with eauto.
intros t T Ht.
remember (@empty ty) as Gamma.
generalize dependent HeqGamma.
has_type_cases (induction Ht) Case; intros HeqGamma; subst.
Case "T_Var".
inversion H.
Case "T_Abs".
left...
Case "T_App".
right.
destruct IHHt1; subst...
SCase "t1 is a value".
destruct IHHt2; subst...
SSCase "t2 is a value".
inversion H; subst; try (solve by inversion).
exists (subst x t2 t12)...
SSCase "t2 steps".
destruct H0 as [t2' Hstp]. exists (tm_app t1 t2')...
SCase "t1 steps".
destruct H as [t1' Hstp]. exists (tm_app t1' t2)...
Case "T_Proj".
right. destruct IHHt...
SCase "rcd is value".
destruct (lookup_field_in_value _ _ _ _ H0 Ht H) as [ti [Hlkup _]].
exists ti...
SCase "rcd_steps".
destruct H0 as [t' Hstp]. exists (tm_proj t' i)...
Case "T_RNil".
left...
Case "T_RCons".
destruct IHHt1...
SCase "head is a value".
destruct IHHt2; try reflexivity.
SSCase "tail is a value".
left...
SSCase "tail steps".
right. destruct H2 as [tr' Hstp].
exists (tm_rcons i t tr')...
SCase "head steps".
right. destruct H1 as [t' Hstp].
exists (tm_rcons i t' tr)... Qed.
コンテキスト不変性¶
Inductive appears_free_in : id -> tm -> Prop :=
| afi_var : forall x,
appears_free_in x (tm_var x)
| afi_app1 : forall x t1 t2,
appears_free_in x t1 -> appears_free_in x (tm_app t1 t2)
| afi_app2 : forall x t1 t2,
appears_free_in x t2 -> appears_free_in x (tm_app t1 t2)
| afi_abs : forall x y T11 t12,
y <> x ->
appears_free_in x t12 ->
appears_free_in x (tm_abs y T11 t12)
| afi_proj : forall x t i,
appears_free_in x t ->
appears_free_in x (tm_proj t i)
| afi_rhead : forall x i ti tr,
appears_free_in x ti ->
appears_free_in x (tm_rcons i ti tr)
| afi_rtail : forall x i ti tr,
appears_free_in x tr ->
appears_free_in x (tm_rcons i ti tr).
Hint Constructors appears_free_in.
Lemma context_invariance : forall Gamma Gamma' t S,
has_type Gamma t S ->
(forall x, appears_free_in x t -> Gamma x = Gamma' x) ->
has_type Gamma' t S.
Proof with eauto.
intros. generalize dependent Gamma'.
has_type_cases (induction H) Case;
intros Gamma' Heqv...
Case "T_Var".
apply T_Var... rewrite <- Heqv...
Case "T_Abs".
apply T_Abs... apply IHhas_type. intros y Hafi.
unfold extend. remember (beq_id x y) as e.
destruct e...
Case "T_App".
apply T_App with T1...
Case "T_RCons".
apply T_RCons... Qed.
Lemma free_in_context : forall x t T Gamma,
appears_free_in x t ->
has_type Gamma t T ->
exists T', Gamma x = Some T'.
Proof with eauto.
intros x t T Gamma Hafi Htyp.
has_type_cases (induction Htyp) Case; inversion Hafi; subst...
Case "T_Abs".
destruct IHHtyp as [T' Hctx]... exists T'.
unfold extend in Hctx.
apply not_eq_beq_id_false in H3. rewrite H3 in Hctx...
Qed.
保存¶
Lemma substitution_preserves_typing : forall Gamma x U v t S,
has_type (extend Gamma x U) t S ->
has_type empty v U ->
has_type Gamma (subst x v t) S.
Proof with eauto.
intros Gamma x U v t S Htypt Htypv.
generalize dependent Gamma. generalize dependent S.
tm_cases (induction t) Case;
intros S Gamma Htypt; simpl; inversion Htypt; subst...
Case "tm_var".
simpl. rename i into y.
remember (beq_id x y) as e. destruct e.
SCase "x=y".
apply beq_id_eq in Heqe. subst.
unfold extend in H0. rewrite <- beq_id_refl in H0.
inversion H0; subst. clear H0.
eapply context_invariance...
intros x Hcontra.
destruct (free_in_context _ _ S empty Hcontra) as [T' HT']...
inversion HT'.
SCase "x<>y".
apply T_Var... unfold extend in H0. rewrite <- Heqe in H0...
Case "tm_abs".
rename i into y. rename t into T11.
apply T_Abs...
remember (beq_id x y) as e. destruct e.
SCase "x=y".
eapply context_invariance...
apply beq_id_eq in Heqe. subst.
intros x Hafi. unfold extend.
destruct (beq_id y x)...
SCase "x<>y".
apply IHt. eapply context_invariance...
intros z Hafi. unfold extend.
remember (beq_id y z) as e0. destruct e0...
apply beq_id_eq in Heqe0. subst.
rewrite <- Heqe...
Case "tm_rcons".
apply T_RCons... inversion H7; subst; simpl...
Qed.
Theorem preservation : forall t t' T,
has_type empty t T ->
t ==> t' ->
has_type empty t' T.
Proof with eauto.
intros t t' T HT.
remember (@empty ty) as Gamma. generalize dependent HeqGamma.
generalize dependent t'.
has_type_cases (induction HT) Case;
intros t' HeqGamma HE; subst; inversion HE; subst...
Case "T_App".
inversion HE; subst...
SCase "ST_AppAbs".
apply substitution_preserves_typing with T1...
inversion HT1...
Case "T_Proj".
destruct (lookup_field_in_value _ _ _ _ H2 HT H)
as [vi [Hget Htyp]].
rewrite H4 in Hget. inversion Hget. subst...
Case "T_RCons".
apply T_RCons... eapply step_preserves_record_tm...
Qed.
☐
End STLCExtendedRecords.