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

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

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

［参照用 記事］

矢印の混乱に対処する： デカルト閉圏のための記法

雑記／備忘

2023-02-09の僕のツイート：

矢印「→」が異なる意味でオーバーロードされているのは相当に深刻な問題だなー。
これで混乱したり挫折する人がいるから、弊害とても大きい。

十数年前からカリー／ハワード対応のセミナーとかやっているわけです。

複数の分野に関係する事柄を説明するのはなかなか難しい、計算過程を理解する／してもらうのも大変。だがしかし、僕やあなたが悪いとは限らない：

  • 説明がうまくいかないときは用語法が悪いのかも知れない。
  • 計算がうまくいかないときは記法が悪いのかも知れない。

デカルト閉圏周辺の記法、特に矢印の使い方を整理して、概念がもっとスッキリするように／計算がもっと楽になるようにしましょう。$`\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\In}{\text{ in }}
\newcommand{\mrm}[1]{\mathrm{#1} }
`$

内容：

カリー／ハワード／ランベック対応

ここ最近、またカリー／ハワード／ランベック対応を話題にしています。

ブログ内検索してみたら、「カリー／ハワード」という語が出てくる最初のブログ記事は2006年のエントリでした。

「ハワード」の検索結果はこんな感じ↓

カリー／ハワード／ランベック対応をテーマにして、技術者・プログラマ向けのセミナー（無料／有料）を何度かやっているので、カリー／ハワード／ランベック対応に対してはある程度の知識と経験はあるつもりです。

でねー、カリー／ハワード／ランベック対応を語るとき何が大変かって、複数の分野をまたぐから、用語法・記法の調停が大変。単に異なる方言が三種類（型理論、論理、圏論）というだけでなく、ひとつの分野内でも用語法・記法はグジャグジャで（例えば、「型理論ってば」参照）、ロクでもないのよね。異なる三種類のグジャグジャが混じったら、そらカオスですわ。

特に僕が困っていることをピンポイントで取り上げると「矢印記号」。

矢印記号の憂鬱

矢印っぽい記号の各分野での使用法を表にまとめると：

型理論 論理 圏論
関数集合型 $`\to`$ 含意 $`\Rightarrow`$ 指数対象 $`[\_, \_]`$
型判断の区切り $`\vdash`$ シーケントの区切り $`\to`$ 射のプロファイルの区切り $`\to `$
証明可能性 $`\vdash`$
2-射のプロファイルの区切り $`\Rightarrow`$

横の行はカリー／ハワード／ランベック対応による対応があります。この表の欄も標準的というわけでもなくて、つうか、方言がたくさんあるだけで標準がないのです。

今日は、矢印記号のバラバラな使用法を調停して折り合いをつけたいと思います。僕が圏論好き〈ケンロニスト〉ということで、色々とご異論・ご意見もお有りでしょうが、圏論側に寄せることにします。つまり、一番ポピュラーな矢印記号である「$`\to`$」は、圏の射のプロファイル（域と余域の仕様）の区切り記号に独占的に使わせていただきます。関数集合型、シーケントの区切りには「$`\to`$」以外の記号を割り当てます。あしからず。

圏論優先にしましたが、現状の圏論の記法がベストとも言えないので、圏論の記法にも手を入れます。

射のプロファイルと射の定義

次の3つの表現は完全に同義です。

  1. $`f: X \to Y \In \cat{C}`$
  2. $`f \in \cat{C}(X, Y)`$
  3. $`f\in \mrm{Mor}(\cat{C}) \land \mrm{dom}(f) = X \land \mrm{cod}(f) = Y`$

矢印記号「$`\to`$」はこの意味で使います。

射 $`f`$ が、引数変数〈入力変数〉を含む式〈項〉 $`\psi`$ で定義されるときは次の形で書きます。

$`\quad f := (x: X \vdash \psi : Y) \In \cat{C}`$

これは、型理論の型判断に名前を付けたものです。これで型判断と折り合いが付きます。名前がないときは、式〈項〉を使って無名の射を定義していることになります。

$`x: X`$ という変数の型宣言は、型理論的には問題がない、つうかこれが普通ですが、圏論的解釈は自明ではありません。集合圏であれば、コロンを所属関係と解釈すればいいでしょう。

$`\quad f := (x\in X \vdash \psi \in Y) \In {\bf Set}`$

集合圏でなくても、終対象があって、終対象からの射が十分にある圏なら、変数 $`x`$ は集合 $`\cat{C}({\bf 1}, X)`$ 上を走る変数として解釈できます。終対象からの射が少ない、あるいはそもそも終対象がない圏なら、変数 $`x`$ は（大きいかも知れない）集合 $`|\cat{C}_{/X}|`$ を走る変数として解釈できます。ここで、$`|\cat{C}_{/X}|`$ は、$`X`$ のオーバー圏〈スライス圏〉の対象の集合です。ストリング図のワイヤーの端点のラベルが変数だという絵図的解釈もあります。まー、細かいことはともかく、変数を含んだ型判断も圏論的に解釈できるってことです。

さて、次のような場合はどうしましょう。

$`\quad g := (x : X, y : Y \vdash \tau : Z) \In \cat{C}`$

圏 $`\cat{C}`$ が直積を持つなら、$`g:X\times Y \to Z \In \cat{C}`$ を、項 $`\tau`$ で定義していると見ればいいでしょう。

別な解釈としては、$`\cat{C}`$ は複圏〈multicategory | オペラッド | operad〉だとして、複射 $`g`$ を項 $`\tau`$ で定義していると見ます。これなら、直積がなくても大丈夫です。複圏／複射がよく分からなかったら、デカルト圏（直積を持つ圏）だけ考えていてもいいです。

大事なことは、型判断を見たら、それは圏または複圏の射を定義しているんだ、と解釈することです。型判断、つまり射の定義と、定義された射のプロファイルを常に一緒に考えましょう。

  • 型判断〈定義〉： $`g := (x : X, y : Y \vdash \tau : Z) \In \cat{C}`$
  • 射のプロファイル： $`g: X \times Y \to Z \In \cat{C}`$

省略された型判断

型判断 $`x : X, y : Y \vdash \tau : Z`$ は、何らかの圏（または複圏）のなかで、項 $`\tau`$ で射を定義している（名前は付けてない）とみなせます。が、型判断の一部が省略されることがあります。省略された部分を自分で補って解釈する必要があります。

引数変数の省略

次の形です。

$`\quad X, Y \vdash \tau : Z`$

項 $`\tau`$ を、変数を使わないで（ポイントフリースタイルで）書いているなら、変数は不要です。

シェルスクリプトのように、引数変数を番号で識別するなら、名前を宣言する必要はありません。つまり、

$`\quad \text{\$1} : X, \text{\$2} : Y \vdash \tau : Z`$

で、項 $`\tau`$ 内では $`\text{\$1, \$2}`$ を使っているということです。

あるいは、単にものぐさして変数を省略しているだけかも知れません。

引数型の省略

次の形です。項 $`\tau`$ 内で $`x, y`$ を使っています。

$`\quad x, y \vdash \tau : Z`$

変数の型が前もって約束されているか、値から型を推測できるときは型（圏の対象）を省略する可能性があります。

引数リスト全体の省略

次の形です。

$`\quad \vdash \tau : Z`$

型理論の型判断では、$`\vdash`$ の左の引数リストはコンテキスト〈context〉と呼びます（これも方言です）。

コンテキストが省略されている場合、項 $`\tau`$ は変数を含まず、型 $`Z`$ の定数を定義しているのでしょう。つまり、

  • 型判断〈定義〉： $`a := ( \vdash \tau : Z) \In \cat{C}`$
  • 射のプロファイル： $`a: {\bf 1} \to Z \In \cat{C}`$ （$`{\bf 1}`$ は $`\cat{C}`$ の終対象）

別な可能性として、コンテキストがほんとはあるのだけど、面倒だから書いてないだけかも知れません。

項の省略

次の形です。

$`\quad x: X, y: Y \vdash Z`$

あるいは、引数変数も省略して：

$`\quad X, Y \vdash Z`$

これが一番困るヤツです。が、多用されます。解釈は二通りあって：

  1. $` X, Y \vdash \tau : Z`$ となる項 $`\tau`$ （で定義される射）の存在を主張している。
  2. $` X, Y \vdash \tau : Z`$ となる項 $`\tau`$ （で定義される射）を構成することを要求している。

一番目が事実を述べている平叙文、二番目は疑問文か命令文です。この二種を区別しないのはひどすぎると思うので、僕は次のように書き分けています。

  1. 存在の主張なら $` X, Y \vdash! \;Z`$
  2. 構成の要求なら $` X, Y \vdash? \;Z`$

証明ソフトウェアでは、構成の要求を「ゴール」と呼びます。$`\vdash`$ の右側〈ターゲット〉も「ゴール」と呼ぶので、しばしば意味不明になります*1。

いつか修正されるかも知れませんが、今日の時点で引用すると（強調は檜山）： https://leanprover.github.io/reference/tactics.html#basic-tactics

This tactic applies to a goal whose goal has the form t ~ u where ~ is a reflexive relation,

このタクティクは、ゴールが t ~ u （~ は反射的関係）という形のゴールに対して適用される。

余談ですが、証明ソフトウェアの説明に出てくる「ゴール」の意味が：

  1. 対話的ソフトウェアの状態のこと
  2. 状態に含まれるどれかのゴール〈要求〉のこと
  3. フォーカスされているカレントゴールのこと
  4. ゴールのターゲットのこと

など曖昧で、マニュアル読んでもわかりゃしないって*2。

内部ホムの書き方

型理論やプログラミング言語における $`f : X \to Y`$ と圏論のプロファイル記述 $`f: X \to Y`$ は意味が違います。同じ矢印記号「$`\to`$」を使っているのは、おそらく、意図的に混同するように仕向けているのだと思います*3。しかし、異なる意味の矢印を混同すると、カリー化という大事な概念が理解できなくなります。あるいは、理解したつもりになって誤解したままになります。

圏論で通常 $`[X, Y]`$ と書かれるのは対象です。指数対象〈exponential object〉とか内部ホム対象〈internal hom object〉と呼びます。単に「指数」「内部ホム」ともいいます。集合圏での指数対象は関数集合のことです。集合圏では次の集合がすべて一致します。

  1. $`\mrm{Map}(A, B)`$ ： 集合間の写像〈関数〉達の集合
  2. $`{\bf Set}(A, B)`$ ： 圏のホムセット
  3. $`[A, B] = B^A`$ ： 指数対象〈内部ホム対象〉

さて、型理論やプログラミング言語における $`f : X \to Y`$ の圏論的解釈は、

$`\quad f:{\bf 1} \to [X, Y] \In \cat{C}`$

です。このことは、「Haskellの二重コロン「::」とバインド記号「>>=」の説明」に書いています。

記法の折衷案として、「タプル・コタプルとVΣ計算」で採用したように、内部ホム対象〈指数対象〉は $`[X \to Y]`$ と書きます。ブラケットは省略できません。

さらに、プロファイルに矢印が出現しないときは、$`{\bf 1}\to`$ を補うと約束します。このルールのもとで：

  • $`f:[X \to Y]`$ （略記）
  • $`f:{\bf 1} \to [X \to Y]`$ （$`{\bf 1}\to`$ を補う）

また、入れ子になった内部ホムの内側のブラケットは省略していいとします。

  • $`h:[X \to Y \to Z ]`$ （略記）
  • $`h:[X \to [Y \to Z] ]`$ （ブラケットを補う）
  • $`h:{\bf 1} \to [X \to [Y \to Z] ]`$ （$`{\bf 1}\to`$ を補う）

一番外側のブラケットは省略せずに書くことは我慢してください。ブラケットに囲まれてない矢印はプロファイルの区切りです。

ホムセットの書き方

圏 $`\cat{C}`$ のホムセットは $`\cat{C}(X, Y)`$ と書くのが定着してます。古くは $`\mrm{Hom}_{\cat{C}}(X, Y)`$ がよく使われていました（今でも使う人はいます）。

ホムセット（外部ホム）と内部ホムの記法フレバーを合わせて、かつ簡潔に書けるように次の約束をします*4。

  • ホムセット $`\cat{C}(X, Y)`$ を $`\cat{C}\{X \to Y\}`$ とも書く。圏 $`\cat{C}`$ が周知のときは単に $`\{X \to Y\}`$ と書いてもよい。
  • デカルト閉圏 $`\cat{C}(X, Y)`$ の内部ホム〈指数対象〉を $`\cat{C}[X \to Y]`$ とも書く。圏 $`\cat{C}`$ が周知のときは単に $`[X \to Y]`$ と書いてもよい（既に約束済み）。

集合圏では、$`{\bf Set}\{ X \to Y \} = {\bf Set}[X \to Y]`$ です。このことから、ホムセットと内部ホムが混同されたり（誤って無意識に）同一視されたりしますが、一般には、ホムセットと内部ホムは別物です。

ベキ集合 $`\mrm{Pow}(\{1, 2\})`$ は8つの要素を持つ順序集合になります。順序からやせた圏〈thin category〉の構造が入ります。部分集合の共通部分を直積、全体集合を終対象、$`X^c\cup Y`$ を指数としてデカルト閉圏になります。

幾つかの対象ペアに対して、ホムセットと内部ホムを求めてみます。

  • $`\{\emptyset \to \{1, 2\} \} = \{ \emptyset \subseteq \{1, 2\} \}`$ （単元集合）
  • $`[\emptyset \to \{1, 2\}] = \emptyset^c \cup \{1, 2\} = \{1, 2\}`$ （二元集合）
  • $`\{ \{1\} \to \{ 2\}\} = \emptyset`$ （空集合）
  • $`[ \{1\} \to \{ 2\} ] = \{1\}^c \cup \{ 2\} = \{ 2\}`$ （単元集合）
  • $`\{ \{1\} \to \{1, 2\}\} = \{ \{1\} \subseteq \{1, 2\} \}`$ （単元集合）
  • $`[ \{1\} \to \{1, 2\} ] = \{1\}^c \cup \{1, 2\} = \{1, 2\}`$ （二元集合）
  • $`\{ \{1\} \to \{ 1\}\} = \{ \{1\} \subseteq \{ 1\}\}`$ （単元集合）
  • $`[ \{1\} \to \{ 1\} ] = \{1\}^c \cup \{ 1\} = \{1, 2\}`$ （二元集合）

ホムセット〈外部ホム〉と内部ホムは別物です。

矢印の端に何も書いてないとき

ゲンツェンのシーケント計算はメチャクチャうまくできた計算体系です。矢印やカンマを杜撰〈ずさん〉に、しかし巧みにあやつることにより、計算を遂行します。が、計算の意味は「Don't think. Feel.」（「プロ関手のコエンド同値関係」参照）なので、入門もトレーニングも困難です。

シーケント計算では、「矢印（$`\to`$ または $`\vdash`$）の左に何も書いてなかったら真があると思い、右に何も書いてなかったら偽があると思え」というルールがあります。謎なルールですが、うまく働きます。

我々もゲンツェンに倣い、「矢印の左に何も書いてなかったら終対象 $`{\bf 1}`$ があると思え」というルールを追加します（終対象の記号 $`{\bf 1}`$ はオーバーロードしてます）。

$`\quad \{\to Y\} = \{ {\bf 1} \to Y\} = \cat{C}\{ {\bf 1} \to Y\} = \cat{C}({\bf 1}, Y) \In {\bf Set}\\
\quad [\to Y] = [ {\bf 1} \to Y ] = \cat{C}[ {\bf 1} \to Y ] = [ {\bf 1}, Y] \In \cat{C}`$

一般的には、左デフォルト対象と右デフォルト対象を決めておいて、矢印の左端／右端が省略されたらデフォルト対象を補うことになります。

ゲンツェン流のシーケントは、“項を省略して存在を主張する型判断”と近いので、区切り記号は $`\vdash`$ でいいと思います。論理の証明可能性メタ記号 $`\vdash`$ とかぶってしまいますが、証明可能性メタ記号を、再度形式化したのがシーケントだから、オーバーロードしてもまーいいんじゃないの*5。

計算例： 指数法則

今までに決めた記法が計算に役立つか試してみましょう。

「タプル・コタプルとVΣ計算」より：

ラムダ・パイ抽象とブイ・シグマ余抽象は、次の指数法則の形でも理解できます。

$`\quad (\prod_{i\in I} A_i)^X \cong \prod_{i\in I} (A_i^X)\\
\quad Y^{\sum_{j\in J} B_j} \cong \prod_{j \in J} Y^{B_j}`$

この指数法則を計算で示してみましょう。

圏 $`\cat{C}`$ はデカルト閉圏で、インデックス集合 $`I, J`$ による極限／余極限を持つとします。極限／余極限をパイ／シグマ記号を使って書きます。

$`\quad \mrm{lim}_I A_\bullet = \Pi_I A_\bullet\\
\quad \mrm{colim}_J B_\bullet = \Sigma_J B_\bullet
`$

ここで、黒丸は、インデックス変数を書いたときにインデックス変数が入る場所を示します。実際にインデックス変数を書いてみると：

$`\quad \mrm{lim}_{i\in I} A_i = \Pi_{i:I} A_i \\
\quad \mrm{colim}_{j\in J} B_j = \Sigma_{j:I} B_j`$

これは、$`A(\bullet), A_\bullet, A[\bullet]`$ のような“書き方の違い”を識別するだけなので、気分だけの問題で書いています。が、$`A`$ にインデックスが入るんだ、という目印にはなります。

ギリシャ文字大文字の $`\Pi, \Sigma`$ は公理的に定義される極限／余極限の記号ですが、総積記号／総和記号 $`\prod, \sum`$ は集合圏における具体的なパイ構成／シグマ構成の意味で使います。手書きだと区別が難しいですが、抽象レベルでは同じ概念なので、区別がつかなくても別に困りません。

集合圏とは限らない圏 $`\cat{C}`$ における指数法則は次のように計算できます。

$`\quad \{ X \to \Pi_I A_\bullet\}\\
\cong \prod_I \{ X \to A_\bullet\} \\
\cong \prod_I \{ \to [X \to A_\bullet] \} \\
\cong \{ \to \Pi_I [X \to A_\bullet] \}`$

$`\quad \{ \Sigma_J B_\bullet \to Y \}\\
\cong \prod_J \{ B_\bullet \to Y \} \\
\cong \prod_J \{ \to [B_\bullet \to Y] \}\\
\cong \{ \to \Pi_J [B_\bullet \to Y] \}`$

使っているのは、極限／余極限の性質とカリー化／反カリー化だけです。見やすくて楽ちんです。念のため、よく使われている普通の記法で書くと：

$`\quad \cat{C}( X, \Pi_{i:I} A_i ) \cong \cat{C}({\bf 1} , \Pi_{i:I} [X, A_i] )\\
\quad \cat{C}( \Sigma_{j:J} B_j, Y ) \cong \cat{C}({\bf 1}, \Pi_{j:J} [B_j, Y])`$

集合圏なら、先に引用した形の指数法則になります。

*1:[追記]そういえば、命題の証明（仮定・前提じゃない）のことを仮説〈hypothesis〉と呼ぶという、意味不明な習慣もありました。[/追記]

*2:「医者の不養生」「紺屋の白袴」なんてことわざがありますが、証明ソフトウェアのマニュアルや論理の教科書が、曖昧な言い回しで書かれているのには閉口します。

*3:ベータ変換を等式のように考えれば、一般の射と、終対象から指数対象への射を区別する必要はない、という意見もあります。僕は反対ですけど。

*4:これらの書き方は、手で書きながら口頭で説明のときにかなり便利です。

*5:論理だけの議論なら、シーケント区切り記号と証明可能性メタ記号は区別したほうがいいです。