檜山正幸のキマイラ飼育記 このページをアンテナに追加 RSSフィード Twitter

キマイラ・サイトは http://www.chimaira.org/です。
トラックバック/コメントは日付を気にせずにどうぞ。
連絡は hiyama{at}chimaira{dot}org へ。
蒸し返し歓迎!
このブログの更新は、Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama
ところで、アーカイブってけっこう便利ですよ。

2017-05-23 (火)

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

| 11:49 | 型付きラムダ計算 構文論 再入門 2/2: カリー/ハワード対応のためにを含むブックマーク

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

前回 1/2 の内容:

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

今回 2/2 の内容:

  1. 疑似ラムダ項の構文
  2. ラムダ項の構成と型付け
  3. 大きなラムダ式のアルファ変換
  4. 大きなラムダ式の構造規則
  5. マルチ代入
  6. 型証明系TPS1
  7. TPS1における代入消去と型付けの一意性
  8. ラムダ計算のポリ化: 型証明系TPS2
  9. もうひとつの型証明系TPS3
  10. LLEの定義
  11. LLEのモノイド構造
  12. ラムダ式の変換と同値に関する注意
  13. おわりに

疑似ラムダ項の構文

ラムダ項の構文を定義したいのですが、まずはザックリとした構文定義をします。ザックリなので、ここでの定義だけでは不十分です。ここで定義される項(構文的な表現)はちゃんとしたラムダ項ではないので疑似ラムダ項(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 であることを意味します。

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

トラックバック - http://d.hatena.ne.jp/m-hiyama/20170523

2017-05-22 (月)

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

| 09:25 | 型付きラムダ計算 構文論 再入門 1/2: カリー/ハワード対応のためにを含むブックマーク

カリー/ハワード対応への障壁」において、カリー/ハワード対応(Curry-Howard correspondence/isomorphism)をうまく説明するのは難しい、という話をしました。その記事の最後の一言は:

いまだベストと思える説明に届かず。

その後も、ベスト(に近い)説明とはどんなものかと考えています。以前から僕は「大きなラムダ計算」という方法を使っているのですが、これをベースにするのがやはり良いように思えます。大きなラムダ計算は型付きラムダ計算の定式化のひとつです。大きなラムダ計算をまともに紹介したことがなかったので、この記事と引き続く記事の2回に分けて説明します(続く第2回もほぼ書き終えていますよ ^_^)。

この2回の記事で、大きなラムダ計算の構文的・証明論的側面を紹介します。ラムダ式への型付けアルゴリズムを形式的証明と捉えて、その証明系の性質を調べます。カリー/ハワード対応を意識してのことです。証明系に関するメタ定理は、ラムダ式と証明図の構造に沿った帰納法で(メタに)証明できますが、煩雑で若干テクニカルなのでだいたい省略します(いつかちゃんと書くかも)。

「型付きラムダ計算を、構文だけで理解するのは苦しい」と思うので、集合圏におけるインフォーマルな意味論にも少しだけ触れます。少数ですが、複圏/多圏のストリング図も(次回に)載せます。本格的な意味論や絵算(pictorial/graphical/diagrammatic calculation)は展開しませんが、単なる構文解説だけよりは実感が増すと思います。

今回 1/2 の内容:

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

次回 2/2 の内容:

  1. 疑似ラムダ項の構文
  2. ラムダ項の構成と型付け
  3. 大きなラムダ式のアルファ変換
  4. 大きなラムダ式の構造規則
  5. マルチ代入
  6. 型証明系TPS1
  7. TPS1における代入消去と型付けの一意性
  8. ラムダ計算のポリ化: 型証明系TPS2
  9. もうひとつの型証明系TPS3
  10. LLEの定義
  11. LLEのモノイド構造
  12. ラムダ式の変換と同値に関する注意
  13. おわりに

予備知識と参考資料

ゼロからのラムダ計算入門には、10年前(2007年)に書いた一連の記事が、今でも役立つと思います。

  1. JavaScriptで学ぶ・プログラマのためのラムダ計算プログラミング言語JavaScriptを引き合いに出して、ラムダ計算をインフォーマルに説明しています。意図的ではありますが、関数抽象を(狭い意味の)「ラムダ式」と呼んだり、通例(「関数を引数に適用する」)とは逆の表現「引数を関数に適用する」をしているので注意してください。
  2. JavaScriptで学ぶ・プログラマのためのラムダ計算 問題集 : すぐ上の記事に対する練習問題集です。
  3. 絵を描いて学ぶ・プログラマのためのラムダ計算 : ラムダ項の構文解析木を使ってベータ変換を解説しています。なお、この過去記事で使っている絵はベータ変換の可視化が目的で、圏論ベース絵算のストリング図ではありません。

型無しラムダ計算の構文とベータ変換(簡約)を簡潔にまとめた記事として、id:tarao(たらお)さんによる次があります。

僕は、アルファ変換について説明してない(予告して不履行)ですが、アルファ変換はけっこう厄介です(ラムダ計算 - Wikipedia)。アルファ変換を知るには、id:sumii(住井)さんの次のテキストの1.5節あたりまで読むのがいいと思います。

ちなみに、上記テキストで"typing"の訳語が「型つけ」なのですが、ナルホド! 口頭でも「片付け」と混同しなくて良いですね。

型付きラムダ計算とデカルト閉圏の関係は次の記事達に書いています。解説というより、雰囲気を伝える“お話”です。興味があれば眺めてみてください。

大きなラムダ計算とは何か

型付きラムダ計算のラムダ式は、変数の型がハッキリしてないとダメなんです。ですから、λx.(g・(f・x)) のような式(ドット'・'は適用だとする)だけ出してもダメです。x, f, g の型を明示する必要があります。型の明示には型宣言を使うことにします*1。A, B, Cを型(の名前)だとして次のように宣言します。

  1. xの型は、A
  2. fの型は、AからBへの関数型
  3. gの型は、BからCへの関数型

これらの宣言を記号的に次のように書きます。

  1. x:A
  2. f:A->B
  3. g:B->C

'->'は関数型を作る記号で、普通の矢印'→'じゃなくて、ハイフンと不等号です。矢印'→'は他でも多用されるので記号を変えました。[A, B] という書き方も多いですが、ブラケットも他の目的で使うので、関数型は A->B にします。

ラムダ式と型宣言を一緒にしてパッケージしたものが大きなラムダ式*2です。ただし、ラムダ束縛変数の型宣言は'λ'の直後に埋め込んでいます(それが普通の書き方)。次は大きなラムダ式の例です。

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

大きなラムダ式との対比のために、内側に置かれたラムダ式を小さなラムダ式とも呼びます。大きなラムダ式の基本的な形は次のようです。

  • 〈型宣言| 小さなラムダ式〉

小さなラムダ式(裸のラムダ式)ではなくて、常に大きなラムダ式を使って進めていくのが大きなラムダ計算です。基本はそれだけのことです。

この記事(+次回)で大きなラムダ計算について最初から説明するので過去記事を参照する必要はありませんが、歴史的経緯を言えば、2008年/2009年あたりのセミナーでは、大きなラムダ計算をインフォーマルに導入しています。

大きなラムダ計算の短い説明ならば次の記事にあります。

概要と目標

前節で説明したような大きなラムダ式(後で少し定義を拡張します)の全体を考えます。すべての大きなラムダ式からなる集合をLLE(large lambda expressionから)とします。LLEに、圏の構造を与えることができます。正確な言い方をすると、集合LLEをベースに圏を作れる、となります。集合LLEをベースに作った圏のほうは太字でLLEと書くことにしましょう。

集合LLEと圏LLEとの関係は、

  • Mor(LLE) = LLE

です。つまり、大きなラムダ式は圏LLEの射(morphism)となります。

では、圏LLEの対象は何でしょうか? それは、大きなラムダ計算で使う型の集合です。当該ラムダ計算で使用できるすべての型の集合をTypeとすると、

  • Obj(LLE) = |LLE| = Type*

です。Type*はTypeの要素を並べたリストの集合、つまり“単一の型を並べたリスト”の集合です。

この記事(+次回)の目標は、圏LLEを構成することです。

注意すべきは、圏LLE完全に構文的に作られているということです。(型付き)ラムダ計算に意味を与えることは、構文領域である圏LLEから意味領域となる圏Cへの関手を作ることです。(意味関手は、単なる関手以上にモノイド構造や閉構造などを保つことも要請します。)例えば、C = Set として、意味関手 SetSem:LLESet を作れば、ラムダ計算を集合と写像の計算として解釈することになります。

意味関手が値を取る圏Cを変えればまったく別な意味論ができます。例えば、順序代数構造(Heyting algebraなど)から作られたやせた圏Cとすることもできます。Cを固定しても意味関手は色々作れます*3

今回(+次回)は圏LLEを作るまでで、その上に意味関手を定義はしませんが、意味論を展開する構文的基盤を準備するのだと思うとよいでしょう。

集合と写像に関する基礎的事項

この節は、インフォーマルな意味論の説明に必要となる用語のまとめです。ザッと眺めるだけ、あるいは飛ばしてしまってもけっこうです。

A, B, Cなどは集合を表すとします。fがAからBへの写像であることを f:A→B と書きます。x∈A ならば、f(x)∈B です。A×Bは集合の直積で、g:A×B→C とは、「gが、AとBのペアを入力としてCの要素を返す写像である」ことです。x∈A, y∈B ならば、g(x, y)∈C です。なお、写像と関数は同義語として扱い、特に区別しません。

関数集合

AからBへの写像の全体を集合と考えたものをBAと書きます。この指数記法は入れ子にするのが辛いので、BAを A->B とも書きます。矢印風記法なら、入れ子も問題ありません; 例えば、A->(B->C) 。A->B を指数集合(exponential set; もともと指数記法で書いたので)とか関数集合(function set)と呼びます。

関数オブジェクト

f:A→B と f∈(A->B) は同じ意味ですが、「AからBへの写像」と「A->B の要素」を区別しないと混乱してしまうことが多いので、関数集合 A->B の要素を関数オブジェクト(function object)と呼ぶことにして、写像fに対応する関数オブジェクトを^fと書きます。(f^とも書きますが、今回は左肩にハットを付けます。)

  • f:A→B ⇔ ^f∈(A->B)

関数オブジェクト^fは、働きとしてのfをコンパイルした結果であるバイナリコードだと思うといいでしょう。^fはバイナリコード=実行可能データです。

適用

入力データxと実行可能データ^fを渡して実行する仮想マシン(の概念的モデル)をappとすると、appは次のような写像です。

  • app:A×(A->B)→B

実行結果は、もとの写像fの値となるので、次の等式が成立します。

  • app(x, ^f) = f(x)

appと入力の順序が逆である写像をapp'とします。

  • app':(A->B)×A→B
  • app'(^f, x) = f(x)

appやapp'を適用写像(application)とか評価写像(evaluation)と呼びます。

写像の直積

集合だけでなくて、写像にも直積を定義しましょう。f:A→X, g:B→Y のとき、f×g:A×B→X×Y は次のように定義します。

  • (f×g)(x, y) := (f(x), g(y))
デカルトペア

<f, g>(x) = (f(x), g(x)) と定義される写像を、fとgのデカルト・ペア(Cartesian pair)と呼びます。写像の直積とデカルトペアは、対角写像Δ(定義: Δ(x) = (x, x))により次のように関係付けられます。

  • <f, g> = Δ;(f×g)
射影と成分

A×B→A という射影をπ1、A×B→B という射影をπ2と書きます。f:C→A×B のとき、f1 = f;π1、f2 = f;π2 と書きます。f1をfの第一成分(first component)、f2をfの第ニ成分(second component)と呼びます。具体的に書くと:

  • f(z) = (x, y) のとき、f1(z) = x、f2(z) = y
単元集合と廃棄写像

1 = {0} として単元集合(シングルトン集合; singleton set)と呼びます。単元集合の唯一の要素は何でもいいです。単元集合を型とみなすときはユニット(unit)型とかヴォイド(void)型とか呼びます。

任意の集合Aから1への写像がただひとつだけあるので、それを!Aと書きます; !A:A→1。!Aには様々な呼び名があります: terminal morphism, final morphism, discarder, discharger など。ここでは、入力を捨ててしまうので廃棄写像(discarding map)と呼びましょう。

型システム

これから先「型」という言葉を頻繁に使います。「型」という言葉の解釈は、めちゃくちゃイッパイあります。ここでは、次の2つの立場を適宜使い分けます。

  1. 型とは集合である。
  2. 型とは単なる記号である。

インフォーマルな意味論としては、「型」は集合を表すと考えます。しかし今回は、オフィシャルな意味論の話はなくて、構文論だけです。実際のところは“ある種の記号”を「型」と呼ぶことになります。

インフォーマルな意味論も含めて、型を構成する手順を説明しましょう。まず、有限個の集合を選びます。例えば、自然数の集合 N = {0, 1, 2, ...} ひとつだだけを選びます。選んだ集合に名前(の記号)を割り当てます。例えば、自然数の集合に英字大文字'N'を割り当てます。他に、英字大文字'I'を単元集合1を表す記号として予約します。これで基本型記号(basic type symbol/name)が決まります。

何でもいいので2種類の結合子記号(connective symbol)を決めます。例えば'△'と'♂'にします。一般的な型記号(type symbol)、あるいは型項(type term)を帰納的に定義します。

  1. 基本型記号は型記号である。
  2. AとBが型記号ならば、(A△B) は型記号である。
  3. AとBが型記号ならば、(A♂B) は型記号である。
  4. 以上により定義されたものだけが型記号である。

心づもりとしては、型記号は集合を表すものです。基本型記号がNとIの場合、型記号Aが表す集合を〚A〛とすれば:

  1. 〚N〛 = N, 〚I〛 = 1
  2. 〚A△B〛 = 〚A〛×〚B〛
  3. 〚A♂B〛 = 〚A〛->〚B〛

例えば ((N△I)♂(N♂N)) の意味は 〚((N△I)♂(N♂N))〛 = (N×1)->(N->N) と計算できます。

以上の“記号の意味”はあくまで心づもり、想定であって、実際には意味論なしの構文論を考えます。したがって、オフィシャルには型とは型記号(型項)のことです。

型が等しいとは、集合の同一性や同型性ではなくて、記号として(図形として)の等しさです。(I△N) と N は違う記号なので違う型です。((N△N)△I) と (N△(N△I)) も違う記号なので違う型です。型Aと型Bがイコールだとは、AとBがまったく同じ記号のことです。

いま、結合子記号に'△'と'♂'を選びましたが、'×'と'->'にします。そうすると、集合のホントの直積/指数と区別が付かない問題が起きますが、文脈により、単なる結合子記号か集合の演算子記号かは区別できるでしょう。

また、(I×N) とか ((N×N)×I) のように律儀に括弧は付けず、I×N、N×N×I のように書きます。要するに、混乱がない限り普通の書き方をする、ということです。普通に書くと、人間の心理として集合を想定してしまいがちですが、オフィシャルには単なる記号だと肝に銘じてください。

続く

次回に続きます。次回で大きなラムダ式の構文を定義して、型付け(typing)を行うための形式的証明系を導入します。そして、構文論だけから得られる圏LLEを定義します。次回内容は:

  1. 疑似ラムダ項の構文
  2. ラムダ項の構成と型付け
  3. 大きなラムダ式のアルファ変換
  4. 大きなラムダ式の構造規則
  5. マルチ代入
  6. 型証明系TPS1
  7. TPS1における代入消去と型付けの一意性
  8. ラムダ計算のポリ化: 型証明系TPS2
  9. もうひとつの型証明系TPS3
  10. LLEの定義
  11. LLEのモノイド構造
  12. ラムダ式の変換と同値に関する注意
  13. おわりに

*1:変数に型情報をくっ付けるとか、型ごとに別な変数集合を準備するとかの方法もあります。ですが、型宣言が一番実用的だと思います。

*2:大きなラムダ式は、実質的には型付きラムダ項(typed lambda term)と変わりません。型宣言とのパッケージを徹底することが意図されています。

*3[追記]構文的な体系をひとつに固定したとして、圏Cに値を取る意味関手がたくさん定義できるのは事実です。しかし、これは鬱陶しくてイヤな状況です。できるなら、Cを決めれば一意的に意味関手が定まって欲しい -- この希望をかなえるように意味論を構成することは可能です。僕が「セマンティック駆動」と言ってきた方法は、Cを先に与えて、それから一意に意味関手を作る方法です。[/追記]

2017-05-18 (木)

よくあるタイポ

| 14:42 | よくあるタイポを含むブックマーク

キーボードで文字を書くと、余分な打鍵が発生して重複した2文字になることがあります。日本語だと、1文字2打鍵なので、それほど起こらないように思えますが、そうでもない。

僕のダイアリー内で「をを」「とと」「のの」を探したらけっこうありました。「とと」「のの」は正しい場合がありますが、「をを」はすべて誤入力です。修正した。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20170518

2017-05-10 (水)

ヤコビ微分圏: はじまり

| 17:00 | ヤコビ微分圏: はじまりを含むブックマーク

CADG(Categorical Abstract Differential Geometry)の練習問題として、ヤコビ微分圏というモノを考えてます。ヤコビ微分圏は、通常の多変数微分計算のエッセンスを圏論的に取り出したものです。ヤコビ微分圏を考えるに至った動機やご利益について語ります。

内容:

  1. CADGとデカルト微分
  2. ヤコビ微分圏の動機
  3. 準半加法圏など
  4. ヤコビ微分圏の抽象的構成・具体的構成

CADGとデカルト微分

CADG(Categorical Abstract Differential Geometry)は、微分や“なめらかさ”の概念を圏論的に定式化して、微分幾何を抽象的に展開する試みです。90年代のリソース・ラムダ計算(resource lambda-calculus, 1993)や80年代のロシツキーの先駆的仕事(Jiri Rosicky, 1984)があったものの、“微分幾何”としての形が整ってきたのは2010年前後でまだ新しい分野です。その有効性と射程はいまだ明らかとは言えません*1

微分を持つ圏/なめらかな対象からなる圏”の定義には幾つもの案があります。そのなかでも基本的で重要なものはデカルト微分(Cartesian differential category)と接圏(tangent category)です。それぞれの圏(の種別)を最初に提案した論文(基本文献)は以下のものです。

デカルト微分圏に関しては、オリジナルから少し変更した一般化デカルト微分(generalized Cartesian differential category)をクラットウェルが定義しています。次の論文に記述があります。

上記の2つの論文のあいだで、一般化デカルト微分圏の定義が少し違っていますが、気にする程の違いではありません。それより、オリジナルのデカルト微分圏(ブルート/コケット/シーリー 2009)と一般化デカルト微分圏(クラットウェル 2013)の関係がハッキリしないほうが問題です。

どうも、一般化デカルト微分圏がオリジナルのデカルト微分圏を完全には包含してないように思えます(下図)。

一般化デカルト微分圏のなかで「すべての対象が(クラットウェルの意味で)“線形”である圏」は間違いなく(ブルート/コケット/シーリーの)デカルト微分圏になります。しかし、デカルト微分圏が必ず一般化デカルト微分圏になる保証はなく、「デカルト微分圏だが一般化デカルト微分圏にならない圏」が存在する可能性があります。とはいいながら、僕はその実例を知らないのですが。

仮に「デカルト微分圏だが一般化デカルト微分圏にならない圏」が在ったにしても、一般化デカルト微分圏のほうが使い勝手がいい定義なので、僕は一般化デカルト微分圏を採用します*2。と、そんな事情で、以降、単にデカルト微分圏と言ってもそれはクラットウェルの一般化デカルト微分圏のことです。

デカルト微分圏は、ユークリッド空間における微分計算の抽象的な定式化です。一方、接圏は、なめらかな多様体の圏から抽象した構造です。デカルト微分圏には必ず接圏の構造を入れられます。さらに、デカルト微分圏に制限構造(restriction structure)を載せて、グロンディ(Marco Grandis)の多様体完備化(manifold completion)すると接圏が出来ることもわかっています。また、適当な仮定のもとで接圏は局所的なデカルト微分圏構造を持ちます*3

以上のことから、「デカルト微分圏 : 接圏」の関係は、「多変数の微分計算 : 多様体微分幾何」の関係と同様だと言えます。CADGの主要な対象物は接圏ですが、その初等理論、局所理論としてデカルト微分圏の理論がある、という状況ですね。

ヤコビ微分圏の動機

f:RnRm をなめらかな写像だとして、一点でのfの微分係数はm行n列のヤコビ行列(Jacobian matrix)で与えられます。CADGでもヤコビ行列の対応物はあるのでしょうか。…… それがないのです。ヤコビ行列の対応物を作るのは可能なのですが、実際には、ヤコビ行列による定式化は採用されていません。その理由は(おそらく)、行列の対応物を作るのが面倒だからでしょう。行列概念なしでも微分計算は可能だし、そのほうが話が単純になります。

「ヤコビ行列を作るのは七面倒くさいだけでいいことないのか?」と疑問に思い、ちょっと試してみました。確かに面倒くさいです。が、いいこと(メリット、見返り)もあります。ヤコビ行列を使った定式化のいいところを挙げてみます。

  1. 通常の多変数微分計算の直接的な定式化である。
  2. 教育的な意義がある。
  3. 論理との関係が見える。
  4. 下部構造が面白い。
  5. 非関手的・非自然な手法が活躍する。

これらのいいことを順に説明していきます。以下では、ヤコビ行列を使った微分ヤコビ微分(Jacobian differential)、ヤコビ微分を備えた圏をヤコビ微分(Jacobian differential category)と呼ぶことにします。

通常の多変数微分計算の直接的な定式化である。

ほとんどの多変数微積分の教科書では、多変数の微分係数・導関数をヤコビ行列により定義していると思います。ですから、ヤコビ行列ベースの定式化は我々が慣れ親しんだシナリオをたどることになり、分かりやすいと思います。ヤコビ微分圏は、通常の微分計算をそのまま圏論フレームワーク内に移します

教育的な意義がある。

CADGでは、位相や極限に関する事は扱いません。これにより、微積分や微分幾何のなかで、何が位相・極限に依存して、何が代数計算だけで出来るのかが明確に切り分けられます。これは教育的に意義がありますが、通常の微分計算/微分幾何と異なったシナリオではピンと来ないでしょう。一番目のメリットである「普通さ」があるヤコビ微分圏なら、「切り分け」も意識しやすくなります。

論理との関係が見える。

僕が「おやっ」と思ったのは、ヤコビ微分圏内の微分計算の公式が命題論理の演繹(公理や推論規則)に対応していることです。含意記号を'⊃'として、微分公式に対応するめぼしい演繹を書くと:

  *(前提なし)
 -----[同一律]
 A⊃A

 A  A⊃B
 --------[モダス・ポネンス]
    B

 A⊃B  B⊃C
 -----------[カット]
   A⊃C

  A⊃(B⊃C)
 ------------
  B⊃(A⊃C)

  A⊃B   C⊃D
 --------------
 (A∧C)⊃(B∧D)

   A
 ----------
 (A⊃B)⊃B

これらの演繹が微分公式に対応していることは、行列概念(の圏論的対応物)とヤコビ微分を導入しないと見えてこないと思います。

下部構造が面白い。

ヤコビ微分を導入する前に、土台になる圏を整備しなくてはなりません。その圏は、デカルト圏にさらに構造が載ったものです。圏全体はデカルト圏で、特定された部分圏には余デカルト構造が入り半加法圏となっています(次節で記述)。このような構造には(僕は)初めて出会いました。それ自身、なかなか興味深いです。

非関手的・非自然な手法が活躍する。

以下に挙げる過去記事(割と最近)で、非関手的・非自然な手法を説明しました。それらの手法の構成素には、圏論的モダリティ、圏論的コンストラクタ、圏論的オペレータなどがあります*4

前段落で述べた「外側のデカルト圏と半加法的な部分圏」という構造を定義するには、圏論的モダリティが便利です。また、圏の対象Xにその線形化(linearization; または線形台 linear carrier)という対象L(X)を対応させる操作は圏論的コンストラクタです。圏上のヤコビ微分圏論的オペレータになります。ヤコビ微分圏は、非関手的・非自然な手法が活躍する事例としての意味があります。

準半加法圏など

ヤコビ微分圏の定義・構成が面倒になる理由は、下部構造の圏が単なるデカルト圏では済まないからです。ヤコビ微分圏の土台になる圏を準半加法圏(qusi-semiadditive category)と呼ぶことにします。「準半」て何だよそれ? と言われそうですが、「準半」に前例がないわけでもありません。

なんでこんな変な名前を付けざるを得ないのか? 「「余」と「双」の使い方がバラバラ」で愚痴ったことがありますが、「双デカルト圏」、「加法圏」、「半加法圏」のあたりは、圏論定義と用語法が腐っているところで、混乱必至。ですが、致し方ないので慣用の用語法に従うとすると、双積(biproduct)を持つ圏が半加法圏(semiadditive category)となります -- これはろくでもないネーミングだと思うんだけど…

それで、ヤコビ微分圏のために必要な圏は、一部分だけが半加法圏となっているデカルト圏です。「一部分だけ」を表す言葉にpartialがあるので、"partially semiadditive category"とかでも良さそうですが、partial/partiallyは、「偏微分」の「偏」として「複数変数のなかの特定変数に関してだけ」の意味で使いたいので温存したい。で、「完全には半加法圏ではない」から"quasi"を前置して"qusi-semiadditive category"=「準半加法圏」になったわけ。トホホホ。

準半加法圏は部分圏(充満部分圏ではない)として半加法圏を持つので、この半加法的部分圏のなかで線形代数ができます。次のような言葉の置き換えをすればイメージが掴めるでしょう。

  • 半加法的部分圏の対象 → ベクトル空間
  • 半加法的部分圏の射 → 線形写像

実際クラットウェルは、現状の用語法は無視して、半加法的対象と射を「線形対象」「線形射」と呼んでいます -- それもアリかも知れません。(現状の用語法に拘らないなら、準半加法圏は準線形デカルト圏であり、線形部分圏を持つ、と言えます。)

まーともかく、準半加法圏は、線形代数ができる部分圏(半加法圏)を持つわけです。しかし、行列概念の定義にはデカルト閉構造(の変種)も必要です。閉構造は外側のデカルト圏全体に存在するわけではなくて、半加法的部分圏が閉構造を持つのです。うーん、「閉」をどこに付けたらいいのかな? 準閉半加法圏? 閉準半加法圏? 準半加法閉圏? ハァー(ため息)、現状の用語法に合わせるのも限界かも。

ヤコビ微分圏の抽象的構成・具体的構成

前節で述べたように、ヤコビ微分圏の面倒な部分は土台になる圏の構成です。逆に言うと、土台になる圏を構成してその性質を十分調べておけば、微分オペレータは割と簡単です。古典的微分計算と対応付けたり、絵による微分計算(微分絵算)も出来るでしょう。

絵図主義者(picturalist)には朗報なんですが、微分圏は絵算と意外に相性がいいです。絵算の創始者の一人であるペンローズは、テンソルの代数計算だけでなく、テンソル場の微分計算も(ペンローズ・ヒエログリフとも呼ばれる)彼の図式法で遂行していたので、微分も絵で描けることもむべなるかなです。

*5

ヤコビ微分圏の典型的な事例は、ユークリッド空間の開集合と、その上で定義された無限回微分可能写像の圏です。各点のヤコビ行列により導関数微分オペレータを定義します -- これがまさにヤコビ微分です。この事例をうまく説明し、今まで見えにくかった構造に光を当てることが出来れば、ヤコビ微分圏の最初の目標はクリアしたと言えるでしょう。

ここまで、ヤコビ微分圏のご利益や周辺事情やロードマップを述べましたが、実質的内容には踏み込んでいません。たぶん、引き続く記事で(いつか)実際のところを話すと思います。一番の難所は錯綜した用語法の整理と選択かも知れません。

*1:現状では、キラーアプリケーションが見当たりません。めざましい応用例がないと、「ちょっと面白かったけど、結局、役に立たなかったね」となる危惧もあります。

*2:僕の感覚では -- つまり、合理的な説明がうまく出来ないのですが -- オリジナルのデカルト微分圏の定義は良くない、と思えます。使い勝手が悪いだけでなく、なにか外している感覚があります。

*3:これらのことを手っ取り早く知りたいなら、次のスライドがあります。Differential Join Restriction Categories, Differential Categories to Tangential Structure, Tangent categories are locally Cartesian differential categories

*4:他に関連記事として、「余可換コモノイド・モダリティ事件の解説」、「天空の支配者」。

*5:画像は、Wikipedia項目"Penrose_graphical_notation"より

トラックバック - http://d.hatena.ne.jp/m-hiyama/20170510

2017-05-08 (月)

圏論的コンストラクタと圏論的オペレータ: 関手性・自然性の呪縛からの脱却

| 12:24 | 圏論的コンストラクタと圏論的オペレータ: 関手性・自然性の呪縛からの脱却を含むブックマーク

圏論で関手と自然変換が重要なのは言うまでもありません。しかし、これらに拘り過ぎるのもマズイのではないか、と思います。プログラミングにおける型構成子や総称関数は、関手・自然変換に対応しないことがままあります。トレースや不動点オペレータは、関手・自然変換ではないけど重要な圏論的構成素です。非関手的対応、非自然な変換も積極的に使いましょう。

内容:

  1. 圏論的コンストラクタと圏論的オペレータとは何か
  2. 関手・自然変換の一部を見ているとき
  3. トレース、不動点微分
  4. モナドデカルト圏、コンパクト閉圏
  5. おわりに

圏論的コンストラクタと圏論的オペレータとは何か

最近、CADG(Categorical Abstract Differential Geometry)をまた調べています。CADGは十分な一般性を持つアブストラクト・ナンセンス(いい意味で)であり、複雑で多様な構成を必要とします。こういう状況では、関手でも自然変換でもないようなシロモノが色々と登場します。

先月、関手でも自然変換でもないようなモノを使う枠組みとして圏論的モダリティを紹介しました。モダリティを構成する素材として、非全域関手と非自然変換を説明しましたが、少し別な観点から、またこの記事で非全域・非自然なモノを解説します。

CDが圏のとき、|C|→|D|、または |C|→Mor(D) の形の写像圏論的コンストラクタ(categorical constructor)と呼びましょう。典型的な例は、プログラミングにおける型構成子(type constructor)です。例えばリスト型構成子は、型Xに対して、Xのリスト型List(X)(プログラミングではList<X>と書くことが多い)を対応させます。型引数を持つ総称関数は、|C|→Mor(D) のタイプの圏論的コンストラクタになります。例えば、id<X> は、型(圏の対象)Xに“Xの恒等関数”を対応させる圏論的コンストラクタとみなせます。

Cが幾つかの圏の直積圏のときを考えましょう。C = C1×...×Cn とします。このとき、C上で定義されたコンストラクタは、|C1|×...×|Cn|→D または |C1|×...×|Cn|→Mor(D) の形です。プログラミングでは、幾つかの型引数を持つ型構成子/総称関数が、直積圏上の(圏論的)コンストラクタに対応します。例えば、2つのベクトル空間V, Wに対して、VからWへのゼロ線形写像をOV,Wとすると、V, W|→OV,Wは2つの対象にひとつの射を対応させるコンストラクタです。

圏論的コンストラクタは対象全域で定義される必要はありません。例えば、順序集合の圏Ordで、「対象Xの最小元を指定する」という操作を考えてみます。これは付点モダリティの例になります。Xに最小元があれば、⊥X:1→X が決まります。しかし、最小元がない順序集合はいくらでもあるので、X|→⊥X : |Ord|→Mor(Ord) は部分的にしか定義されません。

圏の射に射を対応させる写像圏論的オペレータ(categorical operator)と呼びましょう。圏論的オペレータは、圏論コンビネータ(categorical combinator)とも呼びます。この文脈での「オペレータ」と「コンビネータ」は同義語です。ただし、「圏論コンビネータ」というと、S, K, Iなどを圏論的にゴニョゴニョすることだと思う人が多いので、主に「オペレータ」を使うことにします。「オペレータ」という言葉も多義的で曖昧なのですが、まーしょうがない。

例えば、A, B, Cを集合として、集合圏Setにおけるカリー化 (f:A×B→C)|→(Λ(f):A→CB) を考えてみましょう。これは、ΛA,B,C:Set(A×B, C)→Set(A, CB) という集合(Setの対象)3つで添字付けられた写像の族です。このように、圏論的オペレータの実体は、ホムセットのあいだの写像として与えられます。圏Cの構造を与える結合(composition)も、γA,B,C:C(A, B)×C(B, C)→C(A, C) という形の圏論的オペレータです。

圏論的オペレータは、シーケント計算の推論規則の形に書けます(「圏論の筆算としてのシーケント計算」参照)。直積をカンマ、指数(関数空間)を含意記号'⊃'で書くとして、カリー化は:

  A, B ⇒ C
 -----------[Curry = 左含意導入]
  A ⇒ B⊃C

圏の結合なら:

 A ⇒ B    B ⇒ C
 -----------------[Comp = カット]
     A ⇒ C

コンストラクタのなかには、シーケント計算の公理の形に書けるものもあります。A|→idA はそのようなコンストラクタです。

     *(前提なし)
 ---------------[Id = 同一律]
    A ⇒ A

圏論的コンストラクタと圏論的オペレータの区別は必ずしも明確ではありませんし、明確にする必要もないでしょう。関手の射部分(morphism part)をホムセットごとの関数で表した FX,Y:C(X, Y)→D(F(X), F(Y)) は、射から射を作り出しているので圏論的オペレータですが、|C|×|C|→Mor(Set) の形のコンストラクタだとも言えます。おおよその分類基準を書いておくと:

  • 対象のコンストラクタ: いくつか(0個, 1個, 2個, ...)の対象に対して対象を対応させる。
  • 射のコンストラクタ: いくつか(0個, 1個, 2個, ...)の対象に対してを対応させる。
  • オペレータ: いくつか(0個, 1個, 2個, ...)のに対してを対応させる。

関手・自然変換の一部を見ているとき

圏論的コンストラクタ、圏論的オペレータが関手・自然変換を定義しても、もちろんかまいません。実際には関手・自然変換なのだが、関手性・自然性に気付かないでいることもあります。

デカルト閉圏Cにおけるカリー化オペレータ ΛA,B,C:C(A×B, C)→C(A, CB) は、Bを固定してA, Cを動かせば、関手 (-)×B と (-)B のあいだの随伴性を主張しているので、自然同型(成分が同型である自然変換)です。しかし、カリー化が自然変換だと知らないで使っている場合もあるだろうし、自然性なしでも役に立ちます。

カリー化と一緒に使う評価射 evA,B:A×BA→B も、随伴性を構成する余単位自然変換ですが、カリー化との関係を理解していれば、2つの添字A, Bを持つ射の族としての扱いでも十分なことも多いです。

リスト型構成子 X|→List(X) や直積型構成子 X, Y|→X×Y も関手・二項関手に拡張できます。リスト型構構成子はリスト・モナドの一部となり、直積型構成子はデカルト・モノイド積関手の一部になります。モナドデカルト構造は関手概念を使わない定式化もあります(後述)。具体的な計算の場面では、コンストラクタ/オペレータの形のほうが使いやすかったりします。

関手性・自然性を見つけることは非常に重要ですが、関手性・自然性が明らかでないときは、とりあえずはコンストラクタ/オペレータ(コンビネータ)/モダリティとして定式化して調べるのが得策だと思います。どうやっても関手・自然変換にならなくても、役に立ってくれることもあります。

トレース、不動点微分

よく知られた圏論的オペレータにトレース・オペレータと不動点オペレータがあります。これらのオペレータの下部構造として対称モノイド圏が要求されます。トレース・オペレータTrと不動点オペレータFixは次の形をしています。

   f : A¥otimesX → B¥otimesX
 --------------------
  TrA,BX(f) : A → B

   f : A¥otimesX → X
 --------------------
  FixAX(f) : A → X

CADG(圏論的抽象微分幾何)に登場する微分オペレータを、一般化デカルト微分圏(generalized Cartesian differential category)で定式化した場合は次のようになります。Lは圏論的コンストラクタで、対象Xの線形化と呼ばれるモノがL(X)です。

   f : X → Y
 --------------------------
  DX,Y(f) : L(X)×X → L(Y)

トレース/不動点オペレータについては、過去に説明したことがあるので、それらの記事を参照してください(下のリスト)。トレース/不動点オペレータは、部分的な自然性や変形された自然性(対角自然性)を持ちますが、単なる自然変換として説明することはできません。

CADGの微分オペレータ(微分コンビネータ)については、いずれまた述べる機会があるでしょう。

モナドデカルト圏、コンパクト閉圏

モナド

モナドの定義には、クライスリ拡張(Kleisli extension)を使うスタイルがあります。このスタイルを使う場合のモナドの構成素は:

  1. 型構成子 X|→T(X)
  2. 総称関数 ηX:X→T(X)
  3. f:X→T(Y) の形の関数に働く高階総称関数(これがクライスリ拡張) (-)# 、f#:T(X)→T(Y)

Tは“値が対象であるコンストラクタ”、ηは“値が射であるコンストラクタ”、(-)#は“オペレータ”です。拡張オペレータはほんとは添字付きで (-)#X,Y:C(X, T(Y))→C(T(X), T(Y)) です。これらのコンストラクタ/オペレータのあいだの条件(公理)によりモナドが定義されます。

デカルト

デカルト圏を定義するには幾つものやり方がありますが、そのなかのひとつでは次の構成素を使います。

  1. 対象に対してだけ定義された直積 X, Y|→X×Y
  2. 対象X, Yに対して一意に定義された射 π1X,Y:X×Y→X と π2X,Y:X×Y→Y
  3. 特定された対象1
  4. 対象Xに対して一意に定義された射 !X:X→1
  5. f:X→Y, g:X→Z という形の射に対して定義されたデカルト・ペアリング <-, -> 、<f, g>X,Y,Z:X→Y×Z

直積×は“ニ変項のコンストラクタ”、π1, π1は“添字を2つを持つ射のコンストラクタ”、!は“添字を1つ持つ射のコンストラクタ”、<-, ->は“ニ変項(入力の射が2つ)のオペレータ”です。デカルト・ペアリング・オペレータを添字付きで書けば、<-, ->X,Y,Z:C(X, Y)×C(X, Z)→C(X, Y×Z) 。これらのコンストラクタ/オペレータのあいだの条件(公理)によりデカルト圏が定義されます。

コンパクト閉圏

C = (C, ¥otimes, I) は対称モノイド圏であるとして、Cにコンパクト閉構造を載せることを考えましょう。そのとき、次の構成素を追加します。

  1. 対象Xに対して一意に定義された対象X*、Xの双対対象
  2. 対象Xに対して一意に定義された射 ηX:I→X*¥otimesX 、双対の単位
  3. 対象Xに対して一意に定義された射 εX:X¥otimesX*→I 、双対の余単位

(-)*は“コンストラクタ”、ηとεは“射を値とするコンストラクタ”です。これらのコンストラクタ/オペレータのあいだに条件を課します。その条件から、結果的に(-)*は反変関手に拡張できて、η, εも自然変換だとみなせますが、最初から関手性・自然性を仮定する必要はありません。

おわりに

ここで僕が言いたいことは、我々に必要な操作・構成がすべて関手・自然変換であるとは限らないことです。また、最終的には関手・自然変換だと判明するにしても、最初からその姿で現れないかも知れません。そのような操作・構成の定式化に圏論的コンストラクタ/圏論的オペレータが有効です。

コンストラクタ/オペレータは、プログラミングの型構成子/総称関数/高階総称関数などに対応するので、プログラミング的(運算的; calculational)な概念になります。このため、計算には有利となることもあります。

圏論的コンストラクタ/圏論的オペレータは、非全域関手/非自然変換の利用形態のなかで頻出するパターンを取り出して名付けたものです。非全域関手/非自然変換は組織化されて圏論的モダリティとなります。モダリティは、必ずしも関手・自然変換とは限らないメカニズムを使って、圏上の構造を定義する手法です。圏論的モダリティは、圏論の枠内で複雑さ/多様さ(あるいは“汚さ”)をうまく処理してくれます。

2017-05-01 (月)

天空の支配者

| 15:48 | 天空の支配者を含むブックマーク

上空にいる足し算の親玉を捕まえる」で次のように書きました。

雰囲気的に言うと、地上の圏Cの足し算構造を、上空にあるメタ圏内のただひとつの代数系が支配していることになります。

この「上空にいる親玉」を、もっと小洒落た呼び方をしたい、と。で、「天空の支配者」はどうかな、と。天空を支配する者ではなくて、天空にいて地上を支配している者を指します。「天空の城」(ラピュタ)の英訳が"Castle in the Sky"らしいから、"Ruler in the Sky"かな。

支配者、あるいは統御構造の実体は何かというと、最近言い出した圏論的モダリティというヤツです。

モダリティは、関手と自然変換の制約をゆるくしたもので非全域性と非自然性を許します。特に全域かつ自然であるモダリティは従来の関手と自然変換による構造になります。

連休の期間、CADG (Categorical Abstract Differential Geometry)に対する天空の支配者を探そう、と思っています。モダリティによる定式化は、複雑で錯綜した状況を整理するのに役立つので、圏上の微分構造(differential structure)/接構造(tangent structure)にも有効そうです。

“圏上の微分構造/接構造=CADG”は、去年(2016年)の夏に調べたことがありますが、なめらかな多様体の圏やベクトルバンドルの圏の上空に幾つものモナドやコモナドが居るような構造だと思われます。さらに、モナド/コモナドを構成するもっと細かい構成素があり、それらが天空の支配者として君臨している気がしています。今は「思われる/気がしている」状況なので、天空を眺めて支配者を捕捉したいな、というわけ。

2017-04-26 (水)

余可換コモノイド・モダリティ事件の解説

| 12:35 | 余可換コモノイド・モダリティ事件の解説を含むブックマーク

一昨日の記事「圏論的モダリティ:圏上の非自然な構造達」の「僕のモダリティ経験」の節で:

試しに、非負実数係数のテンソルの圏に余可換コモノイド・モダリティを入れてみると、そのモダリティと整合する部分圏として部分性と確率的非決定性の両方がうまく定義できるようです。これが分かったとき、僕にとってはA-ha momentでした。

非全域関手と非自然変換」にて:

特に役に立つのは、2つの非自然変換から構成される余可換コモノイド・モダリティです。余可換コモノイド・モダリティの事例はそのうち述べるつもりです。

予告に従い、余可換コモノイド・モダリティの事例について述べます。タイトルに「事例」でなく「事件」と付けているのは、これから述べることが僕には思いがけないことだったからです。

内容:

  1. 余可換コモノイド・モダリティが定義する部分圏、不思議だ
  2. 余可換コモノイド・モダリティ
  3. 集合圏の余可換コモノイド・モダリティ
  4. 関係圏の余可換コモノイド・モダリティ
  5. モダリティと単葉関係/全域関係
  6. 非負実数係数テンソルとその圏
  7. 非負実数テンソルの圏の余可換コモノイド・モダリティ
  8. モダリティと非分散テンソル/マルコフ・テンソル
  9. 参考文献

余可換コモノイド・モダリティが定義する部分圏、不思議だ

池尻大橋駅から10秒くらいの近さのカフェ・ベローチェで、割と何となくナプキンペーパーで計算していたのですが、計算結果を見て「エッ?!」と驚きました。事前に予想も期待もしてなかった結果だったからです。これが、僕が余可換コモノイド・モダリティに興味を持つキッカケとなった「事件」(大げさだけど)です。詳しい説明は後の節でしますが、概要だけこの節で言っておきます。

係数(成分)が非負実数であるテンソル(幾つかの数を適当な次元の矩形状に並べたモノ)を考えます。非負実数係数のテンソルに関して次の言葉を使いますが、これらは後で定義します。

すべての非負実数(係数の)テンソルから構成される圏NNTens(non-negative (coefficient) tensors)に、自明と思える簡単なモダリティΔ(余乗法)とε(余単位)を入れると:

  1. Δと整合する射の全体は、非分散ブール・テンソルの全体と一致する。Δと整合する射が作るNNTensの部分圏は、有限集合を対象とする部分写像の圏FinPartialと同型である。
  2. εと整合する射の全体は、マルコフ・テンソルの全体と一致する。εと整合する射が作るNNTensの部分圏は、有限離散測度空間を対象とするマルコフ核(別名 stochastic map/kernel/relation)の圏FinStockと同型である。
  3. Δとεの両方と整合する射の全体は、非分散ブールかつマルコフなテンソルの全体と一致する。Δ, εと整合する射が作るNNTensの部分圏は、有限集合と写像の圏FinSetと同型である。

これと似た結果は関係圏Relでも成立します。関係に関する次の言葉も後で定義します。

  • 単葉(一価)関係(univalent relation)
  • 全域関係(total relation)

Relにおける余乗法と余単位も同じ記号Δ, εで表すとして:

  1. Δと整合する射の全体は、単葉な関係の全体と一致する。Δと整合する射が作るRelの部分圏は、部分写像(partial map)の圏Partialと同型である。
  2. εと整合する射の全体は、全域な関係の全体と一致する。
  3. Δとεの両方と整合する射の全体は、単葉かつ全域な関係の全体と一致する。Δ, εと整合する射が作るRelの部分圏は、集合と写像の圏Setと同型である。

うーん? なんでこんな現象が起きるのだろう? 内在的必然性とか背後のメカニズムとかはサッパリ分かりません。不思議だが本当だ。

Δとεの組み合わせは余可換コモノイド・モダリティとなります。経験則として、このモダリティ(Δ, ε)の一部または全部と整合する射を考えることは、面白い部分圏を抽出する手段として有効だ、とは言えそうです。理由は分からんけど。

余可換コモノイド・モダリティ

C = (C, ¥otimes, I, α, λ, ρ, σ) を対称モノイド圏とします。α, λ, ρはそれぞれ、結合律子(associator)、左単位律子(left unitor)、右単位律子(right unitor)、対称(symmetry)です(律子に関しては「律子からカタストロフへ」を参照)。

一般に、Cの対象Aに対して、自己関手 KA:CC はすべての対象をAに移し、すべての射をidAに移す“定数関手”とします。また Sq:CC は、対象も射もモノイド積の意味で平方(二乗)する関手です。

  • KA(X) = A, KA(f) = idA
  • Sq(X) = X¥otimesX, Sq(f) = f¥otimesf

モノイド単位対象Iに対する定数関手KIと平方関手Sqを考えます。この2つは、非全域関手ではなくて普通の(全域な)関手です。さらに非自然変換 Δ::Id ?⇒ Sq :CC と ε::Id ?⇒ KI :CC を考えます。ここで、IdはCの恒等関手です。特殊な矢印記号'?⇒'は、非自然(必ずしも自然ではない)ことを表します。このへんのところは「非全域関手と非自然変換」を参照。

非自然変換Δ, εの、対象Xにおける成分は次の形です。

  • ΔX:X→X¥otimesX in C
  • εX:X→I in C

2つの非自然変換Δとεの組み合わせ(Δ, ε)が余可換コモノイド・モダリティであるとは、任意の対象Xに対して、3つ組 (X, ΔX, εX) が余可換コモノイドになることです。他に、Δとεが圏のモノイド構造と調和するための一貫性条件も要求します。

余可換コモノイドの公理は昨日の記事の「対称モノイド圏の余可換コモノイド・モダリティ」に載せています。ここでは、図を描いておきましょう。余乗法Δは分岐の黒丸、余単位εはストッパーの横棒のアイコンで示すことにします。射の描画方向は ↓→ です。

余結合律、左余単位律、右余結合律、余可換律は次のとおりです。idXを単にXと書き、律子(構造同型射)α, λ, ρによる細かい調整は省略しています。

Δとεとモノイド積/モノイド単位との一貫性(調和性)は次の等式で表現できます。

  1. ΔX⊗Y = (ΔX¥otimesΔY);(X¥otimesσX,Y¥otimesY)
  2. εX⊗Y = εX¥otimesεY
  3. εI = idI

絵なら次のようです。点線は、モノイド単位対象を表す“空なワイヤー”です。

また、f:X→Y in C が“Δと整合すること”と“εと整合すること”は次の図で表せます。

集合圏の余可換コモノイド・モダリティ

集合圏Setに対して、余可換コモノイド・モダリティを定義します。集合圏のモノイド積は直積(記号'×')、モノイド単位対象は 1 = {0} とします。Δ, εを次のように定義します。

  • ΔX:X→X×X, ΔX(x) = (x, x)
  • εX:X→1, εX(x) = 0

集合Xごとの(X, ΔX, εX)が余可換コモノイドになること、そして一貫性条件を満たすことを確認してみてください。

集合圏Setの余可換コモノイド・モダリティでは、すべての射(集合のあいだの写像)がモダリティと整合します。つまり、f:X→Y in Set に対して:

  • f;ΔY = ΔX;(f×f) : X→Y×Y
  • f;εY = εX : X→1

これも簡単に確認できます。

結局、今定義した集合圏の余可換コモノイド・モダリティ(Δ, ε)では、Δもεも自然変換になります。自然変換は非自然変換の特別なものなので問題はありませんが、モダリティと整合する射として部分圏を抽出することは出来ません。部分圏を作る目的から言えば、自然な全域モダリティは役立たずなのです。

余可換コモノイド・モダリティが自然変換になっている状況は、実はモノイド積が直積(デカルト積)になっている場合に限られます。次の定理があります。

  • 対称モノイド圏Cに余可換コモノイド・モダリティ(Δ, ε)があり、Δとεが自然変換のとき、モノイド積は直積(デカルト積)である。

証明は割愛しますが、このことから、直積ではないモノイド積を持つ対称モノイド圏では、自然変換で与えられる余可換コモノイド・モダリティは存在しないことになります。モダリティが欲しかったら、非自然なものを許すしかないのです。これは、非自然性に関する重要な知見です。

関係圏の余可換コモノイド・モダリティ

次に、関係圏Relに余可換コモノイド・モダリティを入れましょう。関係圏のモノイド積も直積(記号'×')、モノイド単位対象は 1 = {0} です。Δとεも集合圏と同じですが、表現の仕方は少し違います。

  • ΔX:X→(X×X), ΔX = {(x, (x', x''))∈X×(X×X) | x = x' = x''} = {(x, (x, x))∈X×(X×X) | x∈X}
  • εX:X→1, εX = {(x, 0)∈X×1 | xは任意(無条件)} = X×1

集合Xごとの(X, ΔX, εX)が関係圏において余可換コモノイドになることも、そして一貫性も、集合圏のときと同様に確認できます。

集合圏とは違い、関係圏の射はΔ, εと整合するとは限りません。t:{1, 2}→{1, 2} in Rel を次のように定義します。

  • t = {(1, 1), (1, 2)}

このtでは、t;Δ{1, 2} = Δ{1, 2};(t×t) は成立しないし、t;ε{1, 2} = ε{1, 2} も成立しません。具体的に計算すれば分かります。

  • t;Δ{1, 2} = {(1, 1), (1, 2)};{(1, (1, 1)), (2, (2, 2))} = {(1, (1, 1)), (1, (2, 2))}
  • Δ{1, 2};(t×t) = {(1, (1, 1)), (2, (2, 2))};{((1, 1), (1, 1)), ((1, 1), (1, 2)), ((1, 2), (1, 1)), ((1, 2), (1, 2))} = {(1, (1, 1)), (1, (1, 2))}
  • t;ε{1, 2} = {(1, 1), (1, 2)};{(1, 0), (2, 0)} = {(1, 0)}
  • ε{1, 2} = {(1, 0), (2, 0)}

以上の計算から、

  • t;Δ{1, 2} ≠ Δ{1, 2};(t×t)
  • t;ε{1, 2} ≠ ε{1, 2}

t = {(1, 1), (1, 2)} は、Δともεとも整合しない射です。

モダリティと単葉関係/全域関係

関係圏Relにおいて、どのような射がΔ, εと整合するかを見ておきましょう。

r:X→Y in Rel がΔと整合するとします。このとき、r;ΔY = ΔX;(r×r) : X→Y×Y in Rel が成立します。等式の左辺/右辺を具体的に書き下してみます。

   r;ΔY
 = {(x, y)∈X×Y | (x, y)∈r};{(y, (y', y''))∈Y×(Y×Y) | y = y' = y''}
 = {(x, y)∈X×Y | (x, y)∈r};{(y, (y, y'))∈Y×(Y×Y) | y = y'}
 = {(x, (y, y'))∈X×(Y×Y) | (x, y)∈r かつ y = y'}

   ΔX;(r×r)
 = {(x, (x, x))∈X×(X×X) | x∈X};{((x, x'), (y, y'))∈(X×X)×(Y×Y) | (x, y)∈r かつ (x', y')∈r}
 = {(x, (y, y'))∈X×(Y×Y) | (x, y)∈r かつ (x, y')∈r}

r;ΔY = ΔX;(r×r) であるためには:

  • (x, y)∈r かつ y = y' ⇔ (x, y)∈r かつ (x, y')∈r

⇒方向は自明なので、実質的な条件は:

  • (x, y)∈r かつ (x, y')∈r ⇒ y = y'

この条件を満たす関係 r:X→Y in Rel単葉(univalent, 一価)な関係と呼びます。したがって、

  • 関係rがΔと整合する ⇔ rは単葉関係である

次に、r:X→Y in Rel がεと整合するとします。このとき、r;εY = εX : X→1 in Rel が成立します。等式の左辺/右辺を具体的に書き下してみます。

   r;εY
 = {(x, y)∈X×Y | (x, y)∈r};{(y, 0)∈Y×1 | yは任意}
 = {(x, 0)∈X×1 | xに対して、(x, y)∈r となる y∈Y が存在する}

   εX
 = {(x, 0)∈X×1 | xは任意}

r;εY = εX であるためには:

  • xに対して、(x, y)∈r となる y∈Y が存在する ⇔ xは任意

言い換えれば:

  • 任意のxに対して、(x, y)∈r となる y∈Y が存在する

この条件を満たす関係 r:X→Y in Rel全域(total)な関係と呼びます。したがって、

  • 関係rがεと整合する ⇔ rは全域関係である

Δとεの両方と整合する関係(Relの射)は、単葉かつ全域な関係となります。単葉かつ全域な関係は、写像だと思ってもかまいません。つまり、関係圏Relの部分圏として集合と写像の圏を再現しています。この部分圏に制限すれば、Δとεは自然変換になるので、部分圏上に自然な余可換コモノイド・モダリティが載ります。自然な余可換コモノイド・モダリティは直積(デカルト構造)を定義するので、この部分圏に制限したモノイド積が直積を与えることも分かります。

デカルト圏(直積/終対象を持つ圏)と、そのデカルト圏を拡張したモノイド圏の組としてはフレイド圏(Freyd category)があります。余可換コモノイド・モダリティを持った対称モノイド圏は、フレイド圏とかなり似ています。そういえば、フレイド圏に非自然な対角や余対角を載せることはやったことがありました。

プレモノイド圏やバイノイド圏は、関手性が破れた積を扱う仕組みでした。どうも、非関手的(no-fanctorial)/非自然(non-natural)な対応や族を扱う必然性はありそうです。モダリティは、非関手的/非自然な構造を扱う道具になる気がします。

非負実数係数テンソルとその圏

これから、係数(成分)が非負実数であるテンソルと、そのようなテンソルを射とする圏NNTens(category of non-negative tensors)に関して手早く(あるいは雑に)説明します。そして、次のような、特別な種類のテンソルを定義します。

R≧0を非負実数の全体とします。以下、X, Y, Zなどは有限集合を表すとします。写像 f:X×Y→R≧0非負実数(係数の)テンソル(non-negative (coefficient) tensor)と呼びます。fをテンソルとして扱うときは、f(x, y)をf[x→y]またはf[x←y]と書くことにします。また、f = (f[x→y] | x∈X, y∈Y) という書き方も用います。これは、行列の成分表示と同じだと思えばいいです。

f = (f[x→y] | x∈X, y∈Y) のテンソルとしてのプロファイルは、X→Y だとします。fは2つの見方ができます。2つの見方を適宜切り替えます。

f = (f[x→y] | x∈X, y∈Y), g = (g[y→z] | y∈Y, z∈Z) のテンソルとしての結合f;gは次のように定義します。

  • (f;g)[x→z] = Σ(y∈Y | f[x→y]g[y→z])

有限集合Xに対する恒等テンソルidXは:

  • idX[x→x'] = (if x = x' then 1 else 0)

idXの成分表示は、クロネッカーのデルタδ[x→x']を使うことも多いです。つまり、idX = (δ[x→x'] | x∈X, x'∈X) 。

ここまでの定義では、添字集合に任意の有限集合を許した行列とテンソルの差はありません。テンソルと呼ぶのは、X = X1×...×Xn, Y = Y1×...×Ym のようなときに、f = (f[x1, ..., xn→y1, ..., ym] | x1∈X1, ..., xn∈Xn, y1∈Y1, ..., ym∈Ym) という表現を使うからです。テンソルの具体的な計算例は、「確率的推論・判断の計算法:マルコフ・テンソル絵算」にあります。ブラケット内の x1, ..., xn→y1, ..., ym で、矢印よりカンマが優先される(結合度が強い)ので注意してください。

非分散テンソル

f:X→Y in NNTens のとき、a∈X に対して次の性質を定義します。

  • fがaで消失するとは、すべてのy∈Yに対して、f[a→y] = 0 のこと。
  • fがaで分散(または分岐)するとは、f[a→y'] ≠ 0 かつ f[a→y''] ≠ 0 かつ y' ≠ y'' であるy', y''が存在すること。

消失と分散を否定すると:

  • fがaで消失しないとは、f[a→y] ≠ 0 となるyが存在すること。
  • fがaで分散しない(または分岐しない)とは、任意のy', y''に対して、y' ≠ y'' であるならば、f[a→y'] = 0 または f[a→y''] = 0 となること。

任意のx∈Xに対してxで分散しないテンソル非分散テンソル(nondispersive tensor)と呼ぶことにします。非分散テンソルは消失を禁止してないので、Xの一部でfは消失しているかも知れません。

ブール・テンソル

テンソルの係数が0か1のどちらかの場合、0をfalse、1をtrueと思うとブール値なので、ブール・テンソル(boolean tensor, Boole tensor)と呼びましょう。ただし、計算はブール値ではなくて非負実数の計算を行うので、1 + 1 = 1 なんてことはありません。このため、ブール・テンソルの結合がブール・テンソルとは限りません。

マルコフ・テンソル(Markov tensor

テンソル f = (f[x→y] | x∈X, y∈Y) が、任意の x∈X に対して Σ(y∈Y | f[x→y]) = 1 のときマルコフ・テンソル(Markov tensor)と呼びます。「確率的推論・判断の計算法:マルコフ・テンソル絵算」の計算はすべてマルコフ・テンソルの計算です。

非負実数テンソルの圏の余可換コモノイド・モダリティ

非負実数テンソルの圏NNTensに余可換コモノイド・モダリティを入れます。NNTensのモノイド積は、対象に対しては直積(記号'×')、射に対してはテンソル積(記号'¥otimes')とします。f:X→Y, g:Z→W in NNTens のとき、f¥otimesg:X×Z→Y×W は次のように定義されます。

  • (f¥otimesg)[x, z → y, w] = f[x→y]g[z→w]

モノイド単位対象は I = {*} とします。唯一の要素を星印にしているのは、「確率的推論・判断の計算法:マルコフ・テンソル絵算」で使った u[x] = u[*→x] のような書き方に合わせるためです。

余乗法Δと余単位εは次のように定義します。

  • ΔX:X→(X×X), ΔX[x→x', x''] = (if x = x' = x'' then 1 else 0)
  • εX:X→I, εX[x→*] = 1

(Δ, ε)が余可換コモノイド・モダリティとなることを示すのは、テンソル計算のよい練習問題です。実際の計算は省略しますが、便利な略記法をここで述べておきます。

テンソルの計算では、しばしば添字を動かした総和をとります。例えば、f:X→Y×Z, g:Y→W, h:Z→W のときに k = f;(g¥otimesh) : Z→W×W を計算するとします。k[x→w, w']を求めるには総和と取ります。

  • k[x→w, w'] = Σ(y∈Y, z∈Z | f[x→y, z]g[y→w]h[z→w'])

このとき、総和を意味するΣを省略して、

  • k[x→w, w'] = (y, z | f[x→y, z]g[y→w]h[z→w'])

と書きます。これは「アインシュタインの総和規約」ですが、和を取る添字は残しています。和を取る添字を目視で判断するのがそれほど楽でではないからです。次の節の計算ではこの総和規約を使います。

モダリティと非分散テンソル/マルコフ・テンソル

非負実数テンソルの圏NNTensにおいて、どのような射がΔ, εと整合するかを調べます。僕が、池尻大橋カフェ・ベローチェのナプキンペーパーにした計算とは、これから述べる計算です。

f:X→Y in NNTens がΔと整合するとします。このとき、f;ΔY = ΔX;(f×f) : X→Y×Y in NNTens が成立します。等式の左辺/右辺を具体的に書き下してみます。

   (f;ΔY)[x→y', y'']
 = (y | f[x→y]Δ[y→y', y''])
 = if y = y' = y'' then f[x, y] else 0

   (ΔX;(f×f))[x→y', y'']
 = (x', x'' | Δ[x→x', x'']f[x'→y']f[x''→y''])
 = if x = x' = x'' then f[x→y']f[x→y''] else 0

整合性は次の等式となります。

  • (if y = y' = y'' then f[x, y] else 0) = (if x = x' = x'' then f[x→y']f[x→y''] else 0)

等式の両辺が等しくなるためには、y' = y'' 以外の部分では、(右辺のテンソル)[x→y', y''] = 0 です。したがって、次が成立します。

  • y' ≠ y'' ならば、f[x→y']f[x→y''] = 0

fの係数(成分)は非負実数なので:

  • f[x→y']f[x→y''] = 0 ⇔ f[x→y'] = 0 または f[x→y''] = 0

結局、

  • y' ≠ y'' ならば、 f[x→y'] = 0 または f[x→y''] = 0

これが任意のxに対して成立するので、fは非分散テンソルです。

また、y' = y''( = y) である部分に関しても、次の制約があります。

  • f[x, y] = f[x→y']f[x→y'']

y = y' = y'' なので、

  • f[x, y] = (f[x→y])2

これは、f[x→y] = 0 または f[x→y] = 1 を意味するので、fはブール・テンソルです。

これで、f:X→Y in NNTens がΔと整合することは、fが非分散ブール・テンソルであることだと分かりました。x∈X に対して、f[x→y] = 1 となるyは高々1つで、残りの係数(成分)f[x→y]はすべて0です。

次に、f:X→Y in NNTens がεと整合するときを考えます。そのとき、f;εY = εX : X→I in NNTens が成立します。

   (f;εY)[x→*]
 = (y | f[x→y]ε[y→*])
 = (y | f[x→y]ε)

   εX[x→*]
 = 1

これより、(y | f[x→y]ε) = 1 がすべての x∈X で成立します。つまり、fはマルコフ・テンソルです。

Δとεの両方と整合するテンソルNNTensの射)は、非分散ブールかつマルコフなテンソルとなります。これは、x∈X に対して、f[x→y] = 1 となるyは1つだけあり、残りの係数(成分)f[x→y]はすべて0となるテンソルです。

非分散ブールかつマルコフなテンソルとは、有限集合XからYへの写像と同じことです。関係圏の場合と同様に、余可換コモノイド・モダリティ(Δ, ε)と整合する部分圏として(有限)集合と写像の圏が再現します。

参考文献

非負実数テンソルの圏NNTensには余可換コモノイド・モダリティが載ります。余可換コモノイド・モダリティ付きの圏としては、NNTensRel(関係圏)はかなり類似しています。現象としては「面白いな」と思いますが、たまたまやってみた計算が発端なので、全体の構図は見えません。よく分からなくてモヤモヤしてます。

とりあえず、ヒントになりそうな論文を挙げておきます(過去に言及した論文達ですが)。

古め(1999年)の論文ですが、色々なアイディアや話題が詰め込まれています。セリンガーが対角(diagonals)と呼んでいるものは余可換コモノイド・モダリティです。

今年(2017年)になって書かれたものだと思います。使われている絵算(pictorial/graphical/diagrammatic calculation)は、余可換コモノイド・モダリティを含むものです。測度論の晦渋な議論に入り込むのを上手に避けながらdisintegrationの計算をしています。

デカルト微分圏をはじめて(2009年頃)導入した論文です。非関手的(non-functorial)/非自然(non-natural)な構造を色々使っている点で参考になるでしょう。

2017-04-24 (月)

圏論的モダリティ:圏上の非自然な構造達

| 09:28 | 圏論的モダリティ:圏上の非自然な構造達を含むブックマーク

圏論的モダリティ(categorical modality)は、圏の対象に構造を持たせるメカニズムです。ただし、構造の素材が関手や自然変換とは限りません。モダリティは、圏の射と整合しない付加的構造を対象に導入する方法だとも言えます。

「モダリティ」という言葉は耳慣れないかも知れませんが、線形論理の意味論や微分圏では、"exponential modality", "storage modality", "resource modality", "coalgebra modality" といった言葉を使います*1。ここでは、線形論理特有のニュアンスは取り除いて、一般的な広い意味で「モダリティ」を使います*2

僕がモダリティに興味を持つ動機については最後の節に書いてあります。

内容:

  1. 集合圏の付点モダリティ
  2. ユークリッド空間のあいだのなめらかな写像の圏のベクトル空間モダリティ
  3. 圏論的モダリティの定義
  4. 対称モノイド圏の余可換コモノイド・モダリティ
  5. 僕のモダリティ経験

集合圏の付点モダリティ

集合圏Setにおいて、その対象(つまり集合)で添字付けられた射(写像)の族 θX:1→X を考えます。ここで、1 = {0} はSetの終対象である単元集合です。圏Setと、射の族 θ = (θX | X∈|Set|, X≠¥emptyset) を一緒にした(Set, θ)を考えます。

集合Xに対する θX:1→X により、Xの一点θX(0)が定まるので、空でないすべての集合が付点集合(pointed set)の構造を持ちます。ここで大事なことは、θが自然変換ではないことです。

θが自然変換 θ::(1への定数関手)⇒IdSet:SetSet なら、任意の f:X→Y in Set に対して次の図式が可換になるはずです。

1 -(θX)→ X
|        |f
↓        ↓
1 -(θY → Y

しかし、すべてのfに対して f(θX(0)) = f(θY(0)) なわけではありません。つまり、θは自然変換にはなりません

θのような、自然変換とは限らない射の族を圏論的モダリティ(categorical modality)、混乱の恐れがなければ単にモダリティと呼びます(後でもっと正確な定義を述べます)。θは、各対象に付点集合の構造を与えるので付点モダリティ(pointed-set modality)と呼ぶことにします。

f(θX(0)) = f(θY(0)) であるようなfを考えることはできます。そのようなfを付点モダリティθと整合する(consistent)射と呼びましょう。θと整合する射の全体は圏Setの部分圏を定義します。その部分圏に限定するならば、先の図式は可換となるので、θは部分圏においては自然変換となります(空集合の扱いに注意が必要ですが)。

θと整合する射の全体からなる圏は、付点集合の圏PtSetとは違います。例えば、集合{0, 1}を考えると、この集合を台集合(underlying set)とする付点集合は ({0, 1}, 0), ({0, 1}, 1) の2つがあります。どちらもPtSetの対象となります。しかし、集合{0, 1}に対するモダリティ(の成分)θ{0, 1}はひとつしかありません。θ{0, 1}で導入される付点集合は、({0, 1}, 0)か({0, 1}, 1)のどちらか一方です。

集合圏Setに付点モダリティを付けることは、空でない各集合からその要素を1個選び出す究極の選択関数の存在を仮定して、そのような選択関数を1個指定することです。

ユークリッド空間のあいだのなめらかな写像の圏のベクトル空間モダリティ

初等的な多変数微分を扱う舞台となるような圏を定義しましょう。C(Rn, Rn) は、ユークリッド空間Rnで全域的に定義されて、Rmに値を取るなめらか(無限回微分可能)な写像の全体とします。

有限次元ユークリッド空間を対象とする圏を考えたいのですが、Rn←→n と1:1対応するので、n次元ユークリッド空間の代わりに単なる整数n(n≧0)を使うことにします。その前提で、圏ESmoothを次のように定義します。(EはEuclideanのつもり。)

  • |ESmooth| = N = {0, 1, 2, ...}
  • ESmooth(n, m) = C(Rn, Rn)
  • 射の結合は、写像としての結合(合成)。
  • 恒等射idnは、RnRnの恒等写像

集合圏の場合と同様に付点モダリティθを定義します。今回のθは、次のような非常にハッキリした定義を持ちます。

  • θn:0→n in ESmooth
  • その実体は、関数 θn:R0Rn
  • R0 = {0} なので、θn(0) = (Rnのゼロ) と定義する。

θ以外に、ψ = (ψn:(n + n)→n in ESmooth | n∈N), τ = (τn:n→n in ESmooth | n∈N), μ = (μn :(1 + n)→n in ESmooth | n∈N) も定義します。

  • ψn:(n + n)→n の実体は、Rn×RnRn の足し算。
  • τn:n→n の実体 RnRn は、反ベクトル(xに対する-x)を対応させる写像
  • μn :(1 + n)→n の実体は、R×RnRn の(左からの)スカラー乗法。

(θ, ψ, τ, μ)は、ESmoothの各対象n(実体はRn)の上に、標準的なベクトル空間の構造を与えます。(θ, ψ, τ μ)を、圏ESmooth上のベクトル空間モダリティvector space modality)と呼びます。モダリティを定義するために、複数の“射の族”を使ってもかまいません。ベクトル空間モダリティでは、4つの族を使っています。

明白に書いていませんが、(θ, ψ, τ, μ)は、すべてのn(あるいはRn)において、ベクトル空間の公理を満たす必要があります(実際に満たします)。モダリティには、公理を添えてもいいのです(というか、ほとんど場合に公理も付きます)。

ESmoothの射は任意のなめらかな写像なので、ベクトル空間モダリティと整合するとは限りません。ベクトル空間モダリティと整合する射は、ユークリッド空間のあいだの線形写像です。ベクトル空間と整合する射が作るESmoothの部分圏は、行列の圏と圏同値(より強く圏同型)です。

圏論的モダリティの定義

自然変換に似ていても自然性(naturality)を持たないものを考え、それを使って改めてモダリティの定義をします。

Cを圏として、Mor(C)はCの射の集合とします。写像 ξ:|C|→Mor(C) を仮に非自然変換(non-natural transformation)と呼びましょう。これは、Cの対象で添字付けられた射の族です。S(X) := dom(ξX), T(X) := cod(ξX) と置くと、ξX:S(X)→T(X) と書けます。もちろん、S, Tは関手ではなく、関手に拡張する必要もありません。S, Tは関手である必要はありませんが、部分的に定義された関手のようなものです。さらに、ξ:|C|→Mor(C) に部分写像(未定義部分があってもいい)を許したときは、部分非自然変換(partial non-natural transformation)と呼びます。

[追記]非自然変換の定義について、別エントリー「非全域関手と非自然変換」に詳しく書きました。[/追記]

例えば、集合圏Set上の付点モダリティの θX:1→X は部分非自然変換(のX成分)です。X = ¥emptyset に対するθは定義されてないのでθは部分的です。一方、ESmooth上で定義されたθ, ξ, τ, μはいずれも全域的な非自然変換です。

C上で定義されたいくつかの非自然変換/部分非自然変換と、等式や可換図式で記述されたいくつかの公理(法則)を一緒にしたものを、圏C圏論的モダリティ、あるいは単にモダリティと呼びます。

モダリティが部分非自然変換を含む集まりで定義されているとき、そのことを強調したいなら部分モダリティ(partial modality)と呼びます。全域非自然変換だけで作られるモダリティは全域モダリティ(total modality)です。集合圏Setの付点モダリティは、空集合では定義されないので部分モダリティです。一方、ユークリッド空間のあいだのなめらかな写像の圏ESmoothの付点モダリティは全域モダリティです。

対称モノイド圏の余可換コモノイド・モダリティ

モダリティの重要な例として、対称モノイド圏の余可換コモノイド・モダリティ(cocommutative comonoid modality)を紹介します。余可換コモノイド・モダリティは、対称モノイド圏のすべての対象に余可換コモノイド構造を与えるものです。圏の射が余可換コモノイド・モダリティと整合する必要はありません。言い方を換えると、圏の射が余可換コモノイド構造に対する準同型になることは要求しないのです。

C = (C, ¥otimes, I, α, λ, ρ, σ) を対称モノイド圏とします。α, λ, ρはそれぞれ、結合律子(associator)、左単位律子(left unitor)、右単位律子(right unitor)、対称(symmetry)です(律子に関しては「律子からカタストロフへ」を参照)。対称モノイド圏Cの余可換コモノイド・モダリティの素材は、次の2つの全域非自然変換です。

  • δX:X→X¥otimesX in C
  • εX:X→I in C

δXは余乗法、εXは余単位です。これらは余可換コモノイドの公理を満たします。以下で、idXを単にXと書いています。

  • [余結合律] δX;(δX¥otimesX) = δX(X¥otimesδX)
  • [左余単位律] δX;(εX¥otimesX) = X
  • [右余単位律] δX;(X¥otimesεX) = X
  • [余可換性] δXX = δX

対称モノイド圏Cが、余可換コモノイド・モダリティ(δ, ε)を持つとき、Cの対象はすべて余可換コモノイド構造を持つことになります。しかし、Cの射が余可換コモノイド構造の準同型になることは全く保証されません。余乗法δXや余単位εXを保存(preserve, respect)しない射がたくさんあるかも知れないのです。

[追記]余可換コモノイド・モダリティの説明はコチラにもあります。[/追記]

僕のモダリティ経験

セリンガー(Peter Selinger)の1999年の論文"Categorical Structure of Asynchrony"に、対角付き(対称)モノイド圏(monoidal category with diagonals)という概念が出てきます。これは余可換コモノイド・モダリティを持つ圏と同じものです。セリンガー論文を読んだのは随分と前ですが、自然変換とはならない(かも知れない)射の族を使う方法は印象に残っています。

最近読んだ長健太(Kenta Cho)/バルト・ヤコブス*3(Bart Jacobs)の論文"Disintegration and Bayesian Inversion, Both Abstractly and Concretely"に、セリンガーの“対角”と同じ余可換コモノイド・モダリティが出てきます。

「ンン? 非同期通信/処理とベイズ確率って何か関係あるのだろうか?」と疑問に思いました。共通点があるとすれば、部分性(partiality)や非決定性(nondeterminism)です。試しに、非負実数係数のテンソルの圏に余可換コモノイド・モダリティを入れてみると、そのモダリティと整合する部分圏として部分性と確率的非決定性の両方がうまく定義できるようです。これが分かったとき、僕にとってはA-ha momentでした。


モダリティは、“対象達が持つ構造”の圏論的な定式化のひとつです。自然性を持たず、射を準同型として扱うことは出来ませんが、非自然であり部分的かも知れないことに注意すればとても便利な概念です。

非全域関手と非自然変換

| 12:30 | 非全域関手と非自然変換を含むブックマーク

圏論的モダリティ:圏上の非自然な構造達」への追記ですが、別エントリーにします。圏論的モダリティ(categorical modality)を定義するために、非自然変換(non-natural transformation)という概念を導入しました。この非自然変換の定義をここで詳しく述べます。

まず、部分的に定義された関手をpartial functorと呼ぶのですが、partial functorの訳語で悩みます。

partial = non-total なので「非全域」という言葉を使うことにします。ここでの「非全域」は「全域ではない」という意味ではありません。「必ずしも全域とは限らない」です。「非可換」というよく使う言葉も「必ずしも可換とは限らない」の意味なので、「非」のよくある用法だと思います。「非自然」も同様な解釈をします。

  • 全域関手は非全域関手の特別なもの。
  • 可換環は非可換環の特別なもの。
  • 自然変換は非自然変換の特別なもの。

よろしいでしょうか。

念のため、非全域関手をホムセット中心のスタイルで定義しておきます。Fが関手のとき、その対象部分(object part)をFobj、射部分(morphism part)をFmorとします。非全域関手では、FobjもFmorも非全域(部分的)になります。Fが非全域関手であることを詳しく言うと:

  1. C, D は圏とする。
  2. Fobj:|C|→|D| は非全域写像(部分写像)である。
  3. A, B∈|C| がFobjの定義域に入るとき、FmorA,B:C(A, B)→D(Fobj(A), Fobj(B)) が定義されるが、これも非全域写像である(必ずしも全域である必要がない)。
  4. A∈|C| がFobjの定義域に入っているなら、idAはFmorA,Aの定義域に入っている。
  5. 通常の関手と同様に、射の結合と恒等射を保存する。

対象Aに対するF(A)も、射fに対するF(f)も、定義されないことがあっても別にいい、ということです。定義されている範囲内で考えれば通常の関手と同じ扱いができます。

F, G:CD が非全域関手とします。α:|C|→Mor(D) という非全域写像が、FからGへの非自然変換だとは次のことです。

  • αA が定義されているなら、F(A)もG(A)も定義されている。
  • dom(αA) = F(A)、cod(αA) = G(A) である。

α::F⇒G と書くと、自然変換と区別が付かないので、α::F ?⇒ G とでも書けばいいかな。非全域関手であることも明示するなら、α::F ?⇒ G:C⊃→D とか。

Cの射 f:A→B in C が、非自然変換αと整合する(consistent, compatible)とは、次の図式が可換になることです。(図式内のα_AはαAのこと。)

F(A) -(α_A)→G(A)
|            |
F(f)          G(f)
↓            ↓
F(B) -(α_B)→G(B)

この可換図式が意味を持つには次の前提が必要です:

  • AもBも、αの定義域に入っている。
  • fはFA,Bの定義域にも、GA,Bの定義域にも入っている。


非全域関手や非自然変換のような変なものをなぜ考えるのでしょう? その答は「使うから」「役に立つから」です。

セリンガーの論文で非自然な構造(対角構造)を見たとき、僕も違和感を感じました。しかし、「非自然変換に整合する射」という形で既存の概念がエレガントに再定式化されるのです。特に役に立つのは、2つの非自然変換から構成される余可換コモノイド・モダリティです。余可換コモノイド・モダリティの事例はそのうち述べるつもりです。

*1:例えば、Robin Cockettの"Seely categories revisited"(http://pages.cpsc.ucalgary.ca/~robin/talks/seely.pdf)、Blute, Cockett, Seelyの"Differential categories"(http://aix1.uottawa.ca/~rblute/difftl.pdf)。

*2:モダリティの本来の意味については、例えば https://ncatlab.org/nlab/show/modality 参照。

*3:英語読みなら「バート・ジェイコブス」が近いかも知れません。

2017-04-19 (水)

確率的推論・判断の計算法:マルコフ・テンソル絵算

| 16:40 | 確率的推論・判断の計算法:マルコフ・テンソル絵算を含むブックマーク

比較的最近書いた記事「同時確率分布の圏の使用例:超具体的」、「アブダクションと確率的推論」などで触れたように、確率(真である度合)を使った推論や判断が面白な―、と思っています。

でも、確率的推論・判断のための計算ってけっこう難しいです。系統的な計算手順も必要だし、何をどう計算するかの指針を与える手法も欲しいです。ここでは、行列/テンソル計算(計算手順)とストリング図(指針策定)を使った方法を紹介します。内容的には“マルコフ・テンソルの圏”を扱うのですが、厳密な定義や根拠/背景は省略して、具体的な例題を中心に述べます。

随分と長い記事です。この記事全体のまとめや言い残したことなどを最後に書いているので、「おわりに」から先に読むのもいいかも知れません。

内容:

  1. 状況設定と問題
  2. どんな道具を使うのか:マルコフ行列
  3. 何もしないときの平均損失
  4. 行列計算で考える
  5. 薬を飲むときの平均損失
  6. 2変数損失関数の平均
  7. どんな道具を使うのか:行列の一般化
  8. どんな道具を使うのか:マルコフ・テンソル
  9. 検査を受けて判断するときの平均損失:準備
  10. マルコフ・テンソルの種類と操作
  11. 検査を受けて判断するときの平均損失:計算
  12. おわりに
  13. オマケ:マルコフ・テンソルと関数の一覧

状況設定と問題

インフルエンザのようなウィルス感染症を考えます。ただし架空の病気で、これから述べる設定はフィクションです。設定に出てくる数値は、必要なときは繰り返し引用するので覚える必要はありません。全体の状況をザッと把握してください。

このウィルスに感染してもしばらくは発病せず、発病前に治療薬(抗ウィルス剤)を飲めば発病を抑えることができます*1。また、現在感染しているかどうかの検査も行えます。

感染検査は完璧ではありません。感染していても陰性と出ることもあれば、逆に感染してないのに陽性反応が出ることもあります。検査(test)の精度は次のテーブルで表現できます。

test
感染してる 感染してない
陽性 98% 5% (誤認)
陰性 2% (誤認) 95%

治療薬もまた完璧ではありません。治療薬の効果(effect)は次のとおりです。(次のテーブルは二項述語テーブルですが、その定義は次節で。)

effect
(二項述語) 感染してる 感染してない
投与する 発病10% 発病0%
投与しない 発病80% 発病0%

感染していて薬を投与しなくても、2割の人は発病せず、何の問題もありません。

もしウィルスに感染して発病すると、苦しい思いをするし、仕事を休むなど様々なダメージを受けます。その損害を金銭に換算して10万円としましょう。検査には300円、治療薬には1000円かかるとします。

この状況で、我々の行動には次のような選択肢があるでしょう。

  1. 何もしない。
  2. 検査を受けずにとりあえず薬を飲む。
  3. 検査を受けて、もし陽性が出たら薬を飲む。

他にも行動の可能性があるでしょうが、この3つを主に考えます。検査代/治療薬代というコストと感染発病したときの損害(金銭換算)を合わせて損失(loss)と呼ぶことにして、上記3種の行動に対する損失を比較しましょう。もちろん、不確定な要素があるので、損失は確率的に評価することになります。これは、確率を考慮した平均損失を計算する問題です。

どんな道具を使うのか:マルコフ行列

確率的計算を系統的に行う上で最も重要な概念はマルコフ行列です*2。なので、マルコフ行列と、マルコフ行列のなかで特殊な形のものを紹介します。

成分が非負実数値で、各列(縦方向)の合計値が1である行列をマルコフ行列(Markov matrix)と呼びます。次の2つはマルコフ行列の例です。

¥begin{bmatrix}0.95 & 0.99 & 0.97 ¥¥ 0.05 & 0.01 & 0.03 ¥end{bmatrix}

¥begin{bmatrix}0.98 & 0.05 ¥¥ 0.02 & 0.95 ¥end{bmatrix}

1番目の行列は、「同時確率分布の圏の使用例:超具体的」で出した製造機械の不良率、2番目は今回の感染検査の精度を表す行列testです。“素の”行列では現実的意味が分からないので、この記事では見出し付きのテーブルを使って書きますが、テーブルも実質的には行列(マトリクス)です。

マルコフ行列は、条件付き確率の表現です。例えば、感染検査〈testテーブル〉の第1列(左列)に注目すると:

感染してる
陽性 98%
陰性 2% (誤認)

これは、「感染している」という条件のもとでの陽性/陰性の出現確率を表します。第2列(左列)も同様に、「感染してない」と条件を付けての陽性/陰性の確率ですね。

マルコフ行列の特殊なものとして次の形を考えます。

  • 1列だけのマルコフ行列
  • 2行だけのマルコフ行列

1列だけのマルコフ行列は確率分布(probability distribution)と呼びます。混乱の恐れがないのなら、単に分布(distribution)とも呼びます。ここでは、形状が1列であることを強調して分布列(distribution column)とも呼びます。次は分布列の例です(次節に出てきます)。

infection
*
感染してる 1%
感染してない 99%

星印('*')はダミーの見出しです。「最初の行は見出し行」という形に揃えるためですが、後で出てくる図示(ストリング図)とも揃えるためです。

2行だけのマルコフ行列で、行の2つの見出しが true/false, Yes/No の意味を持つとき、そのマルコフ行列をファジー述語(fuzzy predicate)と呼びます。混乱の恐れがないのなら、単に述語(predicate)とも呼びます。例えば、検査精度の表はファジー述語です。述語であることを明白にするために、見出しのパターンを「××, 非××」とします。例えば:

test
感染 非感染
陽性 98% 5% (誤認)
非陽性 2% (誤認) 95%

先ほどの分布列〈infection列〉も2行なので述語になっています。

infection
*
感染 1%
非感染 99%

ファジー述語もマルコフ行列なので、列の和は1です。なので、第1行だけ書けば第2行は計算(1 - x)で出ます。述語を1行だけで書くときは次のように書きます。左上の欄に註釈で「(述語)」と書いて、実際には2行であることを警告します。

test
(述語) 感染 非感染
陽性 98% 5% (誤認)

述語かつ分布列なら1個だけの欄で書けます。

infection
(述語) *
感染 1%

治療薬の効果を表すテーブルは、そのままではマルコフ行列ではありませんが、次のような形で書けばファジー述語、すなわち2行のマルコフ行列です。

effect
感染, 投与 感染, 非投与 非感染, 投与 非感染, 非投与
発病 10% 80% 0% 0%
非発病 90% 20% 100% 100%

これをさらに1行形式で書くと:

effect
(述語) 感染, 投与 感染, 非投与 非感染, 投与 非感染, 非投与
発病 10% 80% 0% 0%

横方向の4つの見出しを縦横2×2に分解した形が最初に出した〈effectテーブル〉の形です。縦横の組み合わせを引数とする述語なので、これは二項述語(binary predicate)と呼びます。「二項」の代わりに「二変数」「ニ引数」と言っても同じです。

effect
(二項述語) 感染 非感染
投与 発病10% 発病0%
非投与 発病80% 発病0%

もし、1つの欄のなかに発病と非発病を詰め込むなら:

effect
感染 非感染
投与 発病10%, 非発病90% 発病0%, 非発病100%
非投与 発病80%, 非発病20% 発病0%, 非発病100%

このテーブルをチャンと(?)書きたいなら、3次元のテーブル(キューブ)にすべきなんです。{発病, 非発病}を第3の方向に取って、8個の欄を作るのです。でも、3Dで描くのは容易じゃないので2Dテーブルでやりくりします。

他に、同時確率テーブルや関数行/2変数関数テーブルなども後で使いますが、必要になったときに説明します。

何もしないときの平均損失

まず、何もしないときを考えます。検査代/薬代のコストはかからないので、感染して発病したときの損害10万円だけを考えます。

ファイナンスの確率に関して『量子ファイナンス工学入門』の前田先生は:

明日の株価予想が当たる確率は50%、外れる確率も50%である。当たるか、当たらないか分からない、つまり外れる確率が50%もある賭けに大事なお金を使うことについては慎重な判断を下すべきであろう。

せきしろさんによる確率の計算例では:

かわいい子が来る確率は来るか来ないかだから50%、その子がつまずく[檜山注:隣の席に座ろうとして転ぶ]確率は同様に50%、そして恋が生まれる確率も、生まれるか生まれないかで50%、よって1/8となり、12.5%となる。

このでんでいくと、発病する確率は50%、発病しない確率も50%で、平均損失は 10万円×1/2 + 0円×1/2 = 5万円 となります。これだと二人に一人は10万円損失している、つまり発病していることになります。全人口の半分が発病している状況ならこの計算は正しいですが、それが事実かどうか分かりません*3

実は、感染率の値がないと平均損失の計算はできません。そこで、全人口に対する感染者の比率は1%とします。100人に1人が感染しています。感染者の発病率は80%だったので、0.8%が発病の確率です。

この状況は、1000本に8本の当たりがあるクジを引くのと同じです。当たると賞金10万円なら、平均賞金額(賞金の期待値)は 10万円×8/1000 + 0円×992/1000 = 800円 です。今のケースでは賞金が損失となり、平均損失額が800円です。各個人としては、損失ゼロか10万円のどちらかですが、集団全体として損失を均等に負担するなら一人あたり800円になります。

行列計算で考える

前節の「何もしないとき」の例では、数値(スカラー)の計算だけで平均損失が出ました。前々節で述べたマルコフ行列なんて要りません … いやっ、背後には行列計算があるのです。

感染(infection)の比率は次の1列のマルコフ行列、つまり分布列でした。

infection
*
感染 1%
非感染 99%

発病(development)の比率は2行のマルコフ行列、つまり述語です。

develop
感染 非感染
発病 80% 0%
非発病 20% 100%

なお、この行列developは、薬の効果effectの非投与の部分を取り出したものです。逆に言うと、effectは、developに“薬を投与した場合の情報”を追加したものです。

感染/非感染を集約した発病率の計算は、2つのマルコフ行列の掛け算を計算します。

 develop¥: infection = ¥begin{bmatrix}0.8 & 0 ¥¥ 0.2 & 1 ¥end{bmatrix}¥begin{bmatrix} 0.01 ¥¥ 0.99 ¥end{bmatrix} = ¥begin{bmatrix}0.008 ¥¥ 0.992 ¥end{bmatrix}

ウィルスにA型ウィルスとB型ウィルスがあるならば、もっと行列計算らしくなります。

infection2
*
A感染 0.5%
B感染 0.5%
非感染 99%

B型ウィルスは発病率が低いとしましょう。

develop2
A感染 B感染 非感染
発病 80% 60% 0%
非発病 20% 40% 100%

感染ウィルスの種類と非感染の別を集約した発病率は、3行1列マルコフ行列(右側)infection2と2行3列マルコフ行列(左側)develop2の掛け算で計算します。

 develop2¥: infection2 = ¥begin{bmatrix}0.8 & 0.6 & 0 ¥¥ 0.2 & 0.4 & 1 ¥end{bmatrix}¥begin{bmatrix}0.005 ¥¥ 0.005 ¥¥ 0.99 ¥end{bmatrix} = ¥begin{bmatrix}0.007 ¥¥ 0.993¥end{bmatrix}

より一般に、確率分布を表す1列マルコフ行列(上の具体例ではinfection2)と条件付き確率を表すマルコフ行列(上の具体例ではdevelop2)の掛け算により、条件の場合分けを集約した確率分布を計算できます。

さて、平均損失の計算には、次の損失関数(loss function)が登場します。

loss
(関数) 発病 非発病
損失額 10万円 0円

関数のテーブルは1行だけの行列(マルコフ行列ではない!)とみなして、発病率分布のマルコフ行列(先に計算済の分布列 (develop infection))と掛け算します。これが前節で行った計算で、結果は800円です。

 loss¥: (develop¥: infection) = ¥begin{bmatrix}100000 & 0 ¥end{bmatrix}¥begin{bmatrix}0.008 ¥¥ 0.992¥end{bmatrix} = 800

これも、非発病の損失額が0円なので、あんまり行列計算の感じがしません。ちょっとだけ複雑なケースとして、検査を受けて何もしなかったときを考えてみましょう。損失関数は次のようになります。

loss2
(関数) 発病 非発病
損失額 10万300円 300円

A型ウィルスとB型ウィルスがある場合での平均損失計算は、次の行列計算となります。

 loss2¥: effect2¥: infection2 = ¥begin{bmatrix}100300 & 300 ¥end{bmatrix}¥begin{bmatrix}0.8 & 0.6 & 0 ¥¥ 0.2 & 0.4 & 1 ¥end{bmatrix}¥begin{bmatrix}0.005 ¥¥ 0.005 ¥¥ 0.99 ¥end{bmatrix} = 1000

この程度なら、直感とスカラー計算だけでも何とかなりますが、事情が複雑になれば行列計算が有利になります。行列による定式化は次のようにします。

  1. 確率分布は、1列だけのマルコフ行列(分布列)で表現する。
  2. 条件付き確率は、マルコフ行列で表現する。
  3. 損失関数は、1行だけの行列で表現する。これはマルコフ行列ではない
  4. 平均損失は、損失関数の1行と分布列の1列を掛けたスカラーとなる。

薬を飲むときの平均損失

検査を受けずにとりあえず薬を飲む場合を考えましょう。最初に損失関数を提示しておきます。

loss3
(関数) 発病 非発病
損失額 10万1000円 1000円

1000円は薬代です。

この損失関数を発病率の分布列で平均すれば求める結果が得られます。よって、発病率の分布列を求めればいいことになります。「何もしないとき」とは違い、薬の効果があるので、仮に感染していても発病リスクは低くなり、全体として発病率は低下します。

〈effectテーブル〉から薬を投与(administrate)時の情報だけを取り出します。それをeffectadmとしましょう。

effectadm
感染 非感染
発病 10% 0%
非発病 90% 100%

これと、集団全体での感染率の情報infectionを使います。

infection
*
感染 1%
非感染 99%

これらから、薬投与時の発病率は 1%×10% + 99%×0% = 0.1%、よって平均損失は 10万1000円×0.1% + 1000円×99% = 1100円 です。何もしないときの800円より損失は増加してますが、1000円は薬代のコストなので、発病時のダメージの平均は100円に減っています。この計算の背後には、次のような行列計算があると言えます。

loss3¥: effect_{adm}¥: infection = ¥begin{bmatrix} 101000 & 1000¥end{bmatrix}¥begin{bmatrix} 0.1 & 0 ¥¥ 0.9 & 1¥end{bmatrix}¥begin{bmatrix} 0.01  ¥¥ 0.99 ¥end{bmatrix} = 1100

ところで、「何もしないとき」の計算で出てきたdevelopは、effecから薬を非投与(not administrate, no administration)時の情報だけを取り出したものなので、develop = effectnoadm と書けます。effectnoadmと書き換えて先の計算を再掲すると:

 loss¥: effect_{noadm}¥: infection = ¥begin{bmatrix}100000 & 0 ¥end{bmatrix} ¥begin{bmatrix}0.8 & 0 ¥¥ 0.2 & 1 ¥end{bmatrix}¥begin{bmatrix} 0.01 ¥¥ 0.99 ¥end{bmatrix} = 800

「何もしないとき」と「薬を飲むとき」で類似の計算をしていることが分かります。そうであれば、「何もしないとき」と「薬をのむとき」を混ぜたような計算も同様にできそうです。次節でやってみます。

2変数損失関数の平均

前々節では「何もしないとき」、前節では「薬を飲むとき」の計算をしました。今度は、薬を投与(administration)する/しないが確率的な場合を考えます。

admin
*
投与 25%
非投与 75%

この投与率の解釈は、集団内で薬を投与する人と投与しない人がいて、その比率が25:75である状況です。あるいは別な解釈として、私個人の投与/非投与を、コインを2回投げて2回とも裏が出たら投与する、と決めるような状況です。

いずれにしても、発病を抑える薬の投与率が25%の前提で平均損失を求めてみます。薬代は損失に含めますが、感染検査はないとします。

損失に薬代を入れると、損失関数は2変数になります。{投与, 非投与}×{発病, 非発病} のそれぞれで損失額は違います。

loss3
(2変数関数) 投与 非投与
発病 損失10万1000円 損失10万円
非発病 損失1000円 損失0円

この損失関数の平均を計算するには、{投与, 非投与}×{発病, 非発病}上で定義された確率分布が必要です。平均(期待値、積分)というのは確率分布(より正確には確率測度)を使って計算されるものだからです。

今回のケースでは、薬を使う/使わないの判断は各人に任されています。検査を受けて決めるわけではないので、「感染しているかどうか」と「薬を投与するかどうか」は独立と仮定します。もし、ウィルスの潜伏期間中でも多少の症状が出る場合、この独立性はあやしくなります。「なんか調子悪いな、例のウィルスかな? とりあえず薬飲んどこう」と考える人がいれば、「感染しているかどうか」が「薬を投与するかどうか」の判断に影響します。でも今は独立だとします

感染率を表すinfectionと投与率を表すadminから、{感染, 非感染}×{投与, 非投与} 上の同時確率分布を求めるには、独立性の仮定から掛け算(確率の積の法則)が使えます。ちょっと無理矢理ですが、行列の掛け算の形で計算します(後述のテンソル積を使うのが自然です)。結果をinfAdmとします。

 admin¥: infection = ¥begin{bmatrix}0.25 ¥¥0.75¥end{bmatrix}¥begin{bmatrix}0.01 & 0.99¥end{bmatrix} = ¥begin{bmatrix}0.0025 & 0.2475 ¥¥ 0.0075 & 0.7425¥end{bmatrix} = infAdm

結果をテーブルで示すならば:

infAdm
(同時分布) 感染 非感染
投与 0.25% 24.75%
非投与 0.75% 74.25%

一列の分布列の形式にするなら:

infAdm
*
感染, 投与 0.25%
感染, 非投与 0.75%
非感染, 投与 24.75%
非感染, 非投与74.25%

{感染, 非感染}×{投与, 非投与} 上の確率分布であるinfAdmと、{感染, 非感染}×{投与, 非投与} の各場合ごとに発病率を与える条件付き確率であるeffec(薬の効果)から、{感染, 非感染}×{投与, 非投与}×{発病, 非発病} 上の同時確率分布を計算できます。

(無理矢理な)行列計算を使う手順だけ述べると、2行4列行列の形に書いたeffectにinfAdmから作った4行4列の対角行列(大文字始まりのInfAdmとする)を右から掛けます。その結果はinfAdmDev(infection, administration, developmentの同時確率分布)とします。

 effect¥: InfAdm ¥¥= ¥begin{bmatrix}0.1 & 0.8 &  0 & 0 ¥¥0.9 & 0.2 &  1 & 1¥end{bmatrix}¥begin{bmatrix}0.0025 & 0 & 0 & 0 ¥¥0 &  0.0075 & 0 & 0 ¥¥0 &  0 &  0.2475 & 0 ¥¥0 &  0 &  0 & 0.7425¥end{bmatrix} ¥¥= ¥begin{bmatrix} 0.00025 & 0.0060 & 0  & 0 ¥¥ 0.00225 & 0.0015 & 0.2475 & 0.7425¥end{bmatrix} ¥¥= infAdmDev

見出し付きのテーブルの形にすれば:

infAdmDev
(同時分布) 感染, 投与 感染, 非投与 非感染, 投与 非感染, 非投与
発病 0.25% 6% 0% 0%
非発病 2.25% 1.5% 24.75% 74.25%

感染/非感染の情報は不要なので、足し算して集約すると:

admDev
(同時分布) 投与 非投与
発病 0.25% 6%
非発病 27% 75.25%

これで、損失関数loss3と形が揃いました。

loss3
(2変数関数) 投与 非投与
発病 損失10万1000円 損失10万円
非発病 損失1000円 損失0円

損失関数loss3を横1行、同時分布admDevを縦1列にして掛け算すれば平均損失を計算できます。

 loss3¥: admDev = ¥begin{bmatrix}101000 & 1000 & 100000 & 0 ¥end{bmatrix}¥begin{bmatrix}0.0025 ¥¥0.27 ¥¥0.06   ¥¥0.7525¥end{bmatrix} =  1122.5

どんな道具を使うのか:行列の一般化

今まで出てきた二項述語や同時分布は、2次元テーブルの形をしていますが、マルコフ行列ではありませんでした。そのため、不自然な行列の変形や計算を強いられます。任意個数の添字(インデックス)を持った非負実数の族としてテンソルを定義し(次節で)、そのなかでマルコフ・テンソルを特定しましょう。

行列を成分表示するとき、aj i のような2個の添字(二重インデックス)を使います。テンソル計算では、添字を上下にして aji と書くのが普通です。ここでは、添字(インデックス)をブラケットに入れることにします; a[j, i] ですね。

a[j, i] という書き方ではまだ問題があるのでさらに工夫します。iが列番号でjが行番号のとき a[j←i]と矢印で区切ります。iとjを逆順に書きたいときは a[i→j] とします。矢印を使うと、行列の掛け算を「右から左」でも「左から右」でも自由に書けます。

  • (ba)[k←i] = Σ(j| b[k←j]a[j←i] ) … 右から左の順の積、併置
  • (a;b)[i→k] = Σ(j| a[i→j]b[j→k] ) … 左から右の順の積、セミコロン

添字のi, jなどは整数値でなくても、任意の有限集合の要素でいいとします。すると、X, Yを有限集合として (a[y←x] | x∈X, y∈Y)、または (a[x→y] | x∈X, y∈Y) のような形で行列を書けます。例えば、感染検査の精度を表す行列は、test = (test[r←i] | i∈{感染, 非感染}, r∈{陽性, 非陽性}) で、各成分は次のとおりです。

  • test[陽性←感染] = 98%
  • test[非陽性←感染] = 2%
  • test[陽性←非感染] = 5%
  • test[非陽性←非感染] = 95%

集団全体の感染率の分布列は infection = (infection[i←t] | t∈{*}, i∈{感染, 非感染}) で:

  • infection[感染←*] = 1%
  • infection[非感染←*] = 99%

一般に、a = (a[y←x] | x∈X, y∈Y) (あるいは、a = (a[x→y] | x∈X, y∈Y))のとき、行列aのプロファイルは X→Y (XからY)だといい、そのことを a:X→Y と書きます。感染検査の精度test、集団全体の感染率infectionならば:

  • test:{感染, 非感染}→{陽性, 非陽性}
  • infectiont:{*}→{感染, 非感染}

これらの行列の積 (test infection) = (infection;test) のプロファイルは {*}→{陽性, 非陽性} となります。これでお気付きの方もいるでしょうが、行列の全体も、マルコフ行列の全体も圏となります。が、その詳細はここでは割愛します。

{感染, 非感染}のように、{A, 非A}の形の集合が頻繁に出てくるので、A? = {A, 非A} としましょう。例えば:

  • 感染? = {感染, 非感染}
  • 陽性? = {陽性, 非陽性}

疑問符'?'は、"or not"と読むといいでしょう。また、{*}も頻繁に出てくるので 1 = {*} と置きます。この略記を使ってtestとinfectionのプロファイルを書けば:

  • test:感染?→陽性?
  • infectiont:1→感染?

どんな道具を使うのか:マルコフ・テンソル

薬の効果を表す情報effectは、2次元のテーブルではうまく表せないものでした。ひとつの欄に複数の値を記入することになります。

effect
感染 非感染
投与 発病10%, 非発病90% 発病0%, 非発病100%
非投与 発病80%, 非発病20% 発病0%, 非発病100%

または、縦横の見出しを組み合わせて横の見出しに潰します。

effect
感染, 投与 感染, 非投与 非感染, 投与 非感染, 非投与
発病 10% 80% 0% 0%
非発病 90% 20% 100% 100%

どちらにしても不自然。実は、〈effectテーブル〉の成分は3つの添字(インデックス)を持つのです。effect = (effect[i, a, d] | i∈感染?, a∈投与?, d∈発病?)。アレ、区切りは矢印でした、矢印はどう入れましょうか? 薬の効果の計算では、{感染, 非感染}×{投与, 非投与}の要素を与えて、{発病, 非発病}上の分布を知りたいので、関数的に考えれば 感染?×投与?→発病? というプロファイルになります。

つまり、薬の効果を表す情報は effect = (effect[i, a→d] | i∈感染?, a∈投与?, d∈発病?) となります。3つの添字のうちiとaが入力側、dが出力側です。矢印を逆向きにしたいなら effect = (effect[d←i, a] | i∈感染?, a∈投与?, d∈発病?) でもかまいません。

一般に、いくつかの添字(インデックス)を持つ実数(ここでは非負実数)の族で、添字が入力側と出力側に分割されているものをテンソルtensor)と呼びます*4。行列は添字を2つ持つテンソルです。薬の効果を表すeffectは添字を3つ持つテンソルの例です。

テンソルの入力側添字を固定します; 例えば effect[感染, 非投与→d]。出力側の添字を動かして総和を取りましょう; Σ(d∈発病? | effect[感染, 非投与→d])。この例では総和が1になります。どの入力側添字(の組)に対しても出力側の総和が1のとき、そのテンソルマルコフ・テンソル(Markov tensor)と呼びます。マルコフ行列は特別な形のマルコフ・テンソルです。

同時確率分布もマルコフ・テンソルとみなせます。次の例を考えてみます。

admDev
(同時分布) 投与 非投与
発病 0.025% 0.6%
非発病 24.975% 74.4%

これはマルコフ行列ではないので、(方便として)1列に直してマルコフ行列と考えました。

admDev
*
投与, 発病 0.025%
投与, 非発病 24.975%
非投与, 発病 0.6%
非投与, 非発病 74.4%

行の見出しは 投与?×発病? の要素です。一方、ただ1つの列の見出しはダミーの'*'です。列見出しの集合が入力側、行見出しの集合が出力側なので、同時確率分布admDevのプロファイルは 1→投与?×発病? と考えられます。出力側の 投与?×発病? 上で総和を取ると1になるので、同時分布admDevはマルコフ・テンソルです。

念のために、マルコフ・テンソルの定義を一般的に述べれば: f = (f[x1, ..., xn→y1, ..., ym] | x1∈X1, ..., xn∈Xn, y1∈Y1, ..., ym∈Ym) という添字族がマルコフ・テンソルだとは、次の条件をみたすことです。

  • 任意の a1∈X1, ..., an∈Xn に対して、Σ(y1∈Y1, ..., ym∈Ym | f[a1, ..., an→y1, ..., ym]) = 1

例に挙げたeffectとadmDevは:

  • 薬の効果effectは、プロファイルが 感染?×投与?→発病? であるマルコフ・テンソルである。
  • 薬の効果と感染分布/投与分布から作った同時確率分布admDevは、プロファイルが 1→投与?×発病? であるマルコフ・テンソルである。

複雑なプロファイルを持つマルコフ・テンソルを考えることができますが、今回必要なのは2項ファジー述語に対応するマルコフ・テンソルと、同時確率分布に対応するマルコフ・テンソルです。また、マルコフ・テンソルに関する様々な操作がありますが、系統的説明は省略して、必要なときに必要なだけ導入することにします。

検査を受けて判断するときの平均損失:準備

まず、損失関数を書いておきます。

loss4
(2変数関数) 投与 非投与
発病 損失10万1300円 損失10万300円
非発病 損失1300円 損失300円

300円は検査の費用です。loss4はマルコフ・テンソルではなくて関数です。関数としてのプロファイルを書いておくと: loss4:投与?×発病?→損失額 (as 関数) です。

loss4の平均値を求めるには、1→投与?×発病? というプロファイルを持つ同時確率分布admDev2が必要です。この同時分布admDev2を求めることが課題です。

同時分布admDev2を求めるには、今まで出てきたtest, effect, infectionを使います。これらをまとめておくと:

名前 意味 プロファイル
test 感染検査の精度 感染?→陽性?
effect 治療薬の効果 投与?×感染?→発病?
infection 集団全体の感染率 1→感染?

これらのマルコフ・テンソルを下のような図で表します。マルコフ・テンソルはオダンゴで描きます。オダンゴから出たワイヤーに添字集合をラベルします。上が入力側の添字集合、下が出力側の添字集合です。入力ラベル集合が 1 = {*} のときは、ワイヤーを描かずに'*'マークを付けることにします。

関数は四角い箱で表しましょう。損失関数 loss4:投与?×発病?→損失額 が2変数の関数です。検査の結果を見て薬の投与/非投与を決める判断関数(decision function)も関数 decide:陽性?→投与? (as 関数) です。

念のため注意しておくと、有限集合から有限集合への関数(写像)は、マルコフ行列として表現できます。decide:陽性?→投与? をテーブルで表すなら:

decide
陽性 非陽性
投与 100% 0%
非投与 0% 100%

テーブルの欄の値が100%か0%であるマルコフ行列は関数(写像)を表すのです。有限集合のあいだの関数(写像)は特殊なマルコフ行列なのだとも言えます。損失関数 loss4:投与?×発病?→損失額 は、値の領域(損失額の集合、Rと同型とする)が有限集合ではないのでマルコフ“行列”にはなりませんが、マルコフ核(マルコフ行列/マルコフ・テンソルの一般化)にはなります。

さて、求めるべき同時分布 admDev2:1→投与?×発病? を図示すると次の形です。

admDev2の実際の構成は次々節以降で行います。次節では、マルコフ行列に対する操作の説明をします。

マルコフ・テンソルの種類と操作

X1, ..., Xn, Y1, ..., Ym が(n + m)個の有限集合だとして、f:X1, ..., Xn→Y1, ..., Ym というプロファイルのテンソル反変n階/共変m階テンソルと呼びます。あるいは、nを反変の階数、mを共変の階数、(n + m)を階数と呼びます。この言い方は歴史的なもので、あんまり分かりやすくないのですが、他の言い方も見当たらないので致し方なく使うことにします。

今までに出てきたマルコフ・テンソルの種類を階数と共に挙げておきます。

名称 プロファイル 階数
一般的マルコフ行列 X→Y 反変1階/共変1階
確率分布(1列のマルコフ行列) 1→X 反変0階/共変1階
ファジー述語(2行のマルコフ行列) X→A? 反変1階/共変1階
二項述語 X×Y→A? 反変2階/共変1階
同時確率分布 1→X×Y反変0階/共変2階
有限集合のあいだの写像 X→Y 反変1階/共変1階

マルコフ・テンソルが、これらのどれか一つだけに分類される、ということではありません。例えば、infection:1→感染? は確率分布でもありファジー述語でもあります。

今回の計算で使うマルコフ・テンソルの操作には次のものがあります。

  1. 2つのマルコフ・テンソル結合(composition)
  2. 2つの確率分布のテンソルtensor product)
  3. 確率分布とマルコフ・テンソルからの同時化(同時確率分布の作成;jointification)
  4. 同時確率分布の周辺化(周辺分布の作成; marginalization)

これらの操作を一般的に述べるのではなく、今回使う範囲に限って述べます。説明の後に絵があります。

結合(composition)

マルコフ行列(反変1階/共変1階のマルコフ・テンソル)に限れば、結合は既に出てきています。f = (f[x→y] | x∈X, y∈Y), g = (g[y→z] | y∈Y, z∈Z) に対して、fとgの結合f;gは次のように定義されます。

  • (f;g)[x→z] = Σ(y∈Y | f[x→y]g[y→z])

f;gのプロファイルは X→Z となります。

x, y, zが (x1, ..., xn), (y1, ..., ym), (z1, ..., zk) のようになっても同じで、f:X1×...×Xn→Y1×...×Ym と g:Y1×...×Ym→Z1×...×Zk の結合を定義できます。

テンソル積(tensor product)

確率分布 p = (p[x] | x∈X) と q = (q[y] | y∈Y) があるとき、これらのテンソル積p¥otimesqは次のように定義されます。なお、p[x]はp[*→x]の略記です。

  • (p¥otimesq)[x, y] = p[x]q[y]

p¥otimesqのプロファイルは 1→X×Y となります。

テンソル積は、感染率 infection:1→感染? と投与率 admin:1→投与? から infAdm = infection¥otimesadmin を作る際に使っています。単なる計算としてテンソル積を作ることはいつでもできますが、背後にある確率変数の独立性がないと誤った計算になることがあります。

同時化(jointification)

確率分布 p = (p[x] | x∈X) と、マルコフ行列 f = (f[x→y] | x∈X, y∈Y) があるとき、同時分布 p∩f を次のように定義します。

  • (p∩f)[x, y] = p[x]f[x→y]

これが、マルコフ行列fの分布pによる同時化で、条件付き確率を同時確率に変換する操作です。p∩f のプロファイルは 1→X×Y となります。

周辺化(marginalization)

同時分布 f = (f[x, y] | x∈X, y∈Y) に対して、X方向への周辺化 f↓X,YX と、Y方向への周辺化 f↓X,YY は次のように定義されます。

  • (f↓X,YX)[x] = Σ(y∈Y | f[x, y] )
  • (f↓X,YY)[y] = Σ(x∈X | f[x, y] )

f↓X,YX, f↓X,YY のプロファイルはそれぞれ 1→X, 1→Y です。

上付き添字X, Yは省略して、f↓X, f↓Y でもいいでしょう。また、X×Y×Z上の同時分布をY×Zに周辺化する操作なども同様に定義できます。不要な情報を集約するときに周辺化を使います。


結合、テンソル積、同時化、周辺化を図示すると次のようになります。

検査を受けて判断するときの平均損失:計算

admDev2:1→投与?×発病? を次の4ステップで計算します。

  1. [test;decideの計算] 感染検査の精度を表す test:感染?→陽性? と、検査の結果から投与/非投与を決める関数 decide:陽性?→投与? の結合 test;decide:感染?→投与? を求める。
  2. [infAdm2の計算] test;decide:感染?→投与? を、感染率 infection:1→感染? により同時化して、infection∩(test;decide) = infAdm2 : 1→感染?×投与? を求める。
  3. [infAdmDev2の計算] 薬の効果 effect:感染?×投与?→発病? を、infAdm2:1→感染?×投与? により同時化して、infAdm2∩effect = infAdmDev2 : 1→感染?×投与?×発病? を求める。
  4. [admDev2の計算] 同時確率分布 infAdmDev2:1→感染?×投与?×発病? を周辺化して、確率分布 admDev2:1→投与?×発病? を求める。
test;decide:感染?→投与?

testとdecideの結合は、マルコフ行列の掛け算として自然に計算できます。

 test;decide = decide¥: test = ¥begin{bmatrix} 1 & 0 ¥¥ 0 & 1 ¥end{bmatrix}¥begin{bmatrix} 0.98 & 0.05 ¥¥  0.02 & 0.95 ¥end{bmatrix} = ¥begin{bmatrix} 0.98 & 0.05 ¥¥  0.02 & 0.95 ¥end{bmatrix}

test;decide
感染 非感染
投与 98% 5%
非投与 2% 95%

decideの行列は単位行列になっていますが、陽性? の空間から 投与? の空間に変換しているので無意味ではありません。decideを他の写像に切り替えると、別な結果が得られます。例えば、検査の結果によらず薬を投与するという判断もあります。

infAdm2:1→感染?×投与?

infAdm2 = infection∩(test;decide) は、本来テンソル計算で定義されますが、無理に行列計算でやるなら、分布列(1列のマルコフ行列)infectionを対角行列化して右からtest;decideに掛けます。infectionの対角行列化をInfectionとします。

 {}^{infection¥cap}(test;decide) = (decide¥: test)¥: Infection ¥¥ = ¥begin{bmatrix} 0.98 & 0.05 ¥¥  0.02 & 0.95 ¥end{bmatrix}¥begin{bmatrix}0.01 & 0 ¥¥ 0 & 0.99 ¥end{bmatrix} = ¥begin{bmatrix} 0.0098 & 0.0495 ¥¥ 0.0002 & 0.9405 ¥end{bmatrix} ¥¥= infAdm2

infAdm2
(同時分布) 感染 非感染
投与 0.98% 4.95%
非投与 0.02% 94.05%

感染検査の不完全さから、感染しているにも関わらず非投与の人が0.02%、感染してないのに投与してしまう人が4.95%います。

infAdmDev2:1→感染?×投与?×発病?

infAdmDev2 = infAdm2∩effect も、テンソル計算で定義されます。これも無理に行列計算でやるなら、effectを2行4列の行列の形にして、infAdm2の4成分を対角行列化した4行4列行列InfAdm2を右からeffectに掛けます。

 {}^{infAdm2¥cap}effect = effect¥: InfAdm2¥¥= ¥begin{bmatrix}0.1 & 0.8 & 0 & 0 ¥¥ 0.9 & 0.2 & 1 & 1 ¥end{bmatrix}¥begin{bmatrix}0.0098 & 0      & 0      & 0 ¥¥0      & 0.0002 & 0      & 0 ¥¥0      & 9      & 0.0495 & 0 ¥¥0      & 0      & 0      & 0.9405¥end{bmatrix} ¥¥ = ¥begin{bmatrix}0.00098 & 0.00016 & 0      & 0      ¥¥0.00882 & 0.00004 & 0.0495 & 0.9405 ¥end{bmatrix} ¥¥= infAdmDev2

infAdmDev2
(同時分布) 感染, 投与 感染, 非投与 非感染, 投与 非感染, 非投与
発病 0.098% 0.016% 0% 0%
非発病 0.882% 0.004% 4.95% 94.05%
admDev2:1→投与?×発病?

感染に関する情報は不要なので、列を足し算して集約します。

admDev2
(同時分布) 投与 非投与
発病 0.098% 0.016%
非発病 5.832% 94.054%


目的としたadmDev2が求まったので、損失関数loss4(下に再掲)をadmDev2で重み付けした平均を求めます。

loss4
(2変数関数) 投与 非投与
発病 損失10万1300円 損失10万300円
非発病 損失1300円 損失300円

10万1300円×0.098% + 1300円×5.832% + 10万300円×0.016% + 300円×94.054% = 473.3円 となります。検査を受けて適切な判断と予防治療をすれば、平均損失額はだいぶ下がります。

おわりに

この記事を書くにはちょっと苦労しました。最初は、圏論的定式化と実例の両方を一緒に書こうと思ったのですが、量が増えすぎるのであきらめました。ウィルス感染症に関わる検査、治療薬、損失などを計算する事例だけにしました。例題の計算に必要な概念は説明していますが、系統的でも網羅的でもありません。僕はストリング図に沿って計算してますが、それを再現するのも疲れるので、図の提示も断片的です。

しかしそれでも、確率的問題の定式化と計算に、テンソルとその図式表現であるストリング図が有効であることが多少は伝わったでしょう。

テンソルの数値的計算は、行列計算を流用しています。この方法はバッドノウハウで、あまり好ましくありません。テンソル数値計算ができるソフトウェアを探せば良かったのかも知れませんが、数値計算は手元にあったR言語処理系で行いました(Rにもテンソル計算パッケージはあるようです)。

マルコフ・テンソルは、確率分布、条件付き確率、同時確率に一様な定式化を与える点で便利なのですが、これらの意味的な違いを意識したほうがいいときもあります。この事の背景には、確率分布(確率空間)、条件付き確率、同時確率のそれぞれに対応する圏 ProbCondProbJointProb の存在があります。これらの圏達とその相互関係はまたの機会に述べるつもりです。

確率分布/条件付き確率/同時確率を計算する行為は、ある種の推論だと言えます。確率的推論を行うための論理系(logical system)をうまく定義できれば、それは日常生活の論理を(古典論理より)うまく説明できるかも知れません。「アブダクションと確率的推論」で断片的に述べたことを、もう少し体系化できる可能性があります。

現時点での感触としては、「計算と論理と圏の三者が密接に関連している」というカリー/ハワード/ランベック対応(Curry-Howard-Lambek correspondence)の確率版があるような気がします。

オマケ:マルコフ・テンソルと関数の一覧

矢印が'→!'と書いてあるのは関数です。

  1. test: 感染? → 陽性?
  2. effect: 感染?×投与? → 発病?
  3. infection: 1 → 感染?
  4. develop: 感染? → 発病?
  5. infection2: 1 → AB感染?
  6. develop2: AB感染? → 発病?
  7. loss: 発病? →! 損失額
  8. loss2: 発病? →! 損失額
  9. loss3: 発病? →! 損失額
  10. infAdm: 1 → 感染?×投与?
  11. admin: 1 → 投与?
  12. infAdmDev : 1 → 感染?×投与?×発病?
  13. admDev: 1 → 投与?×発病?
  14. loss4: 投与?×発病? →! 損失額
  15. admDev2: 1 → 投与?×発病?
  16. decide: 陽性? →! 投与?
  17. infAdm2: 1 → 感染?×投与?
  18. infAdmDev2: 1 → 感染?×投与?×発病?
  19. admDev2: → 投与?×発病?

*1:この設定のモトは、T-ウィルスと抗ウィルス剤。レイン・オカンポは薬を打ったが手遅れでした。カルロスは感染してましたが、アンジー(アンジェラ・アシュフォード)が持っていた抗ウィルス剤で発病を免れました。

*2:より一般的な概念はマルコフ核ですが、離散有限の場合ならマルコフ行列で間に合います。

*3ベイズ推論で、ほんとに何も分からないとき、暫定的に五分五分だと仮定することはあります。

*4:「テンソル」は多義語なので、多くの意味を持ちます。ここでは添字族をテンソルと呼ぶ、ということです。

2017-04-18 (火)

滝沢カレンさんの言語芸術 その2

| 15:20 | 滝沢カレンさんの言語芸術 その2を含むブックマーク

去年(2016年)の年末に書いたエントリー「滝沢カレンさんの言語芸術」にて:

滝沢カレンさんの変な日本語が2015年に評判になったようです。もうすぐ2017年ですけど。

事情をよく知らなかったので、このときの僕の印象は「2015年に評判になったらしいけど、一過性のプチブームだったんだろう」というものでした。ところが、2017年になっても滝沢カレンさんの快進撃は止まらないようです。

声に出して読みたい日本語』の著者・斎藤孝 明治大学教授は、滝沢カレンさんの大ファンらしく、彼女の言語センスを「天才的」「詩的」と絶賛しているとか。また、最近の『芸人ドラフト会議』なるテレビ番組の「自分がMCをやるときに使いたいタレント」として、女性タレントとしてはダントツの支持を集めていたようです。そして、Eテレの教育番組『NHK高校講座 ベーシック国語』の生徒役に起用されたそうです。NHKも随分とあざといキャスティングをしますね。

「あの変な日本語は、キャラを作るためにわざとやっているんじゃないか?」という疑惑があるそうです。僕は「それはない」と思います。通常の日本語を普通に使えて、それとは別にあの言語ワールドを自ら創造・構築し、それを自由に切り替えられる、としたら、それはもう掛け値なしの驚嘆すべき天才です。そこまでの突出した言語能力を持ち合わせている人間がいる可能性は低い気がするのです。

その滝沢カレンさんがインスタグラムをやっているのですが、あの日本語でかなり長文のコメントを付けていて、カレン語のファンにはたまりません。

最近のコメントから(文中の「なっちゃん」とは横澤夏子さんのことです):

本当になっちゃん(さん)の一文字一文字発する言葉に今にも踊れそうな自分にびっくりこきまろしつつも、話をどこかで、まだかまだかと聞かせてよと言いたくなるあのやり方、本当に素敵でした

[..snip..]

次のなっちゃん(さん)への嬉しみが高鳴る一日として今日の窓を閉めましょう... では、寝ます

通常日本語への翻訳はまったく無粋とは承知ながらも:

横澤夏子さんの一言一言、その発する言葉に今にも踊りだしそうな自分に、我ながら本当にびっくりしてしまいました。「話をもっともっと聞かせてよ」と言いたくなってしまうようなあの話し方、本当に素敵でした。

[..snip..]

次に横澤夏子さんに会えることへの期待で胸が高鳴るくらい、楽しい一日でした。そんな思いを抱いたまま今日が終わります。おやすみなさい。

「びっくりこきまろしつつ」とか「嬉しみが高鳴る一日」とかの意味が汲み取れてないし、肝心の語感が失われるのでダメです。カレン語は原語で読むべし。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20170418