概念

さて、サブタイプ(subtyping)の学習に入ります。 サブタイプはおそらく、近年設計されたプログラミング言語で使われる静的型システムの最も特徴的な機能です。

動機付けのための例

レコードを持つ単純型付きラムダ計算では、項

    (\r:{y:Nat}. (r.y)+1) {x=10,y=11}

は型付けできません。なぜなら、 これはフィールドが1つのレコードを引数としてとる関数に2つのフィールドを持つレコードが与えられている部分を含んでいて、 一方、T_App規則は関数の定義域の型は引数の型に完全に一致することを要求するからです。

しかしこれは馬鹿らしいことです。 実際には関数に、必要とされるものより良い引数を与えているのです! この関数の本体がレコード引数rに対して行うことができることはおそらく、 そのフィールドyを射影することだけです。型から許されることは他にはありません。 すると、他にxフィールドが存在するか否かは何の違いもないはずです。 これから、直観的に、 この関数は少なくともyフィールドは持つ任意のレコード値に適用可能であるべきと思われます。

同じことを別の観点から見ると、より豊かなフィールドを持つレコードは、 そのサブセットのフィールドだけを持つレコードと 「任意のコンテキストで少なくとも同等の良さである」と言えるでしょう。 より長い(多いフィールドを持つ)レコード型の任意の値は、 より短かいレコード型が求められるコンテキストで「安全に」(safely)使えるという意味においてです。 コンテキストがより短かい型のものを求めているときに、より長い型のものを与えた場合、 何も悪いことは起こらないでしょう(形式的には、プログラムは行き詰まることはないでしょう)。

ここではたらいている一般原理はサブタイプ(付け)(subtyping)と呼ばれます。 型Tの値が求められている任意のコンテキストで型Sの値が安全に使えるとき、 「SはTのサブタイプである」と言い、非形式的に S <: T と書きます。 サブタイプの概念はレコードだけではなく、関数、対、など言語のすべての型コンストラクタに適用されます。

サブタイプとオブジェクト指向言語

サブタイプは多くのプログラミング言語で重要な役割を演じます。 特に、オブジェクト指向言語のサブクラス(subclassing)の概念と近い関係にあります。

(JavaやC#等の)オブジェクトはレコードと考えることができます。 いくつかのフィールドは関数(「メソッド」)で、いくつかのフィールドはデータ値 (「フィールド」または「インスタンス変数」)です。 オブジェクトoのメソッドmを引数a1..anのもとで呼ぶことは、 oからmフィールドを射影として抽出して、それをa1..anに適用することです。

オブジェクトの型はクラス(class)またはインターフェース(interface) として与えることができます。 この両者はどちらも、どのメソッドとどのデータフィールドをオブジェクトが提供するかを記述します。

クラスやインターフェースは、サブクラス(subclass)関係やサブインターフェース (subinterface)関係で関係づけられます。 サブクラス(またはサブインターフェース)に属するオブジェクトには、スーパークラス (またはスーパーインターフェース) に属するオブジェクトのメソッドとフィールドのすべての提供することが求められ、 おそらくそれに加えてさらにいくつかのものを提供します。

サブクラス(またはサブインターフェース)のオブジェクトをスーパークラス(またはスーパーインターフェース) のオブジェクトの場所で使えるという事実は、 複雑なライブラリの構築にきわめて便利なほどの柔軟性を提供します。 例えば、Javaの Swing フレームワークのようなグラフィカルユーザーインターフェースツールキットは、 スクリーンに表示できユーザとインタラクションできるグラフィカルな表現を持つすべてのオブジェクトに共通のフィールドとメソッドを集めた、抽象インターフェースComponentを定義するでしょう。 そのようなオブジェクトの例としては、典型的なGUIのボタン、チェックボックス、スクロールバーなどがあります。 この共通インターフェースのみに依存するメソッドは任意のそれらのオブジェクトに適用できます。

もちろん、実際のオブジェクト指向言語はこれらに加えてたくさんの他の機能を持っています。 フィールドは更新できます。フィールドとメソッドはprivateと宣言できます。 クラスはまた、 オブジェクトを構成しそのメソッドをインプリメントするのに使われる「コード」を与えます。 そしてサブクラスのコードは「継承」を通じてスーパークラスのコードと協調します。 クラスは、静的なメソッドやフィールド、イニシャライザ、等々を持つことができます。

ものごとを単純なまま進めるために、これらの問題を扱うことはしません。 実際、これ以上オブジェクトやクラスについて話すことはありません。 (もし興味があるなら、 Types and Programming Languages にたくさんの議論があります。) その代わり、STLCの単純化された設定のもとで、 サブクラス/サブインターフェース関係の背後にある核となる概念について学習します。

包摂規則

この章のゴールは(直積を持つ)単純型付きラムダ計算にサブタイプを追加することです。 これは2つのステップから成ります:

• 型の間の二項サブタイプ関係(subtype relation)を定義します。
  
  
• 型付け関係をサブタイプを考慮した形に拡張します。

2つ目のステップは実際はとても単純です。型付け関係にただ1つの規則だけを追加します。 その規則は、包摂規則(rule of subsumption)と呼ばれます:
                         Γ ⊢ t : S S <: T
                         ------------------------- (T_Sub)
                               Γ ⊢ t : T

この規則は、直観的には、項について知っている情報のいくらかを「忘れる」ことができると言っています。

例えば、tが2つのフィールドを持つレコード(例えば、S = {x:A→A, y:B→B})で、 フィールドの1つを忘れることにした(T = {y:B→B})とします。 するとtを、1フィールドのレコードを引数としてとる関数に渡すことができるようになります。

サブタイプ関係

最初のステップ、関係 S <: T の定義にすべてのアクションがあります。 定義のそれぞれを見てみましょう。

直積型

最初に、直積型です。ある一つの対が他の対より「良い」とは、 それぞれの成分が他の対の対応するものより良いことです。
                            S1 <: T1 S2 <: T2
                            -------------------- (S_Prod)
                               S1*S2 <: T1*T2

関数型

次の型を持つ2つの関数fとgがあるとします：

       f : C -> {x:A,y:B}
       g : (C->{y:B}) -> D

つまり、fは型{x:A,y:B}のレコードを引数とする関数であり、 gは引数として、型{y:B}のレコードを引数とする関数をとる高階関数です。 (そして、レコードのサブタイプについてはまだ議論していませんが、 {x:A,y:B} は {y:B} のサブタイプであるとします。) すると、関数適用 g f は、両者の型が正確に一致しないにもかかわらず安全です。 なぜなら、gがfについて行うことができるのは、 fを(型Cの)ある引数に適用することだけだからです。 その結果は実際には2フィールドのレコードになります。 ここでgが期待するのは1つのフィールドを持つレコードだけです。 しかしこれは安全です。なぜならgがすることができるのは、 わかっている1つのフィールドを射影することだけで、 それは存在する2つのフィールドの1つだからです。

この例から、関数型のサブタイプ規則が以下のようになるべきということが導かれます。 2つの関数型がサブタイプ関係にあるのは、その結果が次の条件のときです:
                                  S2 <: T2
                              ---------------- (S_Arrow2)
                              S1→S2 <: S1→T2

これを一般化して、2つの関数型のサブタイプ関係を、引数の条件を含めた形にすることが、同様にできます:
                            T1 <: S1 S2 <: T2
                            -------------------- (S_Arrow)
                              S1→S2 <: T1→T2

ここで注意するのは、引数の型はサブタイプ関係が逆向きになることです。 S1→S2 が T1→T2 のサブタイプであると結論するためには、 T1がS1のサブタイプでなければなりません。 関数型のコンストラクタは最初の引数について反変(contravariant)であり、 二番目の引数について共変(covariant)であると言います。

直観的には、型S1→S2の関数fがあるとき、fは型S1の要素を引数にとることがわかります。 明らかにfはS1の任意のサブタイプT1の要素をとることもできます。 fの型は同時にfが型S2の要素を返すことも示しています。 この値がS2の任意のスーパータイプT2に属することも見ることができます。 つまり、型S1→S2の任意の関数fは、型T1→T2を持つと見ることもできるということです。

Top

サブタイプ関係の最大要素を定めることは自然です。他のすべての型のスーパータイプであり、 すべての(型付けできる)値が属する型です。このために言語に新しい一つの型定数Topを追加し、 Topをサブタイプ関係の他のすべての型のスーパータイプとするサブタイプ規則を定めます:
                                   -------- (S_Top)
                                   S <: Top

Top型はJavaやC#におけるObject型に対応するものです。

構造規則

サブタイプ関係の最後に、2つの「構造規則」("structural rules")を追加します。 これらは特定の型コンストラクタからは独立したものです。 推移律(rule of transitivity)は、直観的には、 SがUよりも良く、UがTよりも良ければ、SはTよりも良いというものです...
                              S <: U U <: T
                              ---------------- (S_Trans)
                                   S <: T

... そして反射律(rule of reflexivity)は、 任意の型はそれ自身と同じ良さを持つというものです。
                                   ------ (S_Refl)
                                   T <: T

レコード

レコード型のサブタイプは何でしょうか？

レコード型のサブタイプについての基本的直観は、 「より小さな」レコードの場所で「より大きな」レコードを使うことは常に安全だということです。 つまり、レコード型があるとき、さらにフィールドを追加したものは常にサブタイプになるということです。 もしあるコードがフィールドxとyを持つレコードを期待していたとき、 レコードx、y、zを持つレコードを受けとることは完璧に安全です。 zフィールドは単に無視されるだけでしょう。 例えば次の通りです。

       {x:Nat,y:Bool} <: {x:Nat}
       {x:Nat} <: {}

これはレコードの"width subtyping"(幅サブタイプ)として知られます。

レコードの1つのフィールドの型をそのサブタイプで置き換えることでも、 レコードのサブタイプを作ることができます。 もしあるコードが型Tのフィールドxを持つレコードを待っていたとき、 型Sが型Tのサブタイプである限りは、 型Sのフィールドxを持つレコードが来ることはハッピーです。 例えば次の通りです。

       {a:{x:Nat}} <: {a:{}}

これは"depth subtyping"(深さサブタイプ)として知られています。

最後に、レコードのフィールドは特定の順番で記述されますが、その順番は実際には問題ではありません。 例えば次の通りです。

       {x:Nat,y:Bool} <: {y:Bool,x:Nat}

これは"permutation subtyping"(順列サブタイプ)として知られています。

これらをレコードについての単一のサブタイプ規則に形式化することをやってみましょう。 次の通りです:
                        for each jk in j1..jn,
                    ∃ ip in i1..im, such that
                          jk=ip and Sp <: Tk
                  ---------------------------------- (S_Rcd)
                  {i1:S1...im:Sm} <: {j1:T1...jn:Tn}

つまり、左のレコードは(少なくとも)右のレコードのフィールドラベルをすべて持ち、 両者で共通するフィールドはサブタイプ関係になければならない、ということです。 しかしながら、この規則はかなり重くて読むのがたいへんです。 ここでは、3つのより簡単な規則に分解します。この3つはS_Transを使うことで結合することができ、 同じ作用をすることができます。

最初に、レコード型の最後にフィールドを追加したものはサブタイプになります:
                               n > m
                 --------------------------------- (S_RcdWidth)
                 {i1:T1...in:Tn} <: {i1:T1...im:Tm}

S_RcdWidthを使うと、複数のフィールドを持つレコードについて、 前方のフィールドを残したまま後方のフィールドを落とすことができます。 この規則で例えば {y:B, x:A} <: {y:B} が示されます。

二つ目に、レコード型の構成要素の内部にサブタイプ規則を適用できます:
                       S1 <: T1 ... Sn <: Tn
                  ---------------------------------- (S_RcdDepth)
                  {i1:S1...in:Sn} <: {i1:T1...in:Tn}

例えば S_RcdDepthとS_RcdWidthを両方使って {y:{z:B}, x:A} <: {y:{}} を示すことができます。

三つ目に、フィールドの並べ替えを可能にする必要があります。 念頭に置いてきた例は {x:A,y:B} <: {y:B} でした。 これはまだ達成されていませんでした。 S_RcdDepthとS_RcdWidthだけでは、レコード型の「後」からフィールドを落とすことしかできません。 これから次の規則が必要です:
         {i1:S1...in:Sn} is a permutation of {i1:T1...in:Tn}
         --------------------------------------------------- (S_RcdPerm)
                  {i1:S1...in:Sn} <: {i1:T1...in:Tn}



さらなる例です:

• {x:A,y:B} <: {y:B,x:A}.
• {}->{j:A} <: {k:B}->Top
• Top->{k:A,j:B} <: C->{j:B}

なお、実際の言語ではこれらのサブタイプ規則のすべてを採用しているとは限らないことは、 注記しておくべきでしょう。例えばJavaでは:

• サブクラスではスーパークラスのメソッドの引数または結果の型を変えることはできません (つまり、depth subtypingまたは関数型サブタイプのいずれかができないということです。 どちらかは見方によります)。
  
  
• それぞれのクラスは(直上の)スーパークラスを1つだけ持ちます(クラスの「単一継承」 ("single inheritance")です)。
  
  
  • 各クラスのメンバー(フィールドまたはメソッド)は1つだけインデックスを持ち、 サブクラスでメンバーが追加されるたびに新しいインデックスが「右に」追加されます (つまり、クラスには並び換えがありません)。
    
    
• クラスは複数のインターフェースをインプリメントできます。これは インターフェースの「多重継承」("multiple inheritance")と呼ばれます (つまり、インターフェースには並び換えがあります)。

直積と Top によるレコード (optional)

これらすべてをどのように形式化するかは、レコードとその型をどのように形式化するかに、 まさに依存しています。もしこれらを核言語の一部として扱うならば、 そのためのサブタイプ規則を書き下す必要があります。 ファイルRecordSub_J.vで、この拡張がどのようにはたらくかを示します。

一方、もしそれらをパーサで展開される派生形として扱うならば、新しい規則は何も必要ありません。 直積とUnit型のサブタイプについての既存の規則が、 このエンコードによるレコードのサブタイプに関する妥当な規則になっているかをチェックすれば良いだけです。 このために、前述のエンコードをわずかに変更する必要があります。 組のエンコードのベースケースおよびレコードのエンコードの "don't care" プレースホルダとして、 Unitの代わりにTopを使います。 すると:

    {a:Nat, b:Nat} ----> {Nat,Nat}       つまり (Nat,(Nat,Top))
    {c:Nat, a:Nat} ----> {Nat,Top,Nat}   つまり (Nat,(Top,(Nat,Top)))

レコード値のエンコードは何も変更しません。 このエンコードで上述のサブタイプ規則が成立することをチェックするのは容易です (そしてタメになります)。この章の残りでは、このアプローチを追求します。

中核部の定義

STLCに必要となる重要な拡張を既に概観してきました: (1)サブタイプ関係を追加し、(2)型関係に包摂規則を拡張することです。 すべてがスムースにいくように、前の章の表現にいくらかの技術的改善を行います。 定義の残りは -- 特に言語の構文と操作的意味は -- 前の章で見たものと同じです。 最初に同じ部分をやってみましょう。

構文

よりおもしろい例のために、純粋STLCに非常に小さな拡張を行います。 String、Person、Window等のような、任意の「基本型」の集合を追加します。 これらの型の定数を追加したり、その型の上の操作を追加したりすることをわざわざやりませんが、 そうすることは簡単です。

この章の残りでは、基本型、ブール型、関数型、UnitとTopのみ形式化し、 直積型は練習問題にします。

包摂

包摂の定義は、いつものSTLCと同様です。

簡約

value(値)の定義やstep関係の定義と同様です。

サブタイプ

さて、おもしろい所にやって来ました。サブタイプ関係の定義から始め、その重要な技術的性質を調べます。

定義

サブタイプの定義は、動機付けの議論のところで概観した通りです。

なお、基本型については特別な規則は何ら必要ありません。 基本型は自動的に(S_Reflより)自分自身のサブタイプであり、 (S_Topより)Topのサブタイプでもあります。そしてこれが必要な全てです。

サブタイプの例と練習問題

練習問題: ★★, optional (subtyping judgements)

(この練習問題は、少なくともファイルのここまでに、直積型を言語に追加した後で行ってください。)

レコードを対でエンコードするときに、以下のレコード型を表す直積型を定義しなさい。
    Person := { name : String }
    Student := { name : String ;
                  gpa : Float }
    Employee := { name : String ;
                  ssn : Integer }

☐

以下の事実のほとんどは、Coqで証明するのは簡単です。 練習問題の効果を十分に得るために、 どうやって証明するか自分が理解していることを紙に証明を書いて確認しなさい。

練習問題: ★, optional (subtyping_example_1)

☐

練習問題: ★, optional (subtyping_example_2)

☐

練習問題: ★, optional (subtype_instances_tf_1)

型S、T、U、Vがあり S <: T かつ U <: V とします。 このとき以下のサブタイプ関係の主張のうち、正しいものはどれでしょうか？ それぞれの後に「真」または「偽」と書きなさい。 (ここで、A、B、Cは基本型とします。)

• T→S <: T→S
  
  
• Top→U <: S→Top
  
  
• (C→C) → (A*B) <: (C→C) → (Top*B)
  
  
• T→T→U <: S→S→V
  
  
• (T→T)->U <: (S→S)->V
  
  
• ((T→S)->T)->U <: ((S→T)->S)->V
  
  
• S*V <: T*U

☐

練習問題: ★ (subtype_instances_tf_2)

以下の主張のうち正しいものはどれでしょうか？ それぞれについて「真」または「偽」と書きなさい。
      ∀ S T,
          S <: T →
          S→S <: T→T

      ∀ S T,
           S <: A→A →
           ∃ T,
              S = T→T ∧ T <: A

      ∀ S T1 T1,
           S <: T1 → T2 →
           ∃ S1 S2,
              S = S1 → S2 ∧ T1 <: S1 ∧ S2 <: T2

      ∃ S,
           S <: S→S

      ∃ S,
           S→S <: S

      ∀ S T2 T2,
           S <: T1*T2 →
           ∃ S1 S2,
              S = S1*S2 ∧ S1 <: T1 ∧ S2 <: T2

☐

練習問題: ★ (subtype_concepts_tf)

以下のうち真であるものはどれで、偽であるものはどれでしょうか？

• 他のすべての型のスーパータイプである型がある。
  
  
• 他のすべての型のサブタイプである型がある。
  
  
• 他のすべての対型のスーパータイプである対型がある。
  
  
• 他のすべての対型のサブタイプである対型がある。
  
  
• 他のすべての関数型のスーパータイプである関数型がある。
  
  
• 他のすべての関数型のサブタイプである関数型がある。
  
  
• サブタイプ関係による、同一型を含まない無限降鎖(infinite descending chain)がある。 つまり型の無限列S0、S1、... があり、すべてのSiは異なり、 そして各S(i+1)はS(i)のサブタイプである。
  
  
• サブタイプ関係による、同一型を含まない無限昇鎖(infinite ascending chain)がある。 つまり型の無限列S0、S1、... があり、すべてのSiは異なり、 そして各S(i+1)はS(i)のスーパータイプである。

☐

練習問題: ★★ (proper_subtypes)

次の主張は真でしょうか偽でしょうか？自分の答えを簡単に説明しなさい。
    ∀ T,
         ~(∃ n, T = ty_base n) →
         ∃ S,
            S <: T ∧ S <> T

☐

練習問題: ★★ (small_large_1)

• 次の表明を真にする最小の型Tは何でしょうか？ (ここで「最小」とはサブタイプ関係においてです。)
         empty ⊢ (\p:T*Top. p.fst) ((\z:A.z), unit) : A→A
  
  
  
  
• 同じ表明を真にする最大の型Tは何でしょうか？

☐

練習問題: ★★ (small_large_2)

• 次の表明を真にする最小の型Tは何でしょうか？
         empty ⊢ (\p:(A→A * B→B). p) ((\z:A.z), (\z:B.z)) : T
  
  
  
  
• 同じ表明を真にする最大の型Tは何でしょうか？

☐

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

• 次の表明を真にする最小の型Tは何でしょうか？
         a:A ⊢ (\p:(A*T). (p.snd) (p.fst)) (a , \z:A.z) : A
  
  
  
  
• 同じ表明を真にする最大の型Tは何でしょうか？

☐

練習問題: ★★ (small_large_4)

• 次の表明を真にする最小の型Tは何でしょうか？
         ∃ S,
           empty ⊢ (\p:(A*T). (p.snd) (p.fst)) : S
  
  
  
  
• 同じ表明を真にする最大の型Tは何でしょうか？

☐

練習問題: ★★ (smallest_1)

次の表明を真にする最小の型Tは何でしょうか？
      ∃ S, ∃ t,
        empty ⊢ (\x:T. x x) t : S

☐

練習問題: ★★ (smallest_2)

次の表明を真にする最小の型Tは何でしょうか？
      empty ⊢ (\x:Top. x) ((\z:A.z) , (\z:B.z)) : T

☐

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

レコード型 {x:A, y:C→C} はいくつのスーパータイプを持つでしょうか？ つまり、いくつの異なる型Tが {x:A, y:C→C} <: T を満たすでしょうか? (ここで、2つの型が異なるとは、その記述が異なることとします。 たとえ両者が相互にサブタイプであってもです。 例えば、{x:A,y:B} と {y:B,x:A} は異なります。)

☐

型付け

型付け関係の変更は、包摂規則 T_Sub の追加だけです。

型付けの例

以下の練習問題は言語に直積を追加した後に行いなさい。 それぞれの非形式的な型付けジャッジメントについて、Coqで形式的主張を記述し、 それを証明しなさい。

練習問題: ★, optional (typing_example_0)

☐

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

☐

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

☐

性質

チェックしたいシステムの根本的性質はいつもと同じく、進行と保存です。 STLCに参照を拡張したものとは違い、サブタイプを考慮しても、これらの主張を変化させる必要はありません。 ただし、それらの証明はもうちょっと複雑になります。

サブタイプの反転補題(Inversion Lemmas)

型付け関係の性質を見る前に、サブタイプ関係の2つの重要な構造的性質を記しておかなければなりません:

• BoolはBoolの唯一のサブタイプです
• 関数型のすべてのサブタイプは関数型です

これらは反転補題(inversion lemmas)と呼ばれます。これは、後の証明でもともとの inversionタクティックと同じ役目をするためです。 つまり、サブタイプ関係の主張 S <: T の導出が存在するという仮定と、 SやTの形についてのいくつかの制約が与えられたとき、 それぞれの補題は、SとTの形、および両者の構成要素間のサブタイプ関係の存在について、 より多くのことが言えるためには、 S <: T の導出がどういう形でなければならないかを提示するからです。

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

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

☐

正準形(Canonical Forms)

最初に、進行定理の証明はそれほど変わらないことを見ます。 1つだけ小さなリファインメントが必要です。 問題となる項が関数適用 t1 t2 でt1とt2が両方とも値の場合を考えるとき、 t1がラムダ抽象の形をしており、 そのためST_AppAbs簡約規則が適用できることを確認する必要があります。 もともとのSTLCでは、これは明らかです。 t1が関数型T11→T12を持ち、また、関数型の値を与える規則が1つだけ、 つまり規則T_Absだけであり、そしてこの規則の結論部の形から、 t1は関数型にならざるを得ない、ということがわかります。

サブタイプを持つSTLCにおいては、この推論はそのままうまく行くわけではありません。 その理由は、値が関数型を持つことを示すのに使える規則がもう1つあるからです。 包摂規則です。幸い、このことが大きな違いをもたらすことはありません。 もし Γ ⊢ t1 : T11→T12 を示すのに使われた最後の規則が包摂規則だった場合、 導出のその前の部分で、同様にt1が主部(項の部分)である導出があり、 帰納法により一番最初にはT_Absが使われたことが推論できるからです。

推論のこの部分は次の補題にまとめられています。この補題は、関数型の可能な正準形 ("canonical forms"、つまり値)を示します。

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

☐

同様に、型Boolの正準形は定数trueとfalseです。

進行

進行性の証明は純粋なSTLCとほぼ同様に進みます。ただ何箇所かで正準形補題を使うことを除けば...

「定理」(進行): 任意の項tと型Tについて、 もし empty ⊢ t : T ならばtは値であるか、ある項t'について t ⇒ t' である。

「証明」:tとTが与えられ、empty ⊢ t : T とする。 型付けの導出についての帰納法で進める。

(最後の規則が)T_Abs、T_Unit、T_True、T_Falseのいずれかの場合は、 自明である。なぜなら、関数抽象、unit、true、falseは既に値だからである。 T_Varであることはありえない。なぜなら、変数は空コンテキストで型付けできないからである。 残るのはより興味深い場合である:

• 型付け導出の最後のステップで規則T_Appが使われた場合、 項t1、t2と型T1、T2が存在して t = t1 t2、T = T2、 empty ⊢ t1 : T1 → T2、empty ⊢ t2 : T1 となる。 さらに帰納法の仮定から、t1は値であるかステップを進めることができ、 t2も値であるかステップを進めることができる。 このとき、3つの場合がある:
  
  
  • ある項 t1' について t1 ⇒ t1' とする。このときST_App1より t1 t2 ⇒ t1' t2 である。
    
    
  • t1が値であり、ある項t2'について t2 ⇒ t2' とする。 このとき規則ST_App2より t1 t2 ⇒ t1 t2' となる。なぜなら t1が値だからである。
    
    
  • 最後にt1とt2がどちらも値とする。補題canonical_forms_for_arrow_types より、t1はあるx、S1、s2について\x:S1.s2という形である。 しかしするとt2が値であることから、 ST_AppAbsより (\x:S1.s2) t2 ⇒ [t2/x]s2 となる。
    
    
• 導出の最後のステップで規則T_Ifが使われた場合、項t1、t2、t3があって t = if t1 then t2 else t3 となり、 empty ⊢ t1 : Bool かつ empty ⊢ t2 : T かつ empty ⊢ t3 : T である。 さらに、帰納法の仮定よりt1は値であるかステップを進めることができる。
  
  
  • もしt1が値ならば、ブール値についての正準形補題より t1 = true または t1 = false である。どちらの場合でも、規則ST_IfTrueまたはST_IfFalse を使うことによってtはステップを進めることができる。
    
    
  • もしt1がステップを進めることができるならば、 規則ST_Ifよりtもまたステップを進めることができる。
    
    
• 導出の最後のステップが規則T_Subによる場合、型Sがあって S <: T かつ empty ⊢ t : S となっている。 求める結果は型付け導出の帰納法の仮定そのものである。

型付けの反転補題

保存定理の証明はサブタイプを追加したことでやはり少し複雑になります。 その理由は、上述の「サブタイプの反転補題」と同様に、純粋なSTLCでは「定義から自明」 であった(したがってinversionタクティックからすぐに得られた)のに、 サブタイプがあることで本当の証明が必要になった、 型付け関係についてのいくつもの事実があるからです。 サブタイプがある場合、同じhas_typeの主張を導出するのに複数の方法があるのです。

以下の「反転補題」("inversion lemma")は、 もし、関数抽象の型付け主張 Γ ⊢ \x:S1.t2 : T の導出があるならば、その導出の中に本体t2の型を与える部分が含まれている、 ということを言うものです。

「補題」: もし Γ ⊢ \x:S1.t2 : T ならば、 型S2が存在して Γ, x:S1 ⊢ t2 : S2 かつ S1 → S2 <: T となる。

(この補題は「Tはそれ自身が関数型である」とは言っていないことに注意します。 そうしたいところですが、それは成立しません!)

「証明」:Γ、x、S1、t2、Tを補題の主張に記述された通りとする。 Γ ⊢ \x:S1.t2 : T の導出についての帰納法で証明する。 T_VarとT_Appの場合はあり得ない。 これらは構文的に関数抽象の形の項に型を与えることはできないからである。

• 導出の最後のステップ使われた規則がT_Absの場合、型T12が存在して T = S1 → T12 かつ Γ,x:S1 ⊢ t2 : T12 である。 S2としてT12をとると、S_Reflより S1 → T12 <: S1 → T12 となり、 求める性質が成立する。
  
  
• 導出の最後のステップ使われた規則がT_Subの場合、型Sが存在して S <: T かつ Γ ⊢ \x:S1.t2 : S となる。 型付け導出の帰納仮定より、型S2が存在して S1 → S2 <: S かつ Γ, x:S1 ⊢ t2 : S2 である。 このS2を採用すれば、 S1 → S2 <: T であるからS_Transより求める性質が成立する。

同様に...

型付けについての反転補題と関数型の間のサブタイプの反転補題は「結合補題」 ("combination lemma")としてまとめることができます。 この補題は以下で実際に必要になるものを示します。

コンテキスト不変性

コンテキスト不変性補題は、純粋のSTLCと同じパターンをとります。

置換

置換補題(substitution lemma)は純粋なSTLCと同じ流れで証明されます。 唯一の大きな変更点は、いくつかの場所で、 部分項が型を持つことについての仮定から構造的情報を抽出するために、 Coqのinversionタクティックを使う代わりに上で証明した反転補題を使うことです。

保存

(型の)保存の証明は以前の章とほとんど同じです。適切な場所で置換補題を使い、 型付け仮定から構造的情報を抽出するために上述の反転補題をまた使います。

「定理」(保存)： t、t'が項でTが型であり、empty ⊢ t : T かつ t ⇒ t' ならば、empty ⊢ t' : T である。

「証明」:t と T が empty ⊢ t : T であるとする。 証明は、t'を特化しないまま型付け導出の構造に関する帰納法で進める。 (最後の規則が)T_Abs、T_Unit、T_True、T_Falseの場合は考えなくて良い。 なぜなら関数抽象と定数はステップを進めないからである。 T_Varも考えなくて良い。なぜならコンテキストが空だからである。

• もし導出の最後のステップの規則がT_Appならば、 項t1 t2 と型 T1 T2 が存在して、t = t1 t2、T = T2、 empty ⊢ t1 : T1 → T2、empty ⊢ t2 : T1 である。
  
  ステップ関係の定義から、t1 t2 がステップする方法は3通りである。 ST_App1とST_App2の場合、 型付け導出の帰納仮定とT_Appより求める結果がすぐに得られる。
  
  t1 t2 のステップが ST_AppAbs によるとする。 するとある型Sと項t12について t1 = \x:S.t12 であり、かつ t' = [t2/x]t12 である。
  
  補題abs_arrowより、T1 <: S かつ x:S1 ⊢ s2 : T2 となる。 すると置換補題(substitution_preserves_typing)より、 empty ⊢ [t2/x]t12 : T2 となるがこれが求める結果である。
  
  
  • もし導出の最後のステップで使う規則がT_Ifならば、 項t1、t2、t3が存在して t = if t1 then t2 else t3 かつ empty ⊢ t1 : Bool かつ empty ⊢ t2 : T かつ empty ⊢ t3 : T となる。さらに帰納法の仮定より、もしt1がステップしてt1'に進むならば empty ⊢ t1' : Bool である。 t ⇒ t' を示すために使われた規則によって、3つの場合がある。
    
    
    • t ⇒ t' が規則ST_Ifによる場合、 t' = if t1' then t2 else t3 かつ t1 ⇒ t1' となる。 帰納法の仮定より empty ⊢ t1' : Bool となり、 これからT_Ifより empty ⊢ t' : T となる。
      
      
    • t ⇒ t' が規則ST_IfTrueまたはST_IfFalseによる場合、 t' = t2 または t' = t3 であり、仮定から empty ⊢ t' : T となる。
      
      
• もし導出の最後のステップで使う規則がT_Subならば、 型Sが存在して S <: T かつ empty ⊢ t : S となる。 型付け導出についての帰納法の仮定とT_Subの適用から結果がすぐに得られる。 ☐

型付けの練習問題

練習問題: ★★ (variations)

この問題の各部分は、Unitとサブタイプを持つSTLCの定義を変更する別々の方法を導きます。 (これらの変更は累積的ではありません。各部分はいずれも元々の言語から始まります。) 各部分について、(進行、保存の)性質のうち偽になるものをリストアップしなさい。 偽になる性質について、反例を示しなさい。

• 次の型付け規則を追加する:
                              Γ ⊢ t : S1→S2
                      S1 <: T1 T1 <: S1 S2 <: T2
                      ----------------------------------- (T_Funny1)
                              Γ ⊢ t : T1→T2
  
  
  
  
• 次の簡約規則を追加する:
                               ------------------ (ST_Funny21)
                               unit ⇒ (\x:Top. x)
  
  
  
  
• 次のサブタイプ規則を追加する:
                                 -------------- (S_Funny3)
                                 Unit <: Top→Top
  
  
  
  
• 次のサブタイプ規則を追加する:
                                 -------------- (S_Funny4)
                                 Top→Top <: Unit
  
  
  
  
• 次の評価規則を追加する:
                               ----------------- (ST_Funny5)
                               (unit t) ⇒ (t unit)
  
  
  
  
• 上と同じ評価規則と新たな型付け規則を追加する:
                               ----------------- (ST_Funny5)
                               (unit t) ⇒ (t unit)
  
                             ---------------------- (T_Funny6)
                             empty ⊢ Unit : Top→Top
  
  
  
  
• 関数型のサブタイプ規則を次のものに変更する:
                            S1 <: T1 S2 <: T2
                            ----------------------- (S_Arrow')
                                 S1→S2 <: T1→T2
  
  

☐

練習問題: 直積の追加

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

定義したシステムに対、射影、直積型を追加することは比較的簡単な問題です。 次の拡張を行いなさい:

• tyとtmの定義に、対のコンストラクタ、第1射影、第2射影、直積型を追加しなさい。 (ty_casesとtm_casesに対応する場合を追加することを忘れないこと。)
  
  
• 自明な方法で、well-formedness 関係を拡張しなさい。
  
  
• 操作的意味に前の章と同様の簡約規則を拡張しなさい。
  
  
• サブタイプ関係に次の規則を拡張しなさい:
                          S1 <: T1 S2 <: T2
                          --------------------- (Sub_Prod)
                            S1 * S2 <: T1 * T2
  
  
• 型付け関係に、前の章と同様の、対と射影の規則を拡張しなさい。
  
  
• 進行および保存の証明、およびそのための補題を、 新しい構成要素を扱うように拡張しなさい。 (完全に新しいある補題を追加する必要もあるでしょう。) ☐