このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

型付きラムダ計算 構文論 再入門 2/2: カリー/ハワード対応のために

型付きラムダ計算 構文論 再入門 1/2: カリー/ハワード対応のために」の続きです。

前回 1/2 の内容:

  1. 予備知識と参考資料
  2. 大きなラムダ計算とは何か
  3. 概要と目標
  4. 集合と写像に関する基礎的事項
  5. 型システム

今回 2/2 の内容:

疑似ラムダ項の構文

ラムダ項の構文を定義したいのですが、まずはザックリとした構文定義をします。ザックリなので、ここでの定義だけでは不十分です。ここで定義される項(構文的な表現)はちゃんとしたラムダ項ではないので疑似ラムダ項(lambda pseudoterm)と呼びます。なお、「ラムダ項」と「ラムダ式」は原則として同義語ですが、小さなラムダ式をラムダ項と呼ぶことが多いです。

変数(と呼ばれる記号)の集合をVarとします。疑似ラムダ項とは次のようなものです(帰納的な定義)。

  1. [変数] xが変数(x∈Var)ならば、x は疑似ラムダ項である。
  2. [ユニット] !は疑似ラムダ項である。
  3. [適用] E, Fが疑似ラムダ項ならば、E▷F は疑似ラムダ項である。
  4. [ペア] E, Fが疑似ラムダ項ならば、(E F) は疑似ラムダ項である。
  5. [第一成分] Eが疑似ラムダ項ならば、E_1 は疑似ラムダ項である。
  6. [第二成分] Eが疑似ラムダ項ならば、E_2 は疑似ラムダ項である。
  7. [関数抽象] xが変数、Aが型、Eが疑似ラムダ項ならば、λx:A.E は疑似ラムダ項である。
  8. [括弧] Eが疑似ラムダ項ならば、(E) (Eを括弧で囲んだ形)は疑似ラムダ項である。
  9. 以上により定義されたものだけが疑似ラムダラムダ項である。

E▷F とまったく同じ意味(別記法)で F・E も使います。'▷'と'・'で左右が逆になりますが、どっちを使うのも自由です。今後'・'を多く使うでしょうが、'▷'のほうが圏論の図式順記法や絵算との相性がいいです。


レヴィ(Paul Blain Levy)によるCBPV(Call-By-Push-Value)の項言語でも、適用の書き方は「引数 適用記号 関数」の語順です。レヴィは適用記号にバックスクォートを使っていました。左から右にデータと制御が流れるイメージですね。「Call-By-Push-Valueの不純な関数型言語」参照。

演算子の優先順位は次のようです。演算子の優先順位に頼ると間違いを犯しやすいので、なるべく丸括弧を使いましょう。

優先順位 演算子 演算子形式 結合性 注意
1 _1, _2 後置単項 なし
2 中置二項
2 中置二項 ▷と左右が逆だが同じ
3 (- -) 中置二項 空白が演算子記号

疑似ラムダ項の例をいくつか挙げます。

  1. x
  2. x▷y
  3. y・x (x▷yと同じ)
  4. (x y)
  5. (! x)
  6. ((x y) z)
  7. x_1
  8. ((x y) z)_2
  9. f・(((x y) z)_2)
  10. λx:A.(f・(((x y) z)_2))

記号のインフォーマルな意味を説明しておきます。正式な意味論を述べるわけではなくて、心理的な納得感・安心感が目的です。

  • [ユニット] !は、単元集合1(型の記号はI)の唯一の要素を表す定数記号だと思ってください。Eが0引数関数を表すとき、E・! として評価します。実際のプログラミング言語では、ユニット定数に()を使うことが多いみたいです。
  • [適用] '▷'と'・'は適用(appとapp')を表す中置演算子記号です。'▷'の右、'・'の左に関数オブジェクト(の表現)を置きます。E▷F の値は、Eの評価結果とFの評価結果である関数オブジェクトをappに渡した結果です。適用の記号を省略することはありません
  • [ペア] 空白は関数のペアを作る中置演算子記号です。書き方はLispのリスト記法と同じです。使い方はLispのドットペア記法と同じになります。空白ペアの意味は、関数のデカルト・ペア、または関数の直積です。空白ペアがデカルトペアを表すか直積を表すかは、型証明系(後述)により変わります。
  • [第一成分][第二成分] E_1は、Eの第一成分を意味します。'_1'自体は、第一成分を取り出す後置演算子です。'_2'も同様です。
  • [関数抽象] λx:A. は、型付き変数xによる関数抽象(ラムダ抽象)で、変数xを仮引数とする関数オブジェクトを作ります。
  • [括弧] 曖昧さを避けたり、優先順位を変えるために丸括弧を使います。

疑似ラムダ項Eの自由変数の集合FreeVar(E)は次のように定義します。

  1. xが変数(x∈Var)ならば、FreeVar(x) = {x}
  2. FreeVar(!) = 空集合
  3. E, Fが疑似ラムダ項ならば、FreeVar(E▷F) = FreeVar(E)∪FreeVar(F)
  4. E, Fが疑似ラムダ項ならば、FreeVar((E F)) = FreeVar(E)∪FreeVar(F)
  5. Eが疑似ラムダ項ならば、FreeVar(E_1) = FreeVar(E)
  6. Eが疑似ラムダ項ならば、FreeVar(E_2) = FreeVar(E)
  7. xが変数、Aが型、Eが疑似ラムダ項ならば、FreeVar(λx:A.E) = FreeVar(E)\{x}
  8. Eが疑似ラムダ項ならば、FreeVar((E)) = FreeVar(E)

FreeVar(E)\{x} は、FreeVar(E)から変数xを(あれば)取り除いた集合です。

疑似ラムダ項に対しても、通常の手順によりアルファ変換(alpha conversion)を行えます。アルファ変換は束縛変数をリネームしますが、自由変数のリネームも同様に行えます(リネームで意図せぬラムダ束縛が生じないように注意)。アルファ変換と自由変数のリネームは似てますが、リネーム対象(束縛変数か自由変数か)が違うので区別してください。

ラムダ項の構成と型付け

x:A, y:B のように、変数ごとの型宣言が並んだものをΓ, Δなどのギリシャ文字大文字で表すことにします。この並びのことも型宣言(type declaration)と呼びます。他に、型環境(type environment)とか型コンテキスト(type context)とか呼ぶこともあります。でも、人によって用語法は異なります→「型理論ってば」。

型宣言Γは、変数:型 の形をカンマで区切って並べたものです。変数が重複してはダメで、すべて異なる変数が出現します。Γは空であってもかまいません。Γに出現する変数の集合をVarSet(Γ)とします。

型宣言Γと疑似ラムダ項Eを組にした〈Γ| E〉 を型宣言付き擬似ラムダ項(type-declared lambda pseudoterm)と呼びます。型宣言付き疑似ラムダ項のなかには、不適切なものが含まれています。適切な項とは、型が確定するものです。項の適切さ=項の型付け可能性を定義するために、型判断というものを導入します。

型宣言付き疑似ラムダ項〈Γ| E〉と型Aを組にした 〈Γ| E〉 :A の形を型判断(type judgement)と呼びます。型判断は、「型宣言Γのもとで、ラムダ項Eの型はAである」という主張です。型判断の書き方を変えて、Γ |- E:A とか Γ ⇒ E:A とするとシーケント計算に繋がります。が、今回はシーケント形式は使いません。シーケント形式でのラムダ計算は次の記事に書いています。ラムダ式の構文や推論規則は今回と微妙に違いますが、本質的な差はありません。

最初から正しいと認める型判断を公理型判断(axiom type judgement)、型公理(type axiom)、あるいは混乱の心配がなければ単に公理(axiom)と呼びます。以下に公理型判断のパターンを列挙します。

  • [変数] Γのなかに x:A が含まれるならば、〈Γ| x〉:A は公理である。
  • [ユニット] 〈Γ| !〉:I は公理である。Γは任意で、空でもよい

型推論規則(type inference rule)は、型判断から新しい型判断を作り出す規則です。型推論規則は、次のような型推論(type inference (rule) figure)で記述します。「推論図」、「推論規則」、「規則」という言葉は同義語として使われるので注意してください。


(適用の条件: VarSet(Γ)∩VarSet(Δ) は空でなくてはならない)
〈Γ| E〉:A 〈Δ| F〉:A->B
--------------------------[適用]
〈Γ, Δ| E▷F〉:B

〈Γ| E〉:A 〈Γ| F〉:B
------------------------[デカルトペア]
〈Γ| (E F)〉:A×B

〈Γ| E〉:A×B
----------------[第一成分]
〈Γ| E_1〉:A

〈Γ| E〉:A×B
----------------[第ニ成分]
〈Γ| E_2〉:B

〈x:A, Γ| E〉:B
------------------------[関数抽象]
〈Γ| λx:A.E〉:A->B

型推論規則は、ラムダ項の構文構成規則(term forming rule)と、型付け規則(typing rule)の両方を兼ねています。項の構成と同時にその型も与えているのです。


変数と定数(!は定数)は公理で規定し、他の構文的構成は推論規則で表現しています。しかし、後で出てくる代入(substitution)を前提にして、推論規則を公理に移すこともできます。例えば、ペアの構成を公理にできます。

  • [ペア] Γのなかに x:A と y:B がこの順で(x:A が先で)含まれるならば、〈Γ| (x y)〉:A×B は公理である。

型推論図を積み重ねた図形を型証明図(type proof figure)と呼びます。しばしば、単に証明図ともいいます。次は型証明図の例です。☆は、直下が型公理であることを示す目印です。


☆ ☆
-----------[変数] -------------------[変数]
〈x:A| x〉:A 〈f:A->B| f〉:A->B ☆
--------------------------------------[適用] -----------------[変数]
〈x:A, f:A->B| x▷f〉:B 〈g:B->C| g〉:B->C
-------------------------------------------------------------------[適用]
〈x:A, f:A->B, g:B->C| (x▷f)▷g〉:C
----------------------------------------[関数抽象]
〈f:A->B, g:B->C| λx:A.(x▷f)▷g〉:A->C

型証明図の最下段に現れる型判断を、その型証明図の結論(conclusion)と呼びます。最上段がすべて星印(☆)である型証明図は閉じた型証明図(closed type proof figure)と呼びます。閉じた型証明図の結論となる型判断は型証明可能(type provable)だといいます。混乱の恐れがないなら単に証明可能(provable)でもいいです。

型宣言付き疑似ラムダ項〈Γ:E〉が、〈Γ|E〉:A という型判断と、この型判断を結論とする閉じた型証明図を持つとき、型付け可能(typable)と呼びます。次の2つの言い方は同じ意味です。

  • 型判断 〈Γ|E〉:A が型証明可能である。
  • 〈Γ|E〉は型付け可能で、ΓのもとでのEの型はAである。

型宣言付き疑似ラムダ項〈Γ|E〉が型付け可能なとき、それを型付きラムダ項(typed lambda term)、または型付きラムダ式(typed lambda expression)と呼びます。文脈から分かるなら、「型付き」を省略して単にラムダ項、ラムダ式でもかまいません。

〈Γ| E〉が型付きラムダ式のとき、全体を大きなラムダ式、内部にある疑似ラムダ項Eを小さなラムダ式とも呼びます。この呼び名は、内部のEだけでは不十分なことを強調するために使っています。小さなラムダ式だけでは、型付け可能かどうかは分かりません。

[適用]推論規則を、次のデカルト適用(Cartesian application)に置き換えたほうが理論的な扱いは楽になります。[適用]でも[デカルト適用]でも、どっちを採用しても証明系の能力は変わりません。


〈Γ| E〉:A 〈Γ| F〉:A->B
--------------------------[デカルト適用]
〈Γ| E▷F〉:B

しかし、[デカルト適用]を使う前に型宣言を揃えるのがめんどくさいので、[適用]を採用しました。

大きなラムダ式のアルファ変換

例として次の大きなラムダ式を考えてみましょう。

  • 〈x:A, f:A->(B->C)| λy:B.(f・x)・y〉

この大きなラムダ式は、次の型判断を持ちます(型判断を持つ型宣言付き疑似ラムダ項を、大きなラムダ式と呼ぶのでした)。

  • 〈x:A, f:A->(B->C)| λy:B.(f・x)・y〉:B->C

この型判断の根拠(型証明図)は次です。

                        ☆                         ☆
                   ------------[変数]  -----------------------------[変数]
    ☆             〈x:A| x〉:A        〈f:A->(B->C)| f〉:A->(B->C)
 -----------[変数] -------------------------------------------------[適用]
〈y:B| y〉:B       〈x:A, f:A->(B->C)| f・x〉:B->C
 --------------------------------------------------[適用]
      〈y:B, x:A, f:A->(B->C)| (f・x)・y〉:C
      -------------------------------------------[関数抽象]
      〈x:A, f:A->(B->C)| λy:B.(f・x)・y〉:B->C

大きなラムダ式のインフォーマルな解釈は写像です。型は集合だと思うと、〈x:A, f:A->(B->C)| λy:B.(f・x)・y〉は次の写像を表します。

  • x∈A, f∈(A->(B->C) に対して、式 λy:B.(f・x)・y で表される(B->C)の要素を対応させる。

写像の表現としては、入力変数の名前はどうでもいいので、〈s:A, k:A->(B->C)| λy:B.(k・s)・y〉でも同じ写像を表します。この事情を考慮して、大きなラムダ式にもアルファ変換を定義します。大きなラムダ式のアルファ変換は、内部の小さなラムダ式に対して自由変数のリネームになります。その点を注意すれば、要領は通常のアルファ変換と同じです。混乱しそうなときは、大きなアルファ変換という言葉を使います。

大きなアルファ変換は、必要なときにいつでも実行してかまいません。例えば[適用]推論規則には、「適用の条件: VarSet(Γ)∩VarSet(Δ) は空でなくてはならない」という制限がついてましたが、事前にアルファ変換をするなら、この制限はないも同然です。大きなアルファ変換を明示的に書くときは、次の推論図を使います。

  〈Γ| E〉:A
  ---------------[アルファ変換]
  〈Γ'| E'〉:A

Γ'とE'は、変数をリネームした結果

今後は、大きなアルファ変換で移れる大きなラムダ式は同一視することにします。大きなアルファ変換による同値関係の商集合を考える、とも言えます。

大きなラムダ式の構造規則

推論規則の上段・下段を比べると、関数抽象以外では、上段の型宣言はそのまま下段に引き継がれます。関数抽象では、一番左の個別宣言が取り除かれます。現状では、個別宣言の順序を変えたり、個別宣言を足すことはできません。これでは困ります。

そこで、大きなラムダ式の型宣言部分を操作する規則を導入します。それらの規則を構造規則(structural rule)と呼びます。構造規則も型判断に対する推論図として表現します。構造規則の名前は、直積以外はシーケント計算にちなみます。

  • (interchange)
  • (thinning)
  • (contraction)
  • 直積(direct product)
 〈Γ, x:A, y:B, Δ| E〉:C
 --------------------------[換]
 〈Γ, y:B, x:A, Δ| E〉:C

 〈Γ| E〉:A
 ---------------------[増]
 〈Δ, Γ, Π| E〉:A

 〈Δ, x:A, y:A, Π| E〉:C
 --------------------------[減]
 〈Δ, x:A, Π| E[x/y]〉:C

 〈Δ, x:A, y:B, Π| E〉:C
 --------------------------------------[直積]
 〈Δ, p:A×B, Π| E[p_1/x, p_2/y]〉:C

[増]構造規則を使う前提で、型公理を減らすことができます。

  • [変数] 〈x:A| x〉:A
  • [ユニット] 〈| !〉:I

別にうれしくないので型公理を減らしませんけどね。

[換]構造規則を何度か使うと、型宣言の順序を自由に入れ替えることができます。入れ替えても型判断はそのまま成立する(あるいは、やっぱり成立しない)ので、型判断における型宣言の順序はどうでもいいことが分かります。

[直積]構造規則は、シーケント計算では論理規則に分類されています。論理における構造規則と論理規則の区分は、ラムダ計算の構文論/意味論の観点からは重要ではありません。割とどうでもいい区分です。なお、ラムダ計算とシーケント計算の関係は、次の記事でも触れています。

マルチ代入

E1, ..., En が小さなラムダ式、x1, ..., xn は変数とします。小さなラムダ式Fに対して、Fのなかに出現する自由変数xi(それがあれば)をEi(i = 1, ..., n)で置き換えた式を、

  • F[E1/x1, ..., En/xn]

と書きます(書き方については「型推論に関わる論理の概念と用語 その6:substitutionの記法」参照)。これは、同時置き換えであって、変数1個ずつ順番に置き換えるわけではありません。複数の変数に対する同時置き換えをマルチ代入(multi-substitution)と呼ぶことにします。「マルチ」を使ったのは、複圏(multicategory = operad)と関係しているから、という理由もあります。代入(置き換え)で、意図せぬラムダ束縛が生じないように注意する点は自由変数のリネームと同様です。


マルチ代入は、代入(置き換え)の並列実行だと言っていいでしょう。しかし、並列実行は直列逐次実行でシミュレートできます。何も考えずに逐次実行すると、奇妙な結果になるので、適切に変数のリネームをする必要がありますが、個々の変数出現を1つずつ順番に処理することでマルチ代入をシミュレートできます。

置き換え操作は、型を考慮せずに実行することができますが、型を考慮した正しい置き換えのルールは、次の型推論図で示されます。この推論図(推論規則)もマルチ代入と呼びます。


(マルチ代入の条件: VarSet(Γ1), ..., VarSet(Γn), VarSet(Δ) は、どの2つも共通部分が空(disjoint)でなくてはならない)
〈Γ1| E1〉:A1
...
〈Γn| En〉:An
〈x1:A1, ..., xn:An, Δ| F〉:B
-------------------------------------------[マルチ代入]
〈Γ1, ..., Γn, Δ| F[E1/x1, ..., En/xn]〉:B

横線の上段は、n個の型判断を横に並べたものですが、スペースとレイアウトの関係上縦に並べています。Δは、代入で手付かずの変数が含まれる型宣言です。[マルチ代入]推論規則はΔを許すので、変数すべてを置き換える必要はありません。参考に、[マルチ代入]推論規則に対応するストリング図変形を挙げておきます。

Δが空のときはフル・マルチ代入(full multi-substitution)といいます。


(フル・マルチ代入の条件: VarSet(Γ1), ..., VarSet(Γn) は、どの2つも共通部分が空(disjoint)でなくてはならない)
〈Γ1| E1〉:A1
...
〈Γn| En〉:An
〈x1:A1, ..., xn:An| F〉:B
-------------------------------------------[フル・マルチ代入]
〈Γ1, ..., Γn| F[E1/x1, ..., En/xn]〉:B

推論規則としての[マルチ代入]と[フル・マルチ代入]は同等(どっちを採用しても同じ)ですが、実用上の便利さからマルチ代入を採用します。

型証明系TPS1

今まで述べたことの中間まとめをしておきましょう。

疑似ラムダ項Eと型宣言Γの構文を説明して、それらの組み合わせとして型判断〈Γ| E〉:A (Aは型)を導入しました。型判断は「型宣言Γのもとで、ラムダ項Eの型はAである」という主張です。その主張が正しいことを保証するメカニズムが型証明系(type proof system)です。

一般に論理的証明系(演繹系)は、証明すべき主張を表現する(sentence)の集合、最初から正しいと(天下りに)決めた文である公理(axiom)の集合、新しい文を作り出す手順を示す推論規則(inference rule)の集合からなります。今回の型証明系では、文は型判断であり、公理の集合と推論規則の集合は次のように与えられました。

  1. [変数]公理
  2. [ユニット]公理
  3. [適用]推論規則
  4. [デカルトペア]推論規則
  5. [第一成分]推論規則
  6. [第ニ成分]推論規則
  7. [関数抽象]推論規則
  8. [マルチ代入]推論規則

補助的に、(大きな)アルファ変換と構造規則があります。

  1. アルファ変換
  2. [換]構造規則
  3. [増]構造規則
  4. [減]構造規則
  5. [直積]構造規則

推論規則/アルファ変換/構造規則の組み合わせが証明ですが、証明は証明図という図形で表します。

今回我々が定義した型に関する証明系をTPS1(Type Proof System 1 固有名詞)と呼ぶことにします。いちおうのまとまりが付いたので、TPS1という名前を付けましたが、TPS1は型付きラムダ計算を展開するには機能不足だし、意味論がないので文字通り意味不明だと注意しておきましょう。後でもう少し拡張します。圏論的意味論もいずれ述べる予定です(今回は正式な意味論はなし)。

型判断をα, βなどのギリシャ文字小文字で表すことにします。型判断αがTPS1において証明可能なことを、記号的に次のように書きます。

  • |-TPS1 α

証明図の最上段に現れる型判断を、その証明図の仮定(assumption)と呼びます。星印が上に位置する公理は仮定ではありません。TPS1において、型判断α1, ..., αnを仮定して型判断βが相対証明可能(relatively provable)とは次の意味です。

  • βを結論として、α1, ..., αn の全部または一部を仮定として持つTPS1の証明図が存在する。

記号的には次のように書きます。

  • α1, ..., αn |-TPS1 β

相対証明可能なことも単に証明可能性という場合が多いです。


メタな記号 |-TPS1 を定義したのですが、このようなメタな定義でよいのか? は議論の余地があります。上記の定義では、証明系が仮定を使うとき、「仮定の一部を捨ててもよい」「1つの仮定を何度も使ってよい」「仮定をどの順番で使ってもよい」などを暗黙に前提しています。つまり、仮定の“集まり”を集合だと前提していて、リストやマルチセットは考えてません。

メタな概念である「証明可能性」をさらに形式化して扱うときは、このへんのところをもっと検討する必要があります。

TPS1における代入消去と型付けの一意性

大きなラムダ式〈Γ| E〉は、定義により型付け可能です。つまり、TPS1で証明可能な型判断〈Γ| E〉:A があります。しかし、型Aが一意に決まるかどうかは明らかではありません。

TPS1において、型判断 〈Γ| E〉:A が証明可能なとき、その証明図がひとつとは限りません。例えば、 〈| (! !)〉:I×I は次のようにして証明できます。

     ☆                    ☆
 ----------[ユニット]  ----------[ユニット]
 〈| !〉:I             〈| !〉:I
 ----------------------------------[デカルトペア]
        〈| (! !)〉:I×I

これより短い証明図はありませんが、長い証明図は書けます。例えば:

[ユニット2つ]は次の図とする。
     ☆                    ☆
 ----------[ユニット]  ----------[ユニット]
 〈| !〉:I             〈| !〉:I


                  ☆                      ☆
            ----------------[変数]  ----------------[変数]
           〈x:I, y:I| x〉:I       〈x:I, y:I| y〉:I
            ----------------------------------------------[デカルトペア]
 [ユニット2つ]     〈x:I, y:I| (x y)〉:I×I
 ---------------------------------------------[マルチ代入]
             〈| (! !)〉:I×I

2つの証明図に対応するグラフ(ツリー)は次のようになります。

このような冗長で回り道をした証明ができてしまうのは、マルチ代入規則があるせいです。マルチ代入規則を除外して、他の規則だけにすると(多少の工夫もして)、型判断に対する証明図が(あれば)ひとつだけになります。

しかし、今まで在った推論規則をなくしてしまうので、今まで証明できていた型判断が証明できなくなるリスクがあります。幸いなことに、この心配は無用で、次のメタ定理が成立します。

  • ある型判断がTPS1で証明可能なとき、マルチ代入規則なしでも証明できる。

もっと具体的に言えば:

  • ある型判断のTPS1の証明図があるとき、その証明図を変形して、マルチ代入規則なしの証明図を構成できる。

この事実は、シーケント計算のカット消去定理(Cut elimination theorem)の対応物です。代入消去定理(Substitution elimination theorem)と呼びましょう。

代入消去により得られた証明図は、それ以上は短くできない形をしているので一種の正規形(normal form)となります。正規形の証明図=マルチ代入なしの証明図に限定すれば、型判断と証明図が1:1に対応します。型判断がなんにしろ証明可能なら、それは唯一の正規形証明図を持ちます。

正規形証明図の一意性から、型付けの一意性が従います。

  • 大きなラムダ式〈Γ| E〉が型付け可能なら、その型は一意的に決まる。

適切なアルゴリズムにより、型と共に型付けの証拠である正規形証明図も一意的に得られます。これは大変に都合の良い性質で、TPS1はラムダ計算の構文的基盤として適切であると言っていいでしょう。

証明図に対する代入消去は、代入計算の実行を意味するので、代入消去のアルゴリズムは、“証明図を実行する手順”=“証明図のインタプリタ実装”を与えます。証明図の実行結果である正規形証明図はメタレベルの“値”と解釈されます。つまり、TPS1の証明図をプログラム・ソースコードとするプログラミング・システムがあると考えることができるのです。

ラムダ計算のポリ化: 型証明系TPS2

今まで、型宣言付き疑似ラムダ項は〈Γ| E〉という形で、内部に必ず1個の疑似ラムダ項を持っていました。これを一般化して、内部に複数個の疑似ラムダ項を書いていいことにします。次のような形です。

  • 〈Γ| E1, ..., En〉 (n ≧ 1)

この形を、型宣言付きポリ疑似ラムダ項(type-declared lambda poly-pseudoterm)と呼びます。名前が長すぎるので、ポリ・ラムダ式(poly-lambda expression)とも呼ぶことにします。「ポリ」を付けたのは、多圏(polycategory)と関係するからです。

疑似ラムダ式の並びをΦ, Ψなどのギリシャ文字大文字で表すことにすると、ポリ・ラムダ式は〈Γ| Φ〉という形になります。並び(リスト)の長さをlength(-)と書くことにして、ポリ・ラムダ式(width)と余幅(cowidth)を次のように定義します。

  • width(〈Γ| Φ〉) = length(Γ)
  • cowidth(〈Γ| Φ〉) = length(Φ)

width(〈Γ| Φ〉) = 0 はあり得ますが、cowidth(〈Γ| Φ〉) ≧ 1 です(cowidth(〈Γ| Φ〉) = 0 は今のところ認めません、後で許容するように変更しますが)。任意のn, m(n ≧ 0, m ≧ 1)に対して、width(〈Γ| Φ〉) = n, cowidth(〈Γ| Φ〉) = m であるポリ・ラムダ式が存在します。

ポリ・ラムダ式に対するポリ型判断(poly type judgement)は、次の形です。

  • 〈Γ| E1, ..., En〉:A1, ..., Am

ポリ型判断の幅と余幅もポリ・ラムダ式の場合と同様に定義できます。

ポリ型判断の証明可能性に関して、次が成立することが要請されます。

  1. n = 1 のとき、〈Γ|E〉:A が証明可能かどうかは、既にTPS1で定義されている通り。
  2. n ≧ 2 のとき、〈Γ| E1, ..., En〉:A1, ..., An が証明可能なのは、〈Γ| E1〉:A1, ..., 〈Γ| En〉:An がすべてTPS1で証明可能なとき。

二番目の要請を、推論図として表現すると、次のようになります。


〈Γ| E1〉:A1
...
〈Γ| En〉:An
------------------------------[デカルト併合]
〈Γ| E1, ..., En〉:A1, ..., An

この推論図は、デカルト・タプルの構成法と似てるので、デカルト併合(Cartesian merge)と呼びます。参考に、[デカルト併合]推論規則に対応するストリング図変形を挙げておきます。

ポリ型判断に対して[マルチ代入]推論規則はうまく機能しないので、ポリ型判断に関する代入規則であるポリ代入(poly substitution)を導入します。


(ポリ代入の条件: VarSet(Γ)∩VarSet(Δ) は空でなくてはならない)
〈Γ| E1, ..., En〉:A1, ..., An
〈x1:A1, ..., xn:An, Δ|Ψ〉:B1, ..., Bn
--------------------------------------------------------[ポリ代入]
〈Γ, Δ| Ψ[E1/x1, ..., En/xn]〉:B1, ..., Bn

ここで、Ψ[E1/x1, ..., En/xn] は、リストΨに含まれるすべての疑似ラムダ項にマルチ代入[E1/x1, ..., En/xn]を施したリストを意味します。参考に、[ポリ代入]推論規則に対応するストリング図変形を挙げておきます。

上記の推論図において、Δが空のときはフル・ポリ代入(full poly-substitution)と呼びます。

ポリ型判断を扱う新しい型証明系TPS2を次のように定義します。

  1. TPS2の文は、ポリ型判断だとする。この定義より、(TPS1の文の集合) ⊆ (TPS2の文の集合)。
  2. TPS2の公理の集合は、TPS1の公理の集合と同じ。
  3. TPS2の推論規則(推論図)の集合は、TPS1の推論規則(推論図)に[デカルト併合]を加え、[マルチ代入]を[ポリ代入]と交換したもの。
  4. TPS2の推論図として、TPS1の構造規則(の推論図)もそのまま採用する。推論規則が冗長になる(不要なものまで入る)が気にしない。

TPS1とTPS2に関して、次のメタ定理が成立します。

  1. 〈Γ|E〉:A がTPS1で証明可能ならば、TPS2でも証明可能である。(自明)
  2. 〈Γ|E〉:A がTPS2で証明可能ならば、TPS1でも証明可能である。(非自明)
  3. 〈Γ| E1〉:A1, ..., 〈Γ| En〉:An がすべてTPS1で証明可能ならば、〈Γ| E1, ..., En〉:A1, ..., An がTPS2でも証明可能である。(自明)
  4. 〈Γ| E1, ..., En〉:A1, ..., An がTPS2で証明可能ならば、〈Γ| E1〉:A1, ..., 〈Γ| En〉:An はすべてTPS1でも証明可能である。(非自明)

これらのメタ定理の証明(証明系を外から見てのメタレベルの証明)は、もう少し準備して組み合わせ的・帰納的議論をする必要があります。今回は割愛します。

TSP2の証明可能性がTSP1での議論に帰着できるので、ポリ・ラムダ式の型付けの一意性が言えます。

もうひとつの型証明系TPS3

TPS1は、単一のラムダ式の型付けや代入計算を行うのに便利です。TPS2は、複数のラムダ式を一度に扱うために導入しました。TPS2の1個の型判断(ポリ型判断)は、TPS1の複数の型判断をまとめただけと言えます。

さて、大きなラムダ式圏論的な扱いに適した型証明系としてTPS3を導入します。まず、TPS3では、〈Γ|〉という形の大きなラムダ式を認めます。TPS2における型は、単一型の非空リストでしたが、TSP3では空リスト()を認めます。これに伴い型判断(ポリ型判断)の構文も拡張します。

型証明系→ TPS1 TPS2 TPS3
型判断の幅 n n ≧ 0 n ≧ 0 n ≧ 0
型判断の余幅 m m = 1 m ≧ 1 m ≧ 0
単一の型 長さ1以上の型のリスト 任意長の型のリスト

Γは空も許す型宣言の並び、Φは空も許す型宣言の並び、A1, ..., An を空(n = 0)も許す型の並びとして、TPS3の型判断は、〈Γ| Φ〉:A1, ..., An の形です。3種類の並び(リスト)から構成されますが、並びの長さに何の制限もありません

型証明系としてのTPS3を定めるために、型公理と型推論規則を決めましょう。TPS2で使った以下の型公理/型推論規則はそのまま使い続けます。

  1. [変数]公理
  2. [ユニット]公理
  3. [適用]推論規則
  4. [第一成分]推論規則
  5. [第ニ成分]推論規則
  6. [関数抽象]推論規則

(大きな)アルファ変換も使います。構造規則は廃止します。

TSP3では次の公理を追加します。

  • [空] 〈Γ|〉:()

小さなラムダ式は無し、型は空リストです。Γは任意の型宣言です。特に、〈|〉:() は型公理です。

[デカルトペア]推論規則と[ポリ代入]推論規則、[デカルト併合]推論規則は、対応する別な規則と入れ替えます。対応する別な規則の名称は、モノイドペア(monoidal pair)、フル・ポリ代入(full poly-substitution)、モノイド併合(monoidal merge)です。


(モノイドペアの条件: VarSet(Γ)∩VarSet(Δ) は空でなくてはならない)
〈Γ| E〉:A 〈Δ| F〉:B
------------------------[モノイドペア]
〈Γ, Δ| (E F)〉:A×B


〈Γ| E1, ..., En〉:A1, ..., An
〈x1:A1, ..., xn:An| Ψ〉:B1, ..., Bn
--------------------------------------------------------[フル・ポリ代入]
〈Γ| Ψ[E1/x1, ..., En/xn]〉:B1, ..., Bn


(モノイド併合の条件: VarSet(Γ)∩VarSet(Δ) は空でなくてはならない)
〈Γ| Φ〉:A1, ..., An
〈Δ| Ψ〉:B1, ..., Bm
-------------------------------------[モノイド併合]
〈Γ, Δ| Φ, Ψ〉:A1, ..., An, B1, ..., Bm

型証明系TPS3を次のように定義します。

  1. TPS3の文は、空を許すポリ型判断だとする。この定義より、(TPS2の文の集合) ⊆ (TPS3の文の集合)。
  2. TPS3の公理の集合は、TPS2の公理の集合に、[空]公理を追加したもの。
  3. TPS3の推論規則(推論図)の集合は、TPS2の推論規則(推論図)の[デカルトペア]、[ポリ代入]、[デカルト併合]をそれぞれ、[モノイドペア]、[フル・ポリ代入]、[モノイド併合]に入れ替えたもの。
  4. TPS2の構造規則(それはTPS1の構造規則)は採用しない。TPS3では、構造規則は不要。

念のため、TPS3の公理/推論規則を列挙しておきます。'*'はTPS2から変更しているものです。

  1. [変数]公理
  2. [ユニット]公理
  3. [空]公理 *
  4. [適用]推論規則
  5. [モノイドペア]推論規則 *
  6. [第一成分]推論規則
  7. [第ニ成分]推論規則
  8. [関数抽象]推論規則
  9. [フル・ポリ代入]推論規則 *
  10. [モノイド併合]推論規則 *
  11. アルファ変換

TPS3に関して、次のメタ定理が成立します。

  • TPS2で証明可能なポリ型判断はTPS3でも証明可能である。
  • TPS3で証明可能な余幅が0でないポリ型判断はTPS2でも証明可能である。

上記メタ定理の証明も割愛します。

TPS3の証明可能性がTPS2に帰着できるので、TPSでもポリ・ラムダ式の型付けの一意性が言えます。

LLEの定義

型証明系TPS3を定義したのは、TPS3が圏LLE(前回の「概要と目標」参照)を定義する道具に便利だからです。(実際の型証明に使うなら、TPS2のほうが便利でしょう。)

ポリ・ラムダ式〈Γ| Φ〉がTPS3で型付け可能なとき、そのポリ・ラムダ式を、あらためて大きなラムダ式と呼びます。今ここで「大きなラムダ式」の意味を拡張したわけです。すべての大きなラムダ式からなる集合をLLEとします。

大きなラムダ式αが、〈x1:A, ..., xn:An| E1, ..., En〉の形をしているとき、定義によりこれは型付け可能なので、次のポリ型判断がTPS3で証明可能です。

  • 〈x1:A, ..., xn:An| E1, ..., En〉:B1, ..., Bm

ここで、B1, ..., Bm は一意的に決まります。この事実を使って、大きなラムダ式αの域(domain)と余域(codomain)を次のように定義します。大きなラムダ式には余域が一意に決まることがポイントです。

  • dom(α) = (A1, ..., An)
  • cod(α) = (B1, ..., Bm)

dom(α)もcod(α)も型の並び(リスト)です。型の集合をType、型のリストの集合をType*とすれば、写像として、

  • dom:LLE→Type*
  • cod:LLE→Type*

となります。

(A1, ..., An)∈Type* とするとき、(A1, ..., An)に対する恒等ラムダ式(大きなラムダ式)は次のように定義できます。

  • idA1, ..., An = id(A1, ..., An) = 〈x1:A, ..., xn:An| x1, ..., xn

以上で、dom, cod, idが定義できました。LLEとType*を圏に仕立てるには、圏の結合(composition)が必要です。結合は、フル・ポリ代入によって定義します。cod(α) = (B1, ..., Bm), dom(β) = (B1, ..., Bm) のとき、α;βは次の推論図で定義されます。

  α    β
 -----------[フル・ポリ代入]
    α;β

次の圏の条件を示せます。

  1. dom(idA1, ..., An) = (A1, ..., An)
  2. cod(idA1, ..., An) = (A1, ..., An)
  3. cod(α) = dom(β) ならば、α;β が定義できる。
  4. dom(α;β) = dom(α)
  5. cod(α;β) = cod(β)
  6. (α;β);γ = α;(β;γ)
  7. idA1, ..., An;α = α
  8. α;idB1, ..., Bn = α

結合法則 (α;β);γ = α;(β;γ) 以外は自明だと思います。結合法則は、ポリ代入に関するメタ定理です。

以上により、LLEを射の集合、Type*を対象の集合とする圏LLEが定義できました。

LLEのモノイド構造

LLEにはモノイド構造が入ります。それをこの節で述べます。LLEのモノイド積の記号を□とします。

まず、LLEの対象に対するモノイド積を定義します。(A1, ..., An), (B1, ..., Bm)∈Type* に対して、(A1, ..., An)□(B1, ..., Bm) は連接で定義します。

  • (A1, ..., An)□(B1, ..., Bm) = (A1, ..., An, B1, ..., Bm)

Type*は、□をモノイド演算、空リスト()を単位元とするモノイドとなります。

LLEの射(大きなラムダ式)α, βに対しては、α□βを次の推論図で定義します。

  α   β
 ----------[モノイド併合]
   α□β

(LLE, □, ())は厳密モノイド圏になります。そのことを示すには、次の等式群を確認します。

  1. dom(α□β) = dom(α)□dom(β)
  2. cod(α□β) = cod(α)□cod(β)
  3. id(A1, ..., An)□(B1, ..., Bm) = (idA1, ..., An)□(idB1, ..., Bm)
  4. (α;β)□(γ;δ) = (α□γ);(β□δ)
  5. (α□β)□γ = α□(β□γ)
  6. α□id() = id()□α = α

交替律 (α;β)□(γ;δ) = (α□γ);(β□δ) は、(α□id);(id□β) = (id□β);(α;id) という簡略な形でもいいので、これらの証明は難しくありません。モノイド演算□が、列の連接に過ぎないので事情が非常に簡単になっています。繰り返し注意しますが、大きなアルファ変換は必要なら自動的に実行されると考えます。

ラムダ式の変換と同値に関する注意

ここまでの話では、ラムダ計算では非常に重要であるベータ変換やイータ変換、それらの変換により導入されるラムダ式の同値性が出てきてません。これらの変換と同値性は、構文論だけだと解釈が難しいでしょう。

大きなラムダ式α, βがあって、適切な意味論的解釈〚-〛があるとき、〚α〛 = 〚β〛 ならば、大きなラムダ式αとβは同値だと定めて α ≡ β と書くことにします。メタな命題である α ≡ β を、形式的に証明できる証明系(形式的体系)はどんなものか? と考える必要があります。

同値性に関する証明系は、TPS*より上位の体系になります。仮に、同値性に関する証明系をEPS(equivalence proof system)とすると、次のようなメタ命題のあいだの関係が問題になります。

  • [EPS証明可能性] 形式化された同値性 α ≡ β が形式的証明系EPSで証明可能である。
  • [意味論的同値] 意味論的解釈〚-〛に関して、〚α〛 = 〚β〛 が成立する。

EPSがマトモな証明系であるためには、次(健全性)が要求されます。

  • α ≡ β がEPSで証明可能ならば、〚α〛 = 〚β〛 が成立する。

ベータ同値やイータ同値はEPSの公理となる性質です。EPSに必要な公理はベータ同値/イータ同値だけではなくて、実は色々な公理が要請されます。例えば、〈u:I| u〉と〈u:I| !〉は同値であるべきです。

おわりに

ラムダ式の意味論やラムダ式の同値性の議論が、型付きラムダ計算論の中核でしょう。今回説明したことは、ラムダ式の型付けと代入計算だけ、つまり、圏論的意味論を展開する土台になる構文論の部分です。

型付きラムダ計算の圏論的意味論が目指すべきランドマークは、次の2つのメタな命題が同値であることを主張する“完全性定理”です。

  • |-EPS (α ≡ β)
  • CCCC.( C |= (α ≡ β) )

EPSはラムダ式の同値性に関する証明系で、CCCはすべてのデカルト閉圏(Cartesian Closed Categories)からなるクラスです。C |= (α ≡ β) は、Cに値を持つ解釈(意味関手)〚-〛C に関して 〚α〛C = 〚β〛C であることを意味します。

型付きラムダ計算に関する手法や結果を、このビッグピクチャーのなかに位置付けると、けっこう納得感があると思います。今回の一連の話も、ビッグピクチャーのピースを眺めたことになります。