単純型付きラムダ計算

単純型付きラムダ計算(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. x
  
  2つのブール値をとり、最初のものを返す2引数関数。 (なお、Coqと同様、2引数関数は、実際には本体が1引数関数である1引数関数です。)
  
  
• (\x:Bool. \y:Bool. x) false true
  
  2つのブール値をとり、最初のものを返す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 を持ちます。

構文

型

項

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

いくつかの例...

idB = \a:Bool. a

idBB = \a:Bool→Bool. a

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

k = \a:Bool. \b:Bool. 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関係は常に閉じた(自由変数を持たない)項だけを対象とするからです。

自由変数と置換

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

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

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

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

• [true / a] (if a then a else false) は if true then true else false となります。
  
  
• [true / a] a は true となります。
  
  
• [true / a] (if a then a else b) は if true then true else b となります。
  
  
• [true / a] b は b となります。
  
  
• [true / a] false は false となります(何もしない置換です)。
  
  
• [true / a] (\y:Bool. if y then a else false) は \y:Bool. if y then true else false となります。
  
  
• [true / a] (\y:Bool. a) は \y:Bool. true となります。
  
  
• [true / a] (\y:Bool. y) は \y:Bool. y となります。
  
  
• [true / a] (\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

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

技術的注釈: 置換は、もし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'

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

形式的には:

例

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

練習問題: ★★ (step_example3)

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

☐

型付け

コンテキスト

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

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

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

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

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

型付け関係

非形式的に:
                             Γ x = T
                            -------------- (T_Var)
                            Γ ⊢ x : T

                      Γ , x:T11 ⊢ t12 : T12
                     ---------------------------- (T_Abs)
                     Γ ⊢ \x:T11.t12 : T11→T12

                        Γ ⊢ t1 : T11→T12
                          Γ ⊢ t2 : T11
                        ---------------------- (T_App)
                         Γ ⊢ t1 t2 : T12

                         -------------------- (T_True)
                         Γ ⊢ true : Bool

                        --------------------- (T_False)
                        Γ ⊢ false : Bool

       Γ ⊢ t1 : Bool Γ ⊢ t2 : T Γ ⊢ t3 : T
       -------------------------------------------------------- (T_If)
                  Γ ⊢ if t1 then t2 else t3 : T

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

例

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

非形式的に書くと
     empty ⊢ \a:A. \b:A→A. b (b a))
           : A → (A→A) → A.

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

練習問題: ★★, optional

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

☐

練習問題: ★★ (typing_example_3)

次の型付けが成立することを形式的に証明しなさい:
   empty ⊢ (\a:Bool→B. \b:Bool→Bool. \c:Bool.
               b (a c))
         : T.

☐

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

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

練習問題: ★★★ (typing_nonexample_3)

別の型を持たない例:
    ~ (∃ S, ∃ T,
          empty ⊢ (\a:S. a a) : T).

☐

練習問題: ★ (typing_statements)

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

• b:Bool ⊢ \a:Bool.a : Bool→Bool
  
  
• ∃ T, empty ⊢ (\b:Bool→Bool. \a:Bool. b a) : T
  
  
• ∃ T, empty ⊢ (\b:Bool→Bool. \a:Bool. a b) : T
  
  
• ∃ S, a:S ⊢ (\b:Bool→Bool. b) a : S
  
  
• ∃ S, ∃ T, a:S ⊢ (a a a) : T

☐

練習問題: ★, optional (more_typing_statements)

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

• ∃ T, empty ⊢ (\b:B→B→B. \a:B, b a) : T
  
  
• ∃ T, empty ⊢ (\a:A→B, \b:B-->C, \c:A, b (a c)):T
  
  
• ∃ S, ∃ U, ∃ T, a:S, b:U ⊢ \c:A. a (b c) : T
  
  
• ∃ S, ∃ T, a:S ⊢ \b:A. a (a b) : T
  
  
• ∃ S, ∃ U, ∃ 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 においては自由に現れる変数はありません。

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

置換

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

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

• 最後の規則が afi_var の場合、t = x である。そして、tがΓ で型付けされるという仮定から、そのまま、Γでxに型付けされることが言える。
  
  
• 最後の規則が afi_app1 の場合、t = t1 t2 でxはt1に自由に出現する。 tがΓのもとで型付けされることから、型付け規則からt1も型付けされることになる。 従って帰納仮定よりΓはxに型を付ける。
  
  
• 他のほとんどの場合も同様である。xがtの部分項に自由に現れ、 tがΓで片付けされることから、xが出現しているtの部分項は同様にΓ で型付けされる。従って帰納仮定より求めるべき結果が得られる。
  
  
• 残るのは、最後の規則が afi_abs の場合だけである。この場合、 t = \y:T11.t12 でxはt12に自由に現れる。 またxはyと異なっている。前の場合との違いは、 tはΓのもとで型付けされているが、 その本体t12は (Γ, y:T11) のもとで型付けされているという点である。 このため、帰納仮定は、拡張されたコンテキスト (Γ, y:T11) でx に型付けされる、という主張になる。 Γのもとでxに型が付けられるという結論を得るため、 xとyが異なっているという点に注意して、補題extend_neqを使う。

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

練習問題: ★★ (typable_empty__closed)

☐

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

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

• 導出の最後の規則がT_Varのとき、t = x かつ Γ x = T である。 仮定から Γ' x = T であるから、T_Var より Γ' ⊢ t : T となる。
  
  
• 最後の規則が T_Abs のとき、t = \y:T11. t12 かつ T = T11 → T12 かつ Γ, y:T11 ⊢ t12 : T12 である。 帰納法の仮定は、任意のコンテキストGamma''について、 もし Γ, y:T11 と Gamma'' が t12 内のすべての自由変数に同じ型を割り当てるならば、 t12 は Gamma'' のもとで型T12を持つ、である。 Γ'を、t内の自由変数についてΓ と同じ割当てをするコンテキストとする。 示すべきことは Γ' ⊢ \y:T11. t12 : T11 → T12 である。
  
  T_Abs より、Γ', y:T11 ⊢ t12 : T12 を示せば十分である。 帰納仮定(ただし Gamma'' = Γ', y:T11 とする)より、 Γ, y:T11 と Γ', y:T11 が t12内に自由に現れるすべての変数について割当てが一致することを示せば十分である。
  
  t12に自由に出現する任意の変数はyであるか、それ以外の変数かである。 Γ, y:T11 と Γ', y:T11 は明らかにyについては一致する。 それ以外の場合、t12に自由に出現するy以外の任意の変数は t = \y:T11. t12 にも自由に現れることに注意すると、Γ と Γ' がそのような変数について割当てが一致するという仮定より、 Γ, y:T11 と Γ', y:T11 も一致する。
  
  
• 最後の規則が T_App の場合、t = t1 t2 かつ Γ ⊢ t1 : T2 → T かつ Γ ⊢ t2 : T2 である。 帰納法の仮定の1つは、すべてのコンテキストΓ'について、 Γ'とΓがt1のすべての自由変数について同じ割当てをするならば、 Γ'のもとでt1は型 T2 → T を持つ、となる。 t2についても同様の帰納仮定がある。 証明すべきことは、Γ'がΓと t1 t2 のすべての自由変数について同一の割当てをするという仮定の上で、 Γ'のもとでも t1 t2 が型Tを持つ、ということである。 T_Appより、t1 と t2 がそれぞれ Γ'とΓのもとで同じ型を持つことを示せば十分である。 しかし、t1のすべての自由変数は t1 t2 でも自由変数であり、 t2の自由変数についても同様である。ゆえに、2つの帰納仮定から求める結果が得られる。

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

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

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

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

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

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

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

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

保存

さて、(型の)保存(preservation)を証明する道具立ては揃いました。 保存とは、閉じた項tが型Tを持ち、t'への評価ステップを持つならば、 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でステップする。このとき、 帰納法の仮定から直接求める結果が得られる。

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

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

☐

進行

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

「証明」: ⊢ 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もステップを進むことができる。

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

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

☐

型の一意性

練習問題: ★★★ (types_unique)

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

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

☐

さらなる練習問題

練習問題: ★ (progress_preservation_statement)

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

☐

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

STLCの評価関係に次の新しい規則を加えたとします:
      | T_Strange : ∀ x t,
           has_type empty (tm_abs x Bool t) Bool

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

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

☐

練習問題: ★★ (stlc_variation2)

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

☐

練習問題: 算術を持つSTLC

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

構文と操作的意味

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

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

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

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

• STLCについてここまでやってきたこと(定義から進行定理まで)の全体をコピーして、 ファイルのこの部分にペーストしなさい。
  
  
• subst操作とstep関係の定義を拡張して、算術の操作の適切な節を含むようにしなさい。
  
  
• オリジナルのSTLCの性質の証明を拡張して、新しい構文を扱うようにしなさい。 Coq がその証明を受理することを確認しなさい。

☐