昨日の記事「Proofs-as-Terms が説明困難な事情： n回目の整理」で、カリー／ハワード／ランベック対応を話題にしました。カリー／ハワード／ランベック対応そのものよりは、分野ごとの用語・記法の食い違いや錯綜・混乱に焦点を当てています。
昨日の記事で次のように言いました。
語句レベルではなくて文レベルの対応が必要です。逐語訳ではホントにまったく全然ダメで、分野ごとの文化的違いまで考慮して意訳する必要があります。
必要な文はどのくらいあるでしょうか？ 考えてみると、意外に少ないようです。幾つかの文に対して、各分野で“どう言うか”の翻訳パターン集を準備すればよさそうです。が、もうひとつのアプローチとして、分野に寄らない共通表現（ニュートラルな言い回し）を決めて、共通表現から各分野への翻訳を考えてもいいでしょう。
この記事では、圏論の記法で $`f: A \to B`$ と書かれることに対する共通表現を決めます。抽象的・概念的には $`f: A \to B`$ だけです。“それだけ”なのに、言い回しが山のようにあって人を困惑・混乱させるのです。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
%\newcommand{\msf}[1]{\mathsf{#1}}
%\newcommand{\mbb}[1]{\mathbb{#1}}
%\newcommand{\mcal}[1]{\mathcal{#1}}
%\newcommand{\msc}[1]{\mathscr{#1}}
%\newcommand{\u}[1]{\underline{#1} }
\newcommand{\In}{\text{ in } }
%\newcommand{\hyp}{\text{－} }
\newcommand{\Equiv}{ \Leftrightarrow }
\newcommand{\T}[1]{ \text{#1} }
%\newcommand{\op}{\mathrm{op} }
%\newcommand{\id}{\mathrm{id} }
%\newcommand{\dto}{\looparrowright} % dependent to
%\newcommand{\hto}{\rightsquigarrow} % hetero to
%\newcommand{\parto}{\supset\!\to}
`$
内容：
はじめに
カリー／ハワード／ランベック対応〈Curry-Howard-Lambek correspondence〉には次の分野が関与します。
- 型付きラムダ計算
- 型付きラムダ計算の型システムを与える型理論
- 論理
そして、より抽象度が高い枠組みを与えるために圏論が使われます。
ラムダ計算、型理論、論理、圏論で使われる用語・記法、文レベルの言い回しがあまりにも食い違っていて、「頭おかしくなりそうだ、勘弁してくれ」が僕の長年の悩みです。
救いは、圏論の語彙を使って整理すれば、各分野のゴチャゴチャ・ワチャワチャを切り捨てたクリアな描像が得られることです。これがまさにカリー／ハワード／ランベック対応の内容・内実だとも言えます。
圏論における最も基本的な主張は次の形です。
- $`f:A \to B \In \cat{C}`$
型理論ではファイバー付き圏〈fibered category〉$`\pi: \cat{E}\to \cat{C}`$ がよく使われます。ファイバー付き圏だと次の形の主張が使われます。
- $`\varphi : X \to Y \In \cat{C}`$ （ベース圏の射）
- $`f : A \to B \In \cat{E}_{@X}`$ （ファイバー内の射）
ここで、$`\cat{E}_{@X}`$ は $`X\in |\cat{C}|`$ 上のファイバーです。
$`f:A \to B`$ をニュートラルな言い回しで言えば、「$`f`$ は、$`A`$ から $`B`$ への射である」となります。論理での言い回しは、
- 証明 $`f`$ は、命題 $`A`$ を仮定して、結論である命題 $`B`$ を導く
となります。
証明 $`f`$ を省略する（あえて言及はしない）と：
- 命題 $`A`$ を仮定して、命題 $`B`$ を証明できる
別な言い回しは：
- 命題 $`B`$ は、命題 $`A`$ を仮定すれば証明できる
- 命題 $`B`$ は、命題 $`A`$ のもとで成立する
- 命題 $`B`$ は、前提 $`A`$ において正しい
- ‥‥
$`A`$ も省略してしまうと：
- 命題 $`B`$ は証明できる
- 命題 $`B`$ は証明可能
- 命題 $`B`$ は成立する
- 命題 $`B`$ は正しい
- ‥‥
型理論は型理論でまた独特の言い回しと言い回しの変種達を使います（「型理論における呼び名と言い回しは？」参照）。
「呼び名や言い回しなんて関係ないんだ！ どうでもいいんだ！！」と叫びたくなりますが、そうはいっても、各分野の呼び名と言い回しを全否定することも現実性がないです。
そんな事情なので、どの分野のものでもない、中立的な言い回し（文のパターン）を準備します（次節）。
動詞 support を使った文
この節では、LaTeX数式を使わずに、f: A → B のように単なるテキストを使います。
f: A → B を表現する英語モドキの文を考えます。モドキであって正しい英文にはなりません。英文法を引き合いに出して文句つけるのはやめてくださいね。
f:A → B という圏論的主張に対して、「f と A が B をサポートしている〈支えている〉」と想定します。そのことを次のように表現します。
- (f with A) support B
f と A は役割りが違う（対等ではない）ので f and A とは書きません。
B を主語として受動態の文で書くなら：
- B is supported by f with A
- B is supported with A by f
繰り返しますが、英文としての正しさは度外視してください。
A を主語とするなら：
- A supports B by f
f を主語とするなら：
- f supports B with A
ここまでは、f, A, B という3つの構成素があって、それぞれを主語とした場合の文でした。ここから先は、構成素を省略した場合の文です。
f を省略して A, B だけ：
- A supports B
- B is supported with A
A を省略して f, B だけ：
- f supports B
- B is supported by f
「B を省略して f, A だけ」はありません。そういう言い回しは使わないのです。
f, A を省略して B だけ：
- B is supported
以上の英語モドキの文達は、すべて f:A → B を表現しています。言い回しに違いがあるだけで、意味するところは同じです。こんな英語モドキに何の意味があるんだ？ それは、単純な単一の圏論的事実 $`f:A \to B \In \cat{C}`$ に対して、それを言い表す文は多様であることに慣れるトレーニングに使えます。
使われている様々な（あるいはグチャグチャな）呼び名・言い回しに惑わされることなく、呼び名・言い回しの違いをすべて無視して、背後にある単純で単一の事実を見抜くトレーニングが（多くの人には）必要そうに思えるのです。
事例： ベキ集合
集合 $`X`$ を固定して、ベキ集合 $`\mrm{Pow}(X)`$ を考えます。$`\mrm{Pow}(X)`$ の要素を対象として、包含写像を射とする圏を $`\mbf{X}`$ （ボールト体に注意）とします。
- 圏 $`\mbf{X}`$ の対象は、集合 $`X`$ の部分集合 $`A, B`$ などである。
- 圏 $`\mbf{X}`$ の射は、包含関係 $`A \subseteq B`$ に対応する包含写像 $`i: A \to B`$ である。
$`i : A \to B \In \mbf{X}`$ は次のように表現できます（英文モドキに対応する日本語も添えます）。
- (i with A) support B
- i は A と一緒に、B を支える
i, A, B が何であるかを明示した日本語文は：
- 包含写像 i は部分集合 A と一緒に、部分集合 B を支える
くどいですが、言ってることは $`i : A \to B \In \mbf{X}`$ です。それ以上の意味はありません。
他の言い回しの幾つかを以下に並べます。
A が主語
- A supports B by i
- 部分集合 A は、包含写像 i により 部分集合 B を支える
B が主語、受動態
- B is supported by i with A
- 部分集合 B は、部分集合 A と一緒の包含写像 i により支えられる
A が主語、i を省略
- A supports B
- 部分集合 A は、部分集合 B を支える
B が主語、受動態、i を省略
- B is supported with A
- 部分集合 B は、部分集合 A で支えられる
by, with の違いを「により」、「で」で表しています。
B が主語、受動態、i, A を省略
- B is supported
- 部分集合 B は支えられている
事例： 論理の意味論
集合 $`X`$ を固定して、$`X`$ 上の述語（ブール値の関数）達の集合 $`\mrm{Pred}(X)`$ を考えます。$`\mrm{Pred}(X)`$ の要素を対象として、述語のあいだの論理順序を射とする圏を $`\mbf{X'}`$ とします。論理順序とは、以下のように定義される順序です。
$`\T{For }p, q \in \mrm{Pred}(X)\\
\quad p \preceq q :\Equiv \forall x\in X.\, p(x) \le q(x)
`$
順序 $`\le`$ は、$`0 \lt 1`$（偽は真より小さい）として定義されるブール値のあいだの順序とします。
論理順序を射と考えるのは、前節の「包含関係を射と考える」のと同じ発想です。
- 圏 $`\mbf{X'}`$ の対象は、集合 $`X`$ 上の述語 $`p, q`$ などである。
- 圏 $`\mbf{X'}`$ の射は、論理順序 $`p \preceq q`$ に対応する論理順序射（仮想的な写像） $`i: p \to q`$ である。
$`i : p \to q \In \mbf{X'}`$ は次のように言えます。
- (i with p) support q
- i は p と一緒に、q を支える
論理の話であるという事情により、support を guarantee〈保証する〉に置き換えましょう。
- (i with p) guarantee q
- i は p と一緒に、q を保証する
- 論理順序射 i は述語 p と一緒に、述語 q を保証する
他の言い回しの幾つかを以下に並べます。
p が主語
- p guarantees q by i
- 述語 p は、論理順序射 i により 述語 q を保証する
q が主語、受動態
- q is guaranteed by i with p
- 述語 q は、述語 p と一緒の論理順序射 i により保証される
p が主語、i を省略
- p guarantees q
- 述語 p は、述語 q を保証する
q が主語、受動態、i を省略
- q is guaranteed with p
- 述語 q は、述語 p で保証される
q が主語、受動態、i, p を省略
- q is guaranteed
- 述語 q は保証されている
論理の習慣として、p が省略されたときは、p は恒真な述語 T だとみなします。つまり：
q が主語、受動態、i, p を省略
- q is guaranteed (with T)
- 述語 q は (T で) 保証されている
これは、述語 q が恒真なことを意味します。
事例： 論理の構文論
集合 $`X`$ を固定して、$`X`$ 上で意味を持つ論理式達の集合 $`\mrm{Formula}(X)`$ を考えます。$`\mrm{Formula}(X)`$ の要素を対象として、論理式のあいだの証明を射とする圏を $`\mbf{X''}`$ とします。
- 圏 $`\mbf{X''}`$ の対象は、集合 $`X`$ 上の論理式 $`P, Q`$ などである。
- 圏 $`\mbf{X''}`$ の射は、証明 $`i: P \to Q`$ である。
$`i : P \to Q \In \mbf{X''}`$ は次のように言えます。
- (i with P) guarantee Q
- i は P と一緒に、Q を保証する
- 証明 i は論理式 P と一緒に、論理式 Q を保証する
他の言い回しの幾つかを以下に並べます。
P が主語
- P guarantees Q by i
- 論理式 P は、証明 i により 論理式 Q を保証する
Q が主語、受動態
- Q is guaranteed by i with P
- 論理式 Q は、論理式 P と一緒の証明 i により保証される
P が主語、i を省略
- P guarantees Q
- 論理式 P は、論理式 Q を保証する
Q が主語、受動態、i を省略
- Q is guaranteed with P
- 論理式 Q は、論理式 P で保証される
Q が主語、受動態、i, P を省略
- Q is guaranteed
- 論理式 Q は保証されている
前節と同様な理由（習慣）により、P が省略されたときは、P は真を表す論理定数 T だとみなします。つまり：
Q が主語、受動態、i, P を省略
- Q is guaranteed (with T)
- 論理式 Q は (T で) 保証されている
これは、論理式 Q が仮定なしに証明された論理式であることを意味します。
分析
ベキ集合の事例で出した圏 $`\mbf{X}`$ は、定義により圏です。よく見る圏と変わった点があるとすれば、2つの対象のあいだの射が高々1本であり、やせた圏〈thin category〉なことです。しかし、やせた圏も圏であり、圏論的概念はすべて適用できます。
$`i:A \to B \In \mbf{X}`$ のニュートラルな（クセのない）表現は「$`i`$ は、$`A`$ から $`B`$ への射である」です。$`\mbf{X}`$ という特定の圏の実情としては「$`i`$ は包含写像である」とか「$`A`$ は $`B`$ の部分集合である」とかありますが、だからといって一般的圏論で扱えないなんてことはありません。
述語の事例の圏 $`\mbf{X'}`$ は、圏 $`\mbf{X}`$ と事実上同じ圏です。$`\mbf{X'}`$ と $`\mbf{X}`$ に関する議論はまったく同じです。違うとすれば、呼び名と言い回しだけです。呼び名や言い回しなんて関係ないんだ！ どうでもいいんだ！！
論理式と証明の圏 $`\mbf{X''}`$ は、論理の構文論側の圏です。$`\mbf{X''}\to \mbf{X'}`$ という関手があります。その関手は、論理の構文に意味を対応させます。構文論と意味論を区別しない（曖昧にする）悪しき習慣では、論理式も述語もどちらも命題と呼び、構文的対象物である証明とその意味である論理順序も区別しません。困ったもんだ。
論理の構文に意味を対応させる関手を $`\mrm{S}`$ 、$`\mbf{X'}`$ と $`\mbf{X}`$ の圏同型を与える関手を $`\mrm{E}`$ とすると、以下の可換図式が得られます。$`\mrm{S'}`$ は、 $`\mrm{S}`$ と $`\mrm{E}`$ の結合〈composition〉です。
$`\quad \xymatrix{
\mbf{X''} \ar[r]^{\mrm{S}} \ar[dr]_{\mrm{S'}}
&\mbf{X'} \ar[d]^{\mrm{E}}
\\
{}
&\mbf{X}
}\\
\quad \T{commutative }\In \mbf{Cat}
`$
この可換図式は、カリー／ハワード／ランベック対応のトイモデル（とても簡単な典型的事例）になっています。このトイモデルを理解するときに、呼び名や言い回しの違いから生じるグチャグチャが障害になっているのではないか？ というのが僕の仮説です。個人的経験からは、仮説というよりは事実です。
トイモデルより本格的なカリー／ハワード／ランベック対応では、用語・記法まわりのグチャグチャはさらにひどいものになります。グチャグチャを整理するため、グチャグチャを乗り越えるために、動詞 support を使った共通表現や、論理向けの guarantee への置き換えを使ったトレーニングは有効ではないか、と思います。
