Stlc_J: 単純型付きラムダ計算

Require Export Types_J.

単純型付きラムダ計算

単純型付きラムダ計算(Simply Typed Lambda-Calculus, STLC)は、関数抽象(functional abstraction)を具現する、小さな、核となる計算体系です。関数抽象は、ほとんどすべての実世界のプログラミング言語に何らかの形(関数、手続き、メソッド等)で現れます。

ここでは、この計算体系(構文、スモールステップ意味論、型付け規則)とその性質(進行と保存)の形式化を、これまでやったのとまったく同じパターンで行います。(扱うためにいくらかの作業が必要になる)新しい技術的挑戦は、すべて変数束縛(variable binding)と置換(substitution)の機構から生じます。

概観

STLC は基本型(base types)の何らかの集まりの上に構成されます。基本型はブール型、数値、文字列などです。実際にどの基本型を選択するかは問題ではありません。どう選択しても、言語の構成とその理論的性質はまったく同じように導かれます。これから、簡潔にするため、しばらくはBoolだけとしましょう。この章の終わりには、さらに基本型を追加する方法がわかるでしょう。また後の章では、純粋なSTLCに、対、レコード、サブタイプ、変更可能状態などの他の便利な構成要素をとり入れてよりリッチなものにします。

ブール値から始めて3つのものを追加します:

• 変数
• 関数抽象
• (関数)適用

これから、以下の抽象構文コンストラクタが出てきます(ここではこれを非形式的BNF記法で書き出します。後に形式化します。):

t ::= x                       変数
    | \x:T.t1                 関数抽象
    | t1 t2                   関数適用
    | true                    定数 true
    | false                   定数 false
    | if t1 then t2 else t3   条件式

関数抽象\x:T.t1の\記号はよくギリシャ文字のラムダ(λ)で記述されます(これがラムダ計算の名前の由来です)。変数xは関数のパラメータ(parameter)、項t1は関数の本体(body)と呼ばれます。付記された:Tは関数が適用される引数の型を定めます。

例をいくつか:

• \x:Bool. xブール値の恒等関数。
• (\x:Bool. x) trueブール値trueに適用された、ブール値の恒等関数。
• \x:Bool. if x then false else trueブール値の否定関数。
• \x:Bool. trueすべての(ブール値の)引数に対してtrueを返す定数関数。
• \x:Bool. \y:Bool. x2つのブール値をとり、最初のものを返す2引数関数。(なお、Coqと同様、2引数関数は、実際には本体が1引数関数である1引数関数です。)
• (\x:Bool. \y:Bool. x) false true2つのブール値をとり、最初のものを返す2引数関数を、ブール値falseとtrueに適用したもの。なお、Coqと同様、関数適用は左結合です。つまり、この式は((\x:Bool. \y:Bool. x) false) trueと構文解析されます。
• \f:Bool->Bool. f (f true)(ブール値からブール値への)「関数」fを引数にとる高階関数。この高階関数は、fをtrueに適用し、その値にさらにfを適用します。
• (\f:Bool->Bool. f (f true)) (\x:Bool. false)上記高階関数を、常にfalseを返す定数関数に適用したもの。

最後のいくつかの例で示されたように、STLCは高階(higher-order)関数の言語です。他の関数を引数として取る関数や、結果として他の関数を返す関数を書き下すことができます。

別の注目点は、名前を持つ(named)関数を定義する基本構文を、STLCは何も持っていないことです。すべての関数は「名無し」(“anonymous”)です。後のMoreStlc_J章で、この体系に名前を持つ関数を追加することが簡単であることがわかるでしょう。実のところ、基本的な命名と束縛の機構はまったく同じです。

STLCの型にはBoolが含まれます。この型はブール値定数trueとfalse、および結果がブール値になるより複雑な計算の型です。それに加えて「関数型」(arrow types)があります。これは関数の型です。

T ::= Bool
    | T1 -> T2

例えば:

• \x:Bool. falseは型Bool->Boolを持ちます。
• \x:Bool. xは型Bool->Boolを持ちます。
• (\x:Bool. x) trueは型Boolを持ちます。
• \x:Bool. \y:Bool. xは型Bool->Bool->Bool(つまりBool -> (Bool->Bool))を持ちます。
• (\x:Bool. \y:Bool. x) falseは型Bool->Boolを持ちます。
• (\x:Bool. \y:Bool. x) false trueは型Boolを持ちます。
• \f:Bool->Bool. f (f true)は型(Bool->Bool) -> Boolを持ちます。
• (\f:Bool->Bool. f (f true)) (\x:Bool. false)は型Boolを持ちます。

構文

Module STLC.

型

Inductive ty : Type :=
  | ty_Bool  : ty
  | ty_arrow : ty -> ty -> ty.

項

Inductive tm : Type :=
  | tm_var : id -> tm
  | tm_app : tm -> tm -> tm
  | tm_abs : id -> ty -> tm -> tm
  | tm_true : tm
  | tm_false : tm
  | tm_if : tm -> tm -> tm -> tm.

ここで注目すべきは、関数抽象\x:T.t(形式的にはtm_abs x T t)には常にパラメータの型(T)が付記されることです。これは Coq(あるいは他のML、Haskellといった関数型言語)と対照的です。それらは、付記がないものを型推論で補完します。

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_true"
  | Case_aux c "tm_false" | Case_aux c "tm_if" ].

いくつかの例...

Notation a := (Id 0).
Notation b := (Id 1).
Notation c := (Id 2).

idB = \a:Bool. a

Notation idB :=
  (tm_abs a ty_Bool (tm_var a)).

idBB = \a:Bool->Bool. a

Notation idBB :=
  (tm_abs a (ty_arrow ty_Bool ty_Bool) (tm_var a)).

idBBBB = \a:(Bool->Bool)->(Bool->Bool). a

Notation idBBBB :=
  (tm_abs a (ty_arrow (ty_arrow ty_Bool ty_Bool)
                      (ty_arrow ty_Bool ty_Bool))
    (tm_var a)).

k = \a:Bool. \b:Bool. a

Notation k := (tm_abs a ty_Bool (tm_abs b ty_Bool (tm_var a))).

(これらをDefinitionではなくNotationとすることで、autoに扱いやすくしています。)

操作的意味論

STLC項のスモールステップ意味論を定義するために、いつものように、値の集合を定義することから始めます。次に、自由変数(free variables)と置換(substitution)という、重大な概念を定義します。これらは関数適用式の簡約規則に使われます。そして最後に、スモールステップ関係自体を与えます。

値

STLCの値を定義するために、いくつかの場合を考えなければなりません。

最初に、言語のブール値については、状況は明確です:trueとfalseだけが値です。(if式は決して値ではありません。)

二番目に、関数適用は明らかに値ではありません。関数適用は関数が何らかの引数に対して呼ばれたことを表しているのですから、明らかにこれからやることが残っています。

三番目に、関数抽象については選択肢があります:

• \a:A.t1が値であるのは、t1が値であるときのみである、 とすることができます。つまり、関数の本体が(どのような引数に適用されるかわからない状態で可能な限り)簡約済みであるときのみ、ということです。
• あるいは、\a:A.t1は常に値である、とすることもできます。t1が値であるかどうかに関係なく、です。言いかえると、簡約は関数抽象で止まる、とすることです。

Coq は最初の選択肢を取っています。例えば、

Eval simpl in (fun a:bool => 3 + 4)

はfun a:bool => 7となります。しかし実際の関数型プログラミング言語のほとんどは、第二の選択肢を取っています。つまり、関数の本体の簡約は、関数が実際に引数に適用されたときにのみ開始されます。ここでは、同様に第二の選択肢を選びます。

最後に、関数抽象の中を簡約することを選択しなかったため、変数が値であるかをどうかを心配する必要はなくなります。なぜなら、プログラムの簡約は常に「外側から内側に」行われ、step関係は常に閉じた(自由変数を持たない)項だけを対象とするからです。

Inductive value : tm -> Prop :=
  | v_abs : forall x T t,
      value (tm_abs x T t)
  | t_true :
      value tm_true
  | t_false :
      value tm_false.

Hint Constructors value.

自由変数と置換

これから問題の核心に入ります: 項の変数を別の項で置換する操作です。

この操作は後で関数適用の操作的意味論を定義するために使います。関数適用では、関数本体の中の関数パラメータを引数項で置換することが必要になります。例えば、

(\x:Bool. if x then true else x) false

は、関数の本体のパラメータxをfalseで置換することで、falseに簡約されます。一般に、ある項tの変数xの出現を、与えらえた項sで置換できることが必要です。非形式的な議論では、これは通常[s/xt ] と書き、「tのxをsで置換する」と読みます。

いくつかの例を示します:

• [true / a(if a then a else false)] はif true then true else falseとなります。
• [true / aa] はtrueとなります。
• [true / a(if a then a else b)] はif true then true else bとなります。
• [true / ab] はbとなります。
• [true / afalse] はfalseとなります(何もしない置換です)。
• [true / a(:Bool. if y then a else false)] は\y:Bool. if y then true else falseとなります。
• [true / a(:Bool. a)] は\y:Bool. trueとなります。
• [true / a(:Bool. y)] は\y:Bool. yとなります。
• [true / a(:Bool. a)] は\a:Bool. aとなります。

最後の例はとても重要です。\a:Bool. aのaをtrueで置換したものは、\a:Bool. trueに「なりません」! 理由は、\a:Bool. aの本体のaは関数抽象で束縛されている(bound)からです。このaは新しいローカルな名前で、たまたまグローバルな名前aと同じ綴りであったものです。

以下が、非形式的な定義です...

[s/x]x = s
[s/x]y = y                                     if x <> y
[s/x](\x:T11.t12)   = \x:T11. t12
[s/x](\y:T11.t12)   = \y:T11. [s/x]t12         if x <> y
[s/x](t1 t2)        = ([s/x]t1) ([s/x]t2)
[s/x]true           = true
[s/x]false          = false
[s/x](if t1 then t2 else t3) =
                    if [s/x]t1 then [s/x]t2 else [s/x]t3

... そして形式的には:

Fixpoint subst (s:tm) (x:id) (t:tm) : tm :=
  match t with
  | tm_var x' => if beq_id x x' then s else t
  | tm_abs x' T t1 => tm_abs x' T (if beq_id x x' then t1 else (subst s x t1))
  | tm_app t1 t2 => tm_app (subst s x t1) (subst s x t2)
  | tm_true => tm_true
  | tm_false => tm_false
  | tm_if t1 t2 t3 => tm_if (subst s x t1) (subst s x t2) (subst s x t3)
  end.

技術的注釈: 置換は、もしs、つまり他の項の変数を置換する項が、それ自身に自由変数を含むときを考えると、定義がよりトリッキーなものになります。ここで興味があるのは閉じた項についてのstep関係の定義のみなので、そのさらなる複雑さは避けることができます。

簡約

STLCのスモールステップ簡約関係は、これまで見てきたものと同じパターンに従います。直観的には、関数適用を簡約するため、最初に左側をリテラル関数になるまで簡約します。次に左側(引数)を値になるまで簡約します。そして最後に関数の本体の束縛変数を引数で置換します。この最後の規則は、非形式的には次のように書きます:

(\a:T.t12) v2 ==> [v2/a]t12

これは伝統的にベータ簡約(“beta-reduction”)と呼ばれます。

非形式的に:

---------------------------                    (ST_AppAbs)
(\a:T.t12) v2 ==> [v2/a]t12

         t1 ==> t1'
      ----------------                           (ST_App1)
      t1 t2 ==> t1' t2

         t2 ==> t2'
      ----------------                        (ST_App2)
      v1 t2 ==> v1 t2'

(これに通常のブール値の規則をプラスします)。

形式的には:

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

Inductive step : tm -> tm -> Prop :=
  | ST_AppAbs : forall x T t12 v2,
         value v2 ->
         (tm_app (tm_abs x T t12) v2) ==> (subst v2 x 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_IfTrue : forall t1 t2,
      (tm_if tm_true t1 t2) ==> t1
  | ST_IfFalse : forall t1 t2,
      (tm_if tm_false t1 t2) ==> t2
  | ST_If : forall t1 t1' t2 t3,
      t1 ==> t1' ->
      (tm_if t1 t2 t3) ==> (tm_if t1' t2 t3)

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_IfTrue"
  | Case_aux c "ST_IfFalse" | Case_aux c "ST_If" ].

Notation stepmany := (refl_step_closure step).
Notation "t1 '==>*' t2" := (stepmany t1 t2) (at level 40).

Hint Constructors step.

例

Lemma step_example1 :
  (tm_app idBB idB) ==>* idB.
Proof.
  eapply rsc_step.
    apply ST_AppAbs.
    apply v_abs.
  simpl.
  apply rsc_refl.  Qed.


Lemma step_example1' :
  (tm_app idBB idB) ==>* idB.
Proof. normalize.  Qed.

Lemma step_example2 :
  (tm_app idBB (tm_app idBB idB)) ==>* idB.
Proof.
  eapply rsc_step.
    apply ST_App2. auto.
    apply ST_AppAbs. auto.
  eapply rsc_step.
    apply ST_AppAbs. simpl. auto.
  simpl. apply rsc_refl.  Qed.

再び、上述のnormalizeタクティックを使って、証明を簡単にすることができます。

Lemma step_example2' :
  (tm_app idBB (tm_app idBB idB)) ==>* idB.
Proof.
  normalize.
Qed.

練習問題: ★★ (step_example3)

次の証明をnormalizeを使う方法と使わない方法の両方で行ないなさい。

Lemma step_example3 :
       (tm_app (tm_app idBBBB idBB) idB)
  ==>* idB.
Proof.
  (* FILL IN HERE *) Admitted.

☐

型付け

コンテキスト

問い: 項 “x y” の型は何でしょう？

答え: それはxとyの型に依存します!

つまり、項に型を付けるためには、その自由変数の型についてどういう仮定をしなければならないかを知る必要があります。

このために、3つのものの間の型付けジャッジメント(“typing judgment”)を用意します。これを非形式的にはGamma |- t : Tと記述します。ここでGammaは「型付けコンテキスト」(“typing context”)、つまり、変数から型への写像です。

モジュールにおける部分写像の定義は隠蔽します。なぜなら、実際には SfLib で定義されているからです。

Definition context := partial_map ty.

Module Context.

Definition partial_map (A:Type) := id -> option A.

Definition empty {A:Type} : partial_map A := (fun _ => None).

Definition extend {A:Type} (Gamma : partial_map A) (x:id) (T : A) :=
  fun x' => if beq_id x x' then Some T else Gamma x'.

Lemma extend_eq : forall A (ctxt: partial_map A) x T,
  (extend ctxt x T) x = Some T.
Proof.
  intros. unfold extend. rewrite <- beq_id_refl. auto.
Qed.

Lemma extend_neq : forall A (ctxt: partial_map A) x1 T x2,
  beq_id x2 x1 = false ->
  (extend ctxt x2 T) x1 = ctxt x1.
Proof.
  intros. unfold extend. rewrite H. auto.
Qed.

End Context.

型付け関係

非形式的に:

                      Gamma x = T
                     --------------                              (T_Var)
                     Gamma |- x : T

               Gamma , x:T11 |- t12 : T12
              ----------------------------                       (T_Abs)
              Gamma |- \x:T11.t12 : T11->T12

                 Gamma |- t1 : T11->T12
                   Gamma |- t2 : T11
                 ----------------------                          (T_App)
                  Gamma |- t1 t2 : T12

                  --------------------                          (T_True)
                  Gamma |- true : Bool

                 ---------------------                         (T_False)
                 Gamma |- false : Bool

Gamma |- t1 : Bool    Gamma |- t2 : T    Gamma |- t3 : T
--------------------------------------------------------          (T_If)
           Gamma |- if t1 then t2 else t3 : T

記法Gamma , x:Tは「部分写像Gammaを拡張してxをTに写像するようにしたもの」を表します。

Inductive has_type : context -> tm -> ty -> Prop :=
  | T_Var : forall Gamma x T,
      Gamma x = Some T ->
      has_type Gamma (tm_var x) T
  | T_Abs : forall Gamma x T11 T12 t12,
      has_type (extend Gamma x T11) t12 T12 ->
      has_type Gamma (tm_abs x T11 t12) (ty_arrow T11 T12)
  | T_App : forall T11 T12 Gamma t1 t2,
      has_type Gamma t1 (ty_arrow T11 T12) ->
      has_type Gamma t2 T11 ->
      has_type Gamma (tm_app t1 t2) T12
  | T_True : forall Gamma,
       has_type Gamma tm_true ty_Bool
  | T_False : forall Gamma,
       has_type Gamma tm_false ty_Bool
  | T_If : forall t1 t2 t3 T Gamma,
       has_type Gamma t1 ty_Bool ->
       has_type Gamma t2 T ->
       has_type Gamma t3 T ->
       has_type Gamma (tm_if t1 t2 t3) T.

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_True"
  | Case_aux c "T_False" | Case_aux c "T_If" ].

Hint Constructors has_type.

例

Example typing_example_1 :
  has_type empty (tm_abs a ty_Bool (tm_var a)) (ty_arrow ty_Bool ty_Bool).
Proof.
  apply T_Abs. apply T_Var. reflexivity.  Qed.

has_typeコンストラクタをヒントデータベースに追加したことから、これを auto は直接解くことができることに注意します。

Example typing_example_1' :
  has_type empty (tm_abs a ty_Bool (tm_var a)) (ty_arrow ty_Bool ty_Bool).
Proof. auto.  Qed.

Hint Unfold beq_id beq_nat extend.

非形式的に書くと

empty |- \a:A. \b:A->A. b (b a))
      : A -> (A->A) -> A.

となるものが次の例です:

Example typing_example_2 :
  has_type empty
    (tm_abs a ty_Bool
       (tm_abs b (ty_arrow ty_Bool ty_Bool)
          (tm_app (tm_var b) (tm_app (tm_var b) (tm_var a)))))
    (ty_arrow ty_Bool (ty_arrow (ty_arrow ty_Bool ty_Bool) ty_Bool)).
Proof with auto using extend_eq.
  apply T_Abs.
  apply T_Abs.
  eapply T_App. apply T_Var...
  eapply T_App. apply T_Var...
  apply T_Var...
Qed.

練習問題: ★★, optional

auto、eauto、eapplyを使わずに同じ結果を証明しなさい。

Example typing_example_2_full :
  has_type empty
    (tm_abs a ty_Bool
       (tm_abs b (ty_arrow ty_Bool ty_Bool)
          (tm_app (tm_var b) (tm_app (tm_var b) (tm_var a)))))
    (ty_arrow ty_Bool (ty_arrow (ty_arrow ty_Bool ty_Bool) ty_Bool)).
Proof.
  (* FILL IN HERE *) Admitted.

☐

練習問題: ★★ (typing_example_3)

次の型付けが成立することを形式的に証明しなさい:

   empty |- (\a:Bool->B. \b:Bool->Bool. \c:Bool.
               b (a c))
         : T.

Example typing_example_3 :
  exists T,
    has_type empty
      (tm_abs a (ty_arrow ty_Bool ty_Bool)
         (tm_abs b (ty_arrow ty_Bool ty_Bool)
            (tm_abs c ty_Bool
               (tm_app (tm_var b) (tm_app (tm_var a) (tm_var c))))))
      T.

Proof with auto.
  (* FILL IN HERE *) Admitted.

☐

項が「型付けできない」ことを証明することもできます。例えば\a:Bool. \b:Bool, a bに型をつける型付けが存在しないこと、つまり、

~ exists T,
    empty |- (\a:Bool. \b:Bool, a b) : T.

を形式的にチェックしましょう。

Example typing_nonexample_1 :
  ~ exists T,
      has_type empty
        (tm_abs a ty_Bool
            (tm_abs b ty_Bool
               (tm_app (tm_var a) (tm_var b))))
        T.
Proof.
  intros C. destruct C.

  inversion H. subst. clear H.
  inversion H5. subst. clear H5.
  inversion H4. subst. clear H4.
  inversion H2. subst. clear H2.
  inversion H5. subst. clear H5.

  inversion H1.  Qed.

練習問題: ★★★ (typing_nonexample_3)

別の型を持たない例:

    ~ (exists S, exists T,
          empty |- (\a:S. a a) : T).

Example typing_nonexample_3 :
  ~ (exists S, exists T,
        has_type empty
          (tm_abs a S
             (tm_app (tm_var a) (tm_var a)))
          T).
Proof.
  (* FILL IN HERE *) Admitted.

☐

練習問題: ★ (typing_statements)

以下のうち証明できるのものを挙げなさい。

• b:Bool |- \a:Bool.a : Bool->Bool
• exists T,  empty |- (\b:Bool->Bool. \a:Bool. b a) : T
• exists T,  empty |- (\b:Bool->Bool. \a:Bool. a b) : T
• exists S, a:S |- (\b:Bool->Bool. b) a : S
• exists S, exists T,  a:S |- (a a a) : T

☐

練習問題: ★, optional (more_typing_statements)

以下の命題のうち証明できるものを挙げなさい。証明できるものについては、存在限量された変数に入る具体的な値を示しなさい。

• exists T,  empty |- (\b:B->B->B. \a:B, b a) : T
• exists T,  empty |- (\a:A->B, \b:B-->C, \c:A, b (a c)):T
• exists S, exists U, exists T,  a:S, b:U |- \c:A. a (b c) : T
• exists S, exists T,  a:S |- \b:A. a (a b) : T
• exists S, exists U, exists T,  a:S |- a (\c:U. c a) : T

☐

性質

自由な出現

変数xが項 t に自由に出現する(appears free in a term t)とは、tがxの出現を含み、その出現がxのラベルが付けられた関数抽象のスコープ内にないことです。例えば:

• \x:T->U. x yにおいてyは自由に現れますがxはそうではありません。

• (\x:T->U. x y) xにおいてはxとyはともに自由に現れます。

• \x:T->U. \y:T. x yにおいては自由に現れる変数はありません。

  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_if1 : forall x t1 t2 t3, appears_free_in x t1 -> appears_free_in x (tm_if t1 t2 t3) | afi_if2 : forall x t1 t2 t3, appears_free_in x t2 -> appears_free_in x (tm_if t1 t2 t3) | afi_if3 : forall x t1 t2 t3, appears_free_in x t3 -> appears_free_in x (tm_if t1 t2 t3).

  Tactic Notation “afi_cases” tactic(first) ident(c) := first; [ Case_aux c “afi_var” | Case_aux c “afi_app1” | Case_aux c “afi_app2” | Case_aux c “afi_abs” | Case_aux c “afi_if1” | Case_aux c “afi_if2” | Case_aux c “afi_if3” ].

  Hint Constructors appears_free_in.

自由に現れる変数を持たない項を「閉じている」(closed)と言います。

Definition closed (t:tm) :=
  forall x, ~ appears_free_in x t.

置換

最初に、自由変数と型付けコンテキストを結び付ける技術的な補題が必要になります。変数xが項tに自由に現れ、tがコンテキストGammaで型付けされるならば、Gammaはxに型を付けなければなりません。

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'.

「証明」:xがtに自由に現れることの証明についての帰納法によって、すべてのコンテキストGammaについて、tがGammaのもとで型付けされるならばGammaはxに型をつけることを示す。

• 最後の規則がafi_varの場合、t = xである。そして、tがGammaで型付けされるという仮定から、そのまま、Gammaでxに型付けされることが言える。

• 最後の規則がafi_app1の場合、t = t1 t2でxはt1に自由に出現する。tがGammaのもとで型付けされることから、型付け規則からt1も型付けされることになる。従って帰納仮定よりGammaはxに型を付ける。

• 他のほとんどの場合も同様である。xがtの部分項に自由に現れ、tがGammaで片付けされることから、xが出現しているtの部分項は同様にGammaで型付けされる。従って帰納仮定より求めるべき結果が得られる。

• 残るのは、最後の規則がafi_absの場合だけである。この場合、t = \y:T11.t12でxはt12に自由に現れる。またxはyと異なっている。前の場合との違いは、tはGammaのもとで型付けされているが、その本体t12は(Gamma, y:T11)のもとで型付けされているという点である。このため、帰納仮定は、拡張されたコンテキスト(Gamma, y:T11)でxに型付けされる、という主張になる。Gammaのもとでxに型が付けられるという結論を得るため、xとyが異なっているという点に注意して、補題extend_neqを使う。

  Proof. intros. generalize dependent Gamma. generalize dependent T. afi_cases (induction H) Case; intros; try solve [inversion H0; eauto]. Case “afi_abs”. inversion H1; subst. apply IHappears_free_in in H7. apply not_eq_beq_id_false in H. rewrite extend_neq in H7; assumption. Qed.

次に、空コンテキストで型付けされる任意の項は閉じている(自由変数を持たない)、という事実を必要とします。

練習問題: ★★ (typable_empty__closed)

Corollary typable_empty__closed : forall t T,
    has_type empty t T  ->
    closed t.
Proof.
  (* FILL IN HERE *) Admitted.

☐

しばしば、証明Gamma |- t : Tがあるとき、コンテキストGammaを別のコンテキストGamma'に置換する必要が出てきます。これはどのような場合に安全でしょうか？直観的には、tに自由に現れるすべての変数について、Gamma'がGammaと同じ型を割当てることが少なくとも必要です。実際、この条件だけが必要になります。

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.

「証明」:Gamma |- t : Tの導出についての帰納法を使う。

• 導出の最後の規則がT_Varのとき、t = xかつGamma x = Tである。 仮定からGamma' x = Tであるから、T_VarよりGamma' |- t : Tとなる。

• 最後の規則がT_Absのとき、t = \y:T11. t12かつT = T11 -> T12かつGamma, y:T11 |- t12 : T12である。帰納法の仮定は、任意のコンテキストGamma''について、もしGamma, y:T11とGamma''がt12内のすべての自由変数に同じ型を割り当てるならば、t12はGamma''のもとで型T12を持つ、である。Gamma'を、t内の自由変数についてGammaと同じ割当てをするコンテキストとする。示すべきことはGamma' |- \y:T11. t12 : T11 -> T12である。 T_Absより、Gamma', y:T11 |- t12 : T12を示せば十分である。帰納仮定(ただしGamma'' = Gamma', y:T11とする)より、Gamma, y:T11とGamma', y:T11がt12内に自由に現れるすべての変数について割当てが一致することを示せば十分である。 t12に自由に出現する任意の変数はyであるか、それ以外の変数かである。Gamma, y:T11とGamma', y:T11は明らかにyについては一致する。それ以外の場合、t12に自由に出現するy以外の任意の変数はt = \y:T11. t12にも自由に現れることに注意すると、GammaとGamma'がそのような変数について割当てが一致するという仮定より、Gamma, y:T11とGamma', y:T11も一致する。

• 最後の規則がT_Appの場合、t = t1 t2かつGamma |- t1 : T2 -> TかつGamma |- t2 : T2である。帰納法の仮定の1つは、すべてのコンテキストGamma'について、Gamma'とGammaがt1のすべての自由変数について同じ割当てをするならば、Gamma'のもとでt1は型T2 -> Tを持つ、となる。t2についても同様の帰納仮定がある。証明すべきことは、Gamma'がGammaとt1 t2のすべての自由変数について同一の割当てをするという仮定の上で、Gamma'のもとでもt1 t2が型Tを持つ、ということである。T_Appより、t1とt2がそれぞれGamma'とGammaのもとで同じ型を持つことを示せば十分である。しかし、t1のすべての自由変数はt1 t2でも自由変数であり、t2の自由変数についても同様である。ゆえに、2つの帰納仮定から求める結果が得られる。

  Proof with eauto. intros. generalize dependent Gamma’. has_type_cases (induction H) Case; intros; auto. Case “T_Var”. apply T_Var. rewrite <- H0... Case “T_Abs”. apply T_Abs. apply IHhas_type. intros x0 Hafi.

  unfold extend. remember (beq_id x x0) as e. destruct e...
  

  Case “T_App”. apply T_App with T11... Qed.

ついに、簡約が型を保存することの証明の概念的な核心です。つまり、「置換」が型を保存することを調べます。

非形式的には、置換補題(Substitution Lemma)と呼ばれる補題は次のことを主張します:項tが自由変数xを持ち、xが型Uを持つという仮定のもとでtに型Tが付けられるとする。また、別の項vについて、vが型Uを持つことが示されるとする。このとき、vはtの型付けに関するxについての上述の仮定を満たすことから、tにおけるそれぞれのxの出現をvで置換することはできるはずであり、その置換によって型がTのままである新しい項を得る。

「補題」: もしGamma,x:U |- t : Tかつ|- v : Uならば [Gamma |-v/xt : T].

Lemma substitution_preserves_typing : forall Gamma x U v t T,
     has_type (extend Gamma x U) t T ->
     has_type empty v U   ->
     has_type Gamma (subst v x t) T.

補題の主張について技術的に巧妙な点の1つは、vに型Uを割当てるのが「空」コンテキストであることです。言い換えると、vが閉じていると仮定しています。この仮定はT_Absの場合の証明を(この場面でとりうる別の仮定であるGamma |- v : Uを仮定するのに比べて)大幅に簡単にします。なぜなら、コンテキスト不変補題(the context invariance lemma)が、どんなコンテキストでもvが型Uを持つことを示すからです。v内の自由変数がT-Absによってコンテキストに導入された変数と衝突することを心配する必要はありません。

「証明」:tについての帰納法によって、すべてのTとGammaについてGamma,x:U |- t : Tかつ|- v : Uならば、Gamma |- [v/xt : T]であることを証明する。

• tが変数のとき、tがxであるか否かによって2つの場合がある。
  • t = xの場合、Gamma, x:U |- x : Tという事実から、U = Tになる。ここで示すべきことは、空コンテキストのもとでvが型U = Tという仮定の上で、Gammaのもとで[v/xx = v] が型Tを持つことである。これは、コンテキスト不変補題、つまり、閉じた項が空コンテキストのもとで型Tを持つならば、その項は任意のコンテキストのもとで型Tを持つ、ということから得られる。
  • tがx以外の変数yである場合、yの型はGamma,x:UのもとでもGammaのもとでも変わらないということに注意するだけでよい。
• tが関数抽象\y:T11. t12のとき、帰納仮定から、すべてのGamma'とT'について、Gamma',x:U |- t12 : T'かつ|- v : UならばGamma' |- [v/xt12 : T’]となる。特にGamma,y:T11,x:U |- t12 : T12かつ|- v : UならばGamma,y:T11 |- [v/xt12 : T12] となる。xとyが同じ変数か否かでまた2つの場合がある。 最初にx = yとすると、置換の定義から[v/xt = t] である。これからGamma |- t : Tを示すだけで良い。しかし、Gamma,x:U |- t : Tであって、\y:T11. t12にyは自由に出現することはないから、コンテキスト不変補題からGamma |- t : Tとなる。 次にx <> yとする。型付け関係の反転から [Gamma,x:U,y:T11 |- t12 :T12] であり、これとコンテキスト不変補題からGamma,y:T11,x:U |- t12 : T12となる。これから帰納仮定を使って、Gamma,y:T11 |- [v/xt12 : T12] が得られる。T_AbsからGamma |- \y:T11. [v/xt12 : T11->T12] となり、置換の定義から(x <> yに注意すると)求めるGamma |- \y:T11. [v/xt12 : T11->T12] が得られる。
• tが関数適用t1 t2のときは、結果は置換の定義と帰納法の仮定から直ぐに 得られる。
• 他の場合は、関数適用の場合と同様である。

別の技術的な注: この証明は、型の導出についての帰納法ではなく項についての帰納法を使うことが議論をより簡単にするという、珍しいものです。この理由は、仮定has_type (extend Gamma x U) t Tがある意味で完全に一般化されていないからです。ある意味というのは、型関係の1つの「スロット」、つまりコンテキストが、単に1つの変数ではないということです。このことにより、Coq がもともと持っている帰納法のタクティックでは必要な帰納法の仮定が導かれません。これを回避することは可能ですが、そのために必要な一般化はちょっとトリッキーです。これに対して項tは完全に一般化されています。

Proof with eauto.
  intros Gamma x U v t T Ht Hv.
  generalize dependent Gamma. generalize dependent T.
  tm_cases (induction t) Case; intros T Gamma H;

    inversion H; subst; simpl...
  Case "tm_var".
    rename i into y. remember (beq_id x y) as e. destruct e.
    SCase "x=y".
      apply beq_id_eq in Heqe. subst.
      rewrite extend_eq in H2.
      inversion H2; subst. clear H2.
                  eapply context_invariance... intros x Hcontra.
      destruct (free_in_context _ _ T empty Hcontra) as [T' HT']...
      inversion HT'.
    SCase "x<>y".
      apply T_Var. rewrite extend_neq in H2...
  Case "tm_abs".
    rename i into y. 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...
Qed.

置換補題は一種の「交換性」(“commutation” property)と見なせます。直観的には、置換と型付けはどの順でやってもよいということを主張しています。(適切なコンテキストのもとで)項tとvに個別に型付けをしてから置換によって両者を組合せても良いし、置換を先にやって後から[v/xt ] に型をつけることもできます。どちらでも結果は同じです。

保存

さて、(型の)保存(preservation)を証明する道具立ては揃いました。保存とは、閉じた項tが型Tを持ち、t'への評価ステップを持つならば、t'はまた型Tを持つ閉じた項である、という性質です。言い換えると、スモールステップ評価関係は型を保存するということです。

Theorem preservation : forall t t' T,
     has_type empty t T  ->
     t ==> t'  ->
     has_type empty t' T.

「証明」:|- t : Tの導出についての帰納法を使う。

• まず最後の規則がT_Var、T_Abs、T_True、T_Falseである場合は外して良い。なぜなら、これらの場合、tはステップを進むことができないからである。

• 導出の最後の規則がT_Appのとき、t = t1 t2である。 このとき、t1 t2がt'にステップを進めたことを示すのに使われた規則について、3つの場合が考えられる。

  • t1 t2がST_App1によってステップを進めた場合、t1がステップを進めたものをt1'とする。すると帰納仮定よりt1'はt1と同じ型を持ち、したがって、t1' t2はt1 t2と同じ型を持つ。
  • ST_App2の場合は同様である。
  • t1 t2がST_AppAbsによってステップを進めた場合、t1 = \x:T11.t12であり、t1 t2はsubst t2 x t12にステップする。すると置換が型を保存するという事実から求める結果となる。

• 導出の最後の規則がT_Ifのとき、t = if t1 then t2 else t3であり、 やはりtのステップについて3つの場合がある。

  • tがt2またはt3にステップした場合、結果は直ぐである。なぜならt2とt3はtと同じ型だからである。
  • そうでない場合、tはST_Ifでステップする。このとき、 帰納法の仮定から直接求める結果が得られる。

  Proof with eauto. remember (@empty ty) as Gamma. intros t t’ T HT. generalize dependent t’. has_type_cases (induction HT) Case; intros t’ HE; subst Gamma; subst; try solve [inversion HE; subst; auto]. Case “T_App”. inversion HE; subst...

  SCase "ST_AppAbs".
    apply substitution_preserves_typing with T11...
    inversion HT1...
  

  Qed.

練習問題: ★★, recommended (subject_expansion_stlc)

[]
*)

FILL IN HERE このファイルの前の練習問題で、算術式とブール式の簡単な言語についての主部展開性についてききました(訳注:実際には Types_J.v内の練習問題)。STLCでこの性質は成立するでしょうか？つまり、t ==> t'かつhas_type t' Tならばhas_type t Tということが常に言えるでしょうか？もしそうならば証明しなさい。そうでなければ、反例を挙げなさい。

(* FILL IN HERE *)☐

進行

最後に、「進行」定理(the progress theorem)は閉じた、型が付けられる項は行き詰まらないことを示します。つまり、型が付けられる項は、値であるか、または評価ステップを進むことができるか、どちらかです。

Theorem progress : forall t T,
     has_type empty t T ->
     value t \/ exists t', t ==> t'.

「証明」:|- t : Tの導出についての帰納法による。

• 導出の最後の規則はT_Varではありえない。なぜなら、 空コンテキストにおいて変数には型付けできないからである。

• T_True、T_False、T_Absの場合は自明である。 なぜなら、これらの場合tは値だからである。

• 導出の最後の規則がT_Appの場合、t = t1 t2であり、t1およびt2はどちらも空コンテキストで型付けされる。特に型T2があって、|- t1 : T2 -> Tかつ|- t2 : T2となる。帰納法の仮定から、t1は値であるか、評価ステップを進むことができる。

  • t1が値のとき、t2を考えると、 帰納仮定からさらに値である場合と評価ステップを進む場合がある。
  • t2が値のとき、t1は値で関数型であるから、ラムダ抽象である。 ゆえに、t1 t2はST_AppAbsでステップを進むことができる。
  • そうでなければ、t2はステップを進むことができる。したがってST_App2でt1 t2もステップを進むことができる。
  • t1がステップを進むことができるとき、ST_App1でt1 t2もステップを進むことができる。

• 導出の最後の規則がT_Ifのとき、t = if t1 then t2 else t3でt1は型Boolを持つ。帰納仮定よりt1は値かステップを進むことができるかどちらかである。

  • t1が値のとき、その型がBoolであることからt1はtrueまたはfalseである。trueならばtはt2に進み、そうでなければt3に進む。
  • そうでないとき、t1はステップを進むことができる。したがって(ST_Ifより)tもステップを進むことができる。

  Proof with eauto. intros t T Ht. remember (@empty ty) as Gamma. has_type_cases (induction Ht) Case; subst Gamma... Case “T_Var”.

  inversion H.
  

  Case “T_App”.

  right. destruct IHHt1...
  
  SCase "t1 is a value".
    destruct IHHt2...
    SSCase "t2 is also a value".
  
      inversion H; subst. exists (subst t2 x t)...
      solve by inversion. solve by inversion.
    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_If”. right. destruct IHHt1...

  SCase "t1 is a value".
  
    inversion H; subst. solve by inversion.
    SSCase "t1 = true". eauto.
    SSCase "t1 = false". eauto.
  
  SCase "t1 also steps".
    destruct H as [t1' Hstp]. exists (tm_if t1' t2 t3)...
  

  Qed.

練習問題: ★★★, optional (progress_from_term_ind)

型についての帰納法ではなく項についての帰納法でも進行の証明ができることを示しなさい。

Theorem progress' : forall t T,
     has_type empty t T ->
     value t \/ exists t', t ==> t'.
Proof.
  intros t.
  tm_cases (induction t) Case; intros T Ht; auto.
  (* FILL IN HERE *) Admitted.

☐

型の一意性

練習問題: ★★★ (types_unique)

STLCの別の好ましい性質は、型が唯一であることです。つまり、与えらえた項については(与えられたコンテキストで)高々1つの型しか型付けされません。

この主張を形式化し、証明しなさい。

(* FILL IN HERE *)

☐

さらなる練習問題

なにも見ることなく、単純型付きラムダ計算の進行定理と保存定理を書き下しなさい。

☐

STLCの評価関係に次の新しい規則を加えたとします:

| T_Strange : forall x t,
     has_type empty (tm_abs x Bool t) Bool

この規則を加えても真であるSTLCの性質は以下のうちどれでしょうか？それぞれについて、「真のまま」または「偽に変わる」と書きなさい。偽に変わるものについては、反例を挙げなさい。

• stepの決定性
• 進行
• 保存

☐

step関係からST_App1規則を除いたとします。このとき前の練習問題の3つの性質のうち、偽になるものはどれでしょう？偽になるものについては、反例を挙げなさい。

☐

End STLC.

練習問題: 算術を持つSTLC

STLCが実際のプログラミング言語の核として機能することを見るため、数値についての具体的な基本型と定数、いくつかの基本操作を追加しましょう。

Module STLCArith.

構文と操作的意味

型について、自然数を基本型として加えます(そして簡潔さのためブール型を除きます)。

Inductive ty : Type :=
  | ty_arrow : ty -> ty -> ty
  | ty_Nat   : ty.

項について、自然数の定数、1つ前をとる関数、1つ後をとる関数、積算、ゼロか否かのテスト...を加えます。

Inductive tm : Type :=
  | tm_var : id -> tm
  | tm_app : tm -> tm -> tm
  | tm_abs : id -> ty -> tm -> tm
  | tm_nat  : nat -> tm
  | tm_succ : tm -> tm
  | tm_pred : tm -> tm
  | tm_mult : tm -> tm -> tm
  | tm_if0  : tm -> 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_nat"
  | Case_aux c "tm_succ" | Case_aux c "tm_pred"
  | Case_aux c "tm_mult" | Case_aux c "tm_if0" ].

算術を拡張したSTLCの定義と性質の形式化を完成させなさい。特に:

• STLCについてここまでやってきたこと(定義から進行定理まで)の全体をコピーして、 ファイルのこの部分にペーストしなさい。

• subst操作とstep関係の定義を拡張して、算術の操作の適切な節を含むようにしなさい。

• オリジナルのSTLCの性質の証明を拡張して、新しい構文を扱うようにしなさい。 Coq がその証明を受理することを確認しなさい。

  (* FILL IN HERE *)

☐

End STLCArith.