前層の圏における記法と計算もう少し - 檜山正幸のキマイラ飼育記 (はてなBlog)

日本列島は自然災害に苛まれています。皆さんご無事でしょうか。

「前層の圏における記法と計算」に関してもう少し。定義コンテキストと引数の話。

内容：

定義のための構文
関手と自然変換での例
プロファイルリストと定義の正規化
おわりに

定義のための構文

構文の説明をします。退屈にならないように、簡単な例に沿って説明します。平面R²の距離dを例にしましょう。

d(x, y) := sqrt( (x₁ - y₁)² + (x₂ - y₂)² )

名前（変数）や式の型情報をちゃんと付けると：

d(x∈R², y∈R²) := (sqrt( (x₁ - y₁)² + (x₂ - y₂)² ) ∈R)

あるいはラムダ記法を用いて：

d := λ(x, y)∈R²×R².(sqrt( (x₁ - y₁)² + (x₂ - y₂)² ) ∈R)

次に、R²の一点aを固定して、その点からの距離を考えることにしましょう。

d(x∈R²) := (sqrt( (x₁ - a₁)² + (x₂ - a₂)² ) ∈R)

このとき、aに関する型情報も提供するために、次の形を使います。

For〔a∈R²〕 d(x∈R²) := (sqrt( (x₁ - a₁)² + (x₂ - a₂)² ) ∈R)

なにかを定義する場合の一般的な構文として、次を形式を採用することにします。Forの後の括弧が大きい（亀甲括弧）のは視認性のためです（それ以上の理由はありません）。

For〔名前の型情報〕式1 := 式2

名前の型情報の部分を定義コンテキスト〈definition context〉、式1を定義ヘッド〈definition head〉、式2を定義ボディ〈definition body〉と呼ぶことにします。

定義ヘッドは名前だけ、または名前に仮引数並びを付けた形です。そして仮引数並びは、名前または型情報付きの名前を並べたもの（リスト）です。次はいずれも定義ヘッドになれる式です。

d
d(x, y)
d(x∈R², y∈R²)

仮引数並びに型情報が欠落している場合は、定義コンテキストで補うことができます。例えば：

For〔a∈R², y∈R²〕 d(y) := (sqrt( (a₁ - y₁)² + (a₂ - y₂)² ) ∈R)

戻り値型の情報を定義ヘッド側（':='の左側）に付けてもいいとします。例えば：

For〔a∈R², y∈R²〕 d(y) ∈R := sqrt( (a₁ - y₁)² + (a₂ - y₂)² )

今述べたルールだと、定義の書き方にはかなりの自由度があります。標準的な書き方に“正規化”することは後でまた触れます。

関手と自然変換での例

実際に僕が遭遇した例を説明します。とある状況で、ラムダ式 λu.F(u)(x) や、無名ラムダ変数（ハイフン）を使った F(-)(x) で計算していたのですが、だんだんワケワカラナクなってきました。この F(-)(x) をチャンと書き下すことにします。

とりあえず、F(-)(x) （λu.F(u)(x) でも同じ）の意味が分かりませんよね。Fは関手です。となると、Fの引数は対象か射です。uはたぶん射だろうと推測して、F(u)は、関手Fのターゲット圏の射だろうと見当が付きます。しかし、F(u)(x) の'(x)'の部分が不明。実は、Fは集合圏に値をとる関手でした。よって、F(u)は写像で、F(u)(x)は写像に引数（集合の要素）xを適用したものです。

とまー、そんなことをゴチャゴチャ説明するよりは、正確な記法で書いたほうが早い！

C in Cat 、または C∈|Cat|
F:C^op→Set in CAT 、または F∈CAT¹(C^op, Set)
A in C 、または A∈|C|
x∈F(A)
X in C 、または X∈|C|
u:X→A in C 、または u∈C(X, A)
F(u):F(A)→F(X) in Set 、または F(u)∈Set(F(A), F(X))
F(u)(x)∈F(X)

F(-)(x) と書いたときの背後にこういった状況（文脈）があるわけです。とりあえず、F(-)(x) = λu.F(u)(x) に型情報を付けると：

λu∈C(X, A).(F(u)(x) ∈F(X))

このラムダ式で定義される写像をΨとすれば：

Ψ:C(X, A)→F(X) := λu∈C(X, A).(F(u)(x) ∈F(X))

出現している名前 A, x, X に関する型情報を定義コンテキストに置けば：

For〔A in C, x∈F(A), X in C〕 Ψ:C(X, A)→F(X) := λu∈C(X, A).(F(u)(x) ∈F(X))

さらに、Cが小さい圏で、FがCからSetへの関手であることも定義コンテキストに含めると：

For〔C in Cat, F:C^op→Set in CAT〕 For〔A in C, x∈F(A), X in C〕 Ψ:C(X, A)→F(X) := λu∈C(X, A).(F(u)(x) ∈F(X))

定義コンテキストは、Forの入れ子で書いてもフラットに書いても同じことです。なので、上の表現は次のようにフラットに書いてもかまいません。

For〔C in Cat, F:C^op→Set in CAT, A in C, x∈F(A), X in C〕 Ψ:C(X, A)→F(X) := λu∈C(X, A).(F(u)(x) ∈F(X))

逆に、新たな入れ子を作ってもかまいません。

For〔C in Cat, F:C^op→Set in CAT〕For〔A in C〕For〔x∈F(A), X in C〕
　　Ψ:C(X, A)→F(X) := λu∈C(X, A).(F(u)(x) ∈F(X))

うまく入れ子を作ると、ひとつのコンテキスト内では依存性をなくす（プロファイル宣言の順番を変えてもいい）ように出来ます。

プロファイルリストと定義の正規化

プロファイルは型と同じようなものです。型はモノの種類ですが、プロファイルも種類で、次元が加味されています -- 前回の記事、より詳しくは「圏論的宇宙と反転原理と次元付きの記法」を参照してください。名前にプロファイルを付けるには、in記法、または集合の所属（∈）記法を使います。

プロファイル付きの名前をカンマ区切り*1で並べたものをプロファイルリスト〈profile list〉と呼びます。リストなので、原則的に順序を変えることは出来ません（特定の条件化で並べ替えが出来ることはあります）。例えば、前節最後の定義のコンテキスト内部はプロファイルリストです。

C in Cat, F:C^op→Set in CAT, A in C, x∈F(A), X in C

定義に登場する次の3つの部分は、すべてプロファイルリストです。

定義コンテキスト（の内部）
定義ヘッドの仮引数リスト
ラムダ抽象のラムダリスト（ラムダ束縛変数のリスト）

単に構文が同じだけではなくて、定義コンテキスト／仮引数リスト／ラムダリストは相互に入れ替えが可能です。

定義コンテキストは、暗黙の引数と考えることができます。なので、定義コンテキストの一部または全部を、定義ヘッドの仮引数リストに移すことができます。例えば、最初の距離の例で、

For〔a∈R², y∈R²〕 d(y) ∈R := sqrt( (a₁ - y₁)² + (a₂ - y₂)² )

型宣言（プロファイル宣言）を、仮引数リスト内に移すと：

d(a∈R², y∈R²) ∈R := sqrt( (a₁ - y₁)² + (a₂ - y₂)² )

前節の例：

For〔C in Cat, F:C^op→Set in CAT〕For〔A in C〕For〔x∈F(A), X in C〕
　　Ψ:C(X, A)→F(X) := λu∈C(X, A).(F(u)(x) ∈F(X))

で、定義コンテキスト内のプロファイル宣言の一部を仮引数リストに移すと次のようになります。

For〔C in Cat, F:C^op→Set in CAT〕For〔A in C〕
　　Ψ(x∈F(A), X in C):C(X, A)→F(X) := λu∈C(X, A).(F(u)(x) ∈F(X))

さらに、定義ヘッド（左辺）の仮引数リストは、定義ボディ（右辺）のラムダリストに移すことができます。距離の例なら：

d := λ(a∈R², y∈R²).(sqrt( (a₁ - y₁)² + (a₂ - y₂)² ∈R)

関手／自然変換の例では（複雑になってきたので改行・インデントします）：

For〔C in Cat, F:C^op→Set in CAT〕
For〔A in C〕
  Ψ :=
  λ(x∈F(A), X in C).(
    λu∈C(X, A).(
       F(u)(x)
    ∈F(X)
    )
  : C(X, A)→F(X) in Set
  )

定義の書き方にバラエティがあるので、標準の形を決めたいなら、例えば（あくまで一例）、定義ボディは名前だけにして、in記法を'∈'に書き換えることにすれば、

For〔C∈|Cat|, F∈CAT¹(C^op,  Set)〕
For〔A∈|C|〕
  Ψ :=
  λ(x∈F(A), X∈|C|).(
    λu∈C(X, A).(
      F(u)(x)
    ∈F(X)
    )
  ∈Set(C(X, A), F(X))
  )

さらに、定義コンテキストの一部をラムダリスト内に押し込むことができます。

For〔C∈|Cat|, F∈CAT¹(C^op,  Set)〕
  Ψ :=
  λ(A∈|C|).(
    λ(x∈F(A), X∈|C|).(
      λu∈C(X, A).(
        F(u)(x)
      ∈F(X)
      )
    ∈Set(C(X, A), F(X))
    )
  : F(A)×|C|→Nat(C(-, A), F) in Set
  )

このなかの Nat(C(-, A), F) = Nat(C(-, A), F:C^op→Set) は、CAT²(C(-, A), F) のことですが、Cが小さいので、集合（Setの対象）とみなしたものです。米田の補題から、Nat(C(-, A), F) $\stackrel{\sim}{=}$ F(A) なので、同型をあたかもイコールのように扱えば、最後のプロファイル行は次のように書けます。