Records: STLCにレコードを追加する


Set Warnings "-notation-overridden,-parsing".
From Coq Require Import Strings.String.
From PLF Require Import Maps.
From PLF Require Import Imp.
From PLF Require Import Smallstep.
From PLF Require Import Stlc.

レコードを追加する


MoreStlc章で、レコードを、直積のネストの構文糖衣として扱う方法を見ました。 これは簡単な例にはいいのですが、しかし変換は非形式的です。 （現実的に、もしこの方法でレコードを本当に扱うならパーサ内で実行されることになりますが、パーサはここでは省いています。） そしてとにかく、効率的ではありません。 これから、レコードを言語の第一級(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 (string * X).

Inductive ty : Type :=
  | Base : string -> ty
  | Arrow : ty -> ty -> ty
  | TRcd : (alist ty) -> ty.

残念ながら、ここで Coq の限界につきあたりました。 この型は期待する帰納原理を自動的には提供してくれないのです。 TRcdの場合の帰納法の仮定はリストのty要素について何の情報も提供してくれないのです。 このせいで、行いたい証明に対してこの型は役に立たなくなっています。 

(* Check ty_ind. 
   ====> 
    ty_ind : 
      forall P : ty -> Prop, 
        (forall i : id, P (Base i)) -> 
        (forall t : ty, P t -> forall t0 : ty, P t0  
                            -> P (Arrow t t0)) -> 
        (forall a : alist ty, P (TRcd a)) ->    (* ??? *) 
        forall t : ty, P t 
*)

End FirstTry.

より良い帰納法の原理をCoqから取り出すこともできます。 しかしそれをやるための詳細はあまりきれいではありません。 またCoqが単純なInductive定義に対して自動生成したものほど直観的でもありません。
幸い、レコードについて、別の、ある意味より単純でより自然な形式化方法があります。 Coq 標準のlist型の代わりに、型の構文にリストのコンストラクタ（"nil"と"cons"）を本質的に含めてしまうという方法です。

Inductive ty : Type :=
  | Base : string -> ty
  | Arrow : ty -> ty -> ty
  | RNil : ty
  | RCons : string -> ty -> ty -> ty.

同様に、項のレベルで、空レコードに対応するコンストラクタtrnilと、フィールドのリストの前に1つのフィールドを追加するコンストラクタrconsを用意します。

Inductive tm : Type :=
  | var : string -> tm
  | app : tm -> tm -> tm
  | abs : string -> ty -> tm -> tm
  
  | rproj : tm -> string -> tm
  | trnil : tm
  | rcons : string -> tm -> tm -> tm.

いくつかの例です...
Open Scope string_scope.

Notation a := "a".
Notation f := "f".
Notation g := "g".
Notation l := "l".
Notation A := (Base "A").
Notation B := (Base "B").
Notation k := "k".
Notation i1 := "i1".
Notation i2 := "i2".

{ i1:A }


{ i1:A->B, i2:A }


Well-Formedness(正しい形をしていること、整式性)


レコードの抽象構文をリストから nil/cons 構成に一般化したことで、次のような奇妙な型を書くことがができるという問題が発生します。

Definition weird_type := RCons X A B.

ここでレコード型の「後部」は実際にはレコード型ではありません!

以降で型ジャッジメントを、weird_typeのようなill-formedの（正しくない形の）型が項に割当てられないように構成します。 これをサポートするために、レコード型と項を識別するためのrecord_tyとrecord_tm、 およびill-formedの型を排除するためのwell_formed_tyを定義します。

最初に、型がレコード型なのは、 それの一番外側のレベルがRNilとRConsだけを使って構築されたもののときです。

Inductive record_ty : ty -> Prop :=
  | RTnil :
        record_ty RNil
  | RTcons : forall i T1 T2,
        record_ty (RCons i T1 T2).

With this, we can define well-formed types.

Inductive well_formed_ty : ty -> Prop :=
  | wfBase : forall i,
        well_formed_ty (Base i)
  | wfArrow : forall T1 T2,
        well_formed_ty T1 ->
        well_formed_ty T2 ->
        well_formed_ty (Arrow T1 T2)
  | wfRNil :
        well_formed_ty RNil
  | wfRCons : forall i T1 T2,
        well_formed_ty T1 ->
        well_formed_ty T2 ->
        record_ty T2 ->
        well_formed_ty (RCons i T1 T2).

Hint Constructors record_ty well_formed_ty.

record_tyが再帰的ではないことに注意します。 これは一番外側のコンストラクタだけをチェックします。 一方well_formed_tyは型全体がwell-formedか(正しい形をしているか)、 つまり、レコードのすべての後部（RConsの第2引数）がレコードであるか、を検証します。
もちろん、型だけでなく項についても、ill-formedの可能性を考慮しなければなりません。 しかし、別途well_formed_tmを用意しなくても、ill-formed項は型チェックが排除します。 なぜなら、型チェックが既に項の構成を調べているからです。 必要なものはrecord_ty相当のもので、項の外側がtrnilとrconsで作られていればレコード項だという保証をするだけです。

Inductive record_tm : tm -> Prop :=
  | rtnil :
        record_tm trnil
  | rtcons : forall i t1 t2,
        record_tm (rcons i t1 t2).

Hint Constructors record_tm.

置換

Substitution extends easily.

Fixpoint subst (x:string) (s:tm) (t:tm) : tm :=
  match t with
  | var y => if eqb_string x y then s else t
  | abs y T t1 => abs y T
                     (if eqb_string x y then t1 else (subst x s t1))
  | app t1 t2 => app (subst x s t1) (subst x s t2)
  | rproj t1 i => rproj (subst x s t1) i
  | trnil => trnil
  | rcons i t1 tr1 => rcons i (subst x s t1) (subst x s tr1)
  end.

Notation "'[' x ':=' s ']' t" := (subst x s t) (at level 20).

簡約


レコードが値であるのは、そのフィールドがすべて値であるときです。

Inductive value : tm -> Prop :=
  | v_abs : forall x T11 t12,
      value (abs x T11 t12)
  | v_rnil : value trnil
  | v_rcons : forall i v1 vr,
      value v1 ->
      value vr ->
      value (rcons i v1 vr).

Hint Constructors value.

簡約を定義するために、レコード項から1つのフィールドを取り出すユーティリティ関数を定義しておきます。

Fixpoint tlookup (i:string) (tr:tm) : option tm :=
  match tr with
  | rcons i' t tr' => if eqb_string i i' then Some t else tlookup i tr'
  | _ => None
  end.

step関数は、射影規則において、この項レベルのlookup関数を使います。

Reserved Notation "t1 '-->' t2" (at level 40).

Inductive step : tm -> tm -> Prop :=
  | ST_AppAbs : forall x T11 t12 v2,
         value v2 ->
         (app (abs x T11 t12) v2) --> ([x:=v2]t12)
  | ST_App1 : forall t1 t1' t2,
         t1 --> t1' ->
         (app t1 t2) --> (app t1' t2)
  | ST_App2 : forall v1 t2 t2',
         value v1 ->
         t2 --> t2' ->
         (app v1 t2) --> (app v1 t2')
  | ST_Proj1 : forall t1 t1' i,
        t1 --> t1' ->
        (rproj t1 i) --> (rproj t1' i)
  | ST_ProjRcd : forall tr i vi,
        value tr ->
        tlookup i tr = Some vi ->
        (rproj tr i) --> vi
  | ST_Rcd_Head : forall i t1 t1' tr2,
        t1 --> t1' ->
        (rcons i t1 tr2) --> (rcons i t1' tr2)
  | ST_Rcd_Tail : forall i v1 tr2 tr2',
        value v1 ->
        tr2 --> tr2' ->
        (rcons i v1 tr2) --> (rcons i v1 tr2')

where "t1 '-->' t2" := (step t1 t2).

Notation multistep := (multi step).
Notation "t1 '-->*' t2" := (multistep t1 t2) (at level 40).

Hint Constructors step.

型付け


次に型付け規則を定義します。これは上述の推論規則をほぼそのまま転写したものです。 大きな違いは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であることだけを保証するからです。

Fixpoint Tlookup (i:string) (Tr:ty) : option ty :=
  match Tr with
  | RCons i' T Tr' =>
      if eqb_string i i' then Some T else Tlookup i Tr'
  | _ => None
  end.

Definition context := partial_map ty.

Reserved Notation "Gamma '|-' t '\in' T" (at level 40).

Inductive has_type : context -> tm -> ty -> Prop :=
  | T_Var : forall Gamma x T,
      Gamma x = Some T ->
      well_formed_ty T ->
      Gamma |- (var x) \in T
  | T_Abs : forall Gamma x T11 T12 t12,
      well_formed_ty T11 ->
      (update Gamma x T11) |- t12 \in T12 ->
      Gamma |- (abs x T11 t12) \in (Arrow T11 T12)
  | T_App : forall T1 T2 Gamma t1 t2,
      Gamma |- t1 \in (Arrow T1 T2) ->
      Gamma |- t2 \in T1 ->
      Gamma |- (app t1 t2) \in T2
  
  | T_Proj : forall Gamma i t Ti Tr,
      Gamma |- t \in Tr ->
      Tlookup i Tr = Some Ti ->
      Gamma |- (rproj t i) \in Ti
  | T_RNil : forall Gamma,
      Gamma |- trnil \in RNil
  | T_RCons : forall Gamma i t T tr Tr,
      Gamma |- t \in T ->
      Gamma |- tr \in Tr ->
      record_ty Tr ->
      record_tm tr ->
      Gamma |- (rcons i t tr) \in (RCons i T Tr)

where "Gamma '|-' t '\in' T" := (has_type Gamma t T).

Hint Constructors has_type.

例


練習問題: ★★ (examples), standard

証明を完成させなさい。 証明の中ではCoq の自動化機能を自由に使って構いません。 しかし、もし型システムがどのように動作するか確信できていないなら、最初に基本機能（特にeapplyではなくapply）を使った証明を行い、次に自動化を使ってその証明を圧縮するのがよいかもしれません。 証明を始める前に、主張が何かを確かめなさい。

Lemma typing_example_2 :
  empty |-
    (app (abs a (RCons i1 (Arrow A A)
                      (RCons i2 (Arrow B B)
                       RNil))
              (rproj (var a) i2))
            (rcons i1 (abs a A (var a))
            (rcons i2 (abs a B (var a))
             trnil))) \in
    (Arrow B B).
Proof.
Admitted.

Example typing_nonexample :
  ~ exists T,
      (update empty a (RCons i2 (Arrow A A)
                                RNil)) |-
               (rcons i1 (abs a B (var a)) (var a)) \in
               T.
Proof.
Admitted.

Example typing_nonexample_2 : forall y,
  ~ exists T,
    (update empty y A) |-
           (app (abs a (RCons i1 A RNil)
                     (rproj (var a) i1))
                   (rcons i1 (var y) (rcons i2 (var y) trnil))) \in
           T.
Proof.
Admitted.

型付けの性質


このシステムの進行と保存の証明は、純粋な単純型付きラムダ計算のものと本質的に同じです。 しかし、レコードについての技術的補題を追加する必要があります。

Well-Formedness


Lemma wf_rcd_lookup : forall i T Ti,
  well_formed_ty T ->
  Tlookup i T = Some Ti ->
  well_formed_ty Ti.
Proof with eauto.
  intros i T.
  induction T; intros; try solve_by_invert.
  -
    inversion H. subst. unfold Tlookup in H0.
    destruct (eqb_string i s)...
    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,
  Gamma |- t \in T -> well_formed_ty T.
Proof with eauto.
  intros Gamma t T Htyp.
  induction Htyp...
  -
    inversion IHHtyp1...
  -
    eapply wf_rcd_lookup...
Qed.

フィールドのルックアップ


補題: もし empty |- v : T で、かつ Tlookup i T が Some Ti を返すならば, tlookup i v はある項 ti について Some ti を返す。 ただし、empty |- ti \in Ti となる。
証明: 型の導出Htypについての帰納法で証明する。 Tlookup i T = Some Ti であることから、 T はレコード型でなければならない。 このこととvが値であることから、ほとんどの場合は精査で除去でき、 T_RConsの場合だけが残る。
型導出の最後のステップがT_RConsによるものであるとき、 あるi0、t、tr、T、Trについて t = rcons i0 t tr かつ T = TRCons i0 T Tr である。
このとき2つの可能性が残る。i0 = i か、そうでないかである。
  • i = i0 のとき、Tlookup i (RCons i0 T Tr) = Some Ti から T = Ti となる。これから t自身が定理を満たすことが言える。
  • 一方、i <> i0 とする。すると
            Tlookup i T = Tlookup i Tr
    かつ
            tlookup i t = tlookup i tr
    となる。 これから、帰納法の仮定より結果が得られる。
形式的に記述すると以下の通りです。

Lemma lookup_field_in_value : forall v T i Ti,
  value v ->
  empty |- v \in T ->
  Tlookup i T = Some Ti ->
  exists ti, tlookup i v = Some ti /\ empty |- ti \in Ti.
Proof with eauto.
  intros v T i Ti Hval Htyp Hget.
  remember (@empty ty) as Gamma.
  induction Htyp; subst; try solve_by_invert...
  -
    simpl in Hget. simpl. destruct (eqb_string i i0).
    +
      simpl. inversion Hget. subst.
      exists t...
    +
      destruct IHHtyp2 as [vi [Hgeti Htypi]]...
      inversion Hval... Qed.

進行


Theorem progress : forall t T,
     empty |- t \in T ->
     value t \/ exists t', t --> t'.
Proof with eauto.
  intros t T Ht.
  remember (@empty ty) as Gamma.
  generalize dependent HeqGamma.
  induction Ht; intros HeqGamma; subst.
  -
    
    
    inversion H.
  -
    
    
    left...
  -
    
    
    right.
    destruct IHHt1; subst...
    +
      destruct IHHt2; subst...
      *
      
      
        inversion H; subst; try solve_by_invert.
        exists ([x:=t2]t12)...
      *
        
        
        destruct H0 as [t2' Hstp]. exists (app t1 t2')...
    +
      
      
      destruct H as [t1' Hstp]. exists (app t1' t2)...
  -
    
    
    right. destruct IHHt...
    +
      
      
      destruct (lookup_field_in_value _ _ _ _ H0 Ht H)
        as [ti [Hlkup _]].
      exists ti...
    +
      
      
      destruct H0 as [t' Hstp]. exists (rproj t' i)...
  -
    
    
    left...
  -
    
    
    destruct IHHt1...
    +
      destruct IHHt2; try reflexivity.
      *
      
      
        left...
      *
        
        
        right. destruct H2 as [tr' Hstp].
        exists (rcons i t tr')...
    +
      
      
      right. destruct H1 as [t' Hstp].
      exists (rcons i t' tr)... Qed.

コンテキスト不変性


Inductive appears_free_in : string -> tm -> Prop :=
  | afi_var : forall x,
      appears_free_in x (var x)
  | afi_app1 : forall x t1 t2,
      appears_free_in x t1 -> appears_free_in x (app t1 t2)
  | afi_app2 : forall x t1 t2,
      appears_free_in x t2 -> appears_free_in x (app t1 t2)
  | afi_abs : forall x y T11 t12,
        y <> x ->
        appears_free_in x t12 ->
        appears_free_in x (abs y T11 t12)
  | afi_proj : forall x t i,
     appears_free_in x t ->
     appears_free_in x (rproj t i)
  | afi_rhead : forall x i ti tr,
      appears_free_in x ti ->
      appears_free_in x (rcons i ti tr)
  | afi_rtail : forall x i ti tr,
      appears_free_in x tr ->
      appears_free_in x (rcons i ti tr).

Hint Constructors appears_free_in.

Lemma context_invariance : forall Gamma Gamma' t S,
     Gamma |- t \in S ->
     (forall x, appears_free_in x t -> Gamma x = Gamma' x) ->
     Gamma' |- t \in S.
Proof with eauto.
  intros. generalize dependent Gamma'.
  induction H;
    intros Gamma' Heqv...
  -
    apply T_Var... rewrite <- Heqv...
  -
    apply T_Abs... apply IHhas_type. intros y Hafi.
    unfold update, t_update. destruct (eqb_stringP x y)...
  -
    apply T_App with T1...
  -
    apply T_RCons... Qed.

Lemma free_in_context : forall x t T Gamma,
   appears_free_in x t ->
   Gamma |- t \in T ->
   exists T', Gamma x = Some T'.
Proof with eauto.
  intros x t T Gamma Hafi Htyp.
  induction Htyp; inversion Hafi; subst...
  -
    destruct IHHtyp as [T' Hctx]... exists T'.
    unfold update, t_update in Hctx.
    rewrite false_eqb_string in Hctx...
Qed.

保存


Lemma substitution_preserves_typing : forall Gamma x U v t S,
     (update Gamma x U) |- t \in S ->
     empty |- v \in U ->
     Gamma |- ([x:=v]t) \in S.
Proof with eauto.
  intros Gamma x U v t S Htypt Htypv.
  generalize dependent Gamma. generalize dependent S.
  induction t;
    intros S Gamma Htypt; simpl; inversion Htypt; subst...
  -
    simpl. rename s into y.
    unfold update, t_update in H0.
    destruct (eqb_stringP x y) as [Hxy|Hxy].
    +
    
    
      subst.
      inversion H0; subst. clear H0.
      eapply context_invariance...
      intros x Hcontra.
      destruct (free_in_context _ _ S empty Hcontra)
        as [T' HT']...
      inversion HT'.
    +
    
    
      apply T_Var...
  -
    rename s into y. rename t into T11.
    apply T_Abs...
    destruct (eqb_stringP x y) as [Hxy|Hxy].
    +
      
      
      eapply context_invariance...
      subst.
      intros x Hafi. unfold update, t_update.
      destruct (eqb_string y x)...
    +
      
      
      apply IHt. eapply context_invariance...
      intros z Hafi. unfold update, t_update.
      destruct (eqb_stringP y z)...
      subst. rewrite false_eqb_string...
  -
    apply T_RCons... inversion H7; subst; simpl...
Qed.

Theorem preservation : forall t t' T,
     empty |- t \in T ->
     t --> t' ->
     empty |- t' \in T.
Proof with eauto.
  intros t t' T HT.
  remember (@empty ty) as Gamma. generalize dependent HeqGamma.
  generalize dependent t'.
  induction HT;
    intros t' HeqGamma HE; subst; inversion HE; subst...
  -
    
    
    inversion HE; subst...
    +
      
      
      apply substitution_preserves_typing with T1...
      inversion HT1...
  -
    
    
    destruct (lookup_field_in_value _ _ _ _ H2 HT H)
      as [vi [Hget Htyp]].
    rewrite H4 in Hget. inversion Hget. subst...
  -
    
    
    apply T_RCons... eapply step_preserves_record_tm...
Qed.
☐

End STLCExtendedRecords.