証明図風縦書き記法と6つの悪習 (TBD) - (2nd) 檜山正幸のキマイラ飼育記

まだ未完成、出来上がったら本編に移します。

いきなりですが、“自然演繹の証明図”風の図の例を2つ挙げます。

  A   B
 -------
  A∧B

   A
  ---
   A

そして、“シーケント計算の証明図”風の図の例も2つ：

  A → B   B → C
 --------------- 
    A → C

   ☆
 -------
  A → A

これらの図は、上から下に向かって読むので縦書き記法で描かれていると言っていいでしょう（横書き部分もありますが）。このテの図が使えれば便利です。論理に限らず、圏論／計算科学のなかでも使える場面は数多くあります。が、あまり評判は良くありません。

横棒（連続するマイナス記号で書いています）を含む縦書き図が理解できない／難しい、という嘆きは何度か何人かから聞いたことがあります。なぜ難しいのでしょうか？内容的に難しいというよりは、好ましくない暗黙の了解事項が多すぎるのです。「好ましくない暗黙の了解事項」を「悪習」と呼ぶことにします。理解を妨げ、無駄な難解さを生み出している悪習を説明することにより、縦書き図への障壁を取り除きたいと思います*1。

事例として使うのはモノイド圏だけなので、論理に関する知識は不要です。モノイド圏が出てくるので、圏論の初歩的知識は要ります。

内容：

モノイド圏
6つの悪習
多変数関数と多値関数
単純プロファイル、複プロファイル、多プロファイル
縦書き記法
複射、多射の縦書き
実例：モノイド積を表す縦書き図
要素対応の縦書き図
セマンティクスの話とその他の事例

モノイド圏

集合圏Setは、集合の直積 × と特定された単元集合 1 = {0} を持ちます。× と 1 は、モノイド類似の法則を満たします。

For A, B, C∈|Set|, (A×B)×C $\cong$ A×(B×C)
For A∈|Set|, 1×A $\cong$ A
For A∈|Set|, A×1 $\cong$ A

直積は、対象〈集合〉に対してだけではなく、射〈写像 | 関数〉に対しても定義できます。（以下の定義内で、ペア（二項のタプル）を囲む括弧と、引数渡し〈評価〉の括弧を省略せずに書いています。）

For f:A → X, g:B → Y in Set
For (a, b)∈A×B
Define (f×g)((a, b)) := (f(a), g(b)) ∈X×Y

射に対する × と射の結合 ; は“いい感じに協調”します。例えば、次が成立します。

For f:A → X, g:B → Y, h:X → S, k:Y → T in Set
(f×g);(h×k) = (f;h)×(g;k) :A×B → S×T in Set

以上の説明は、(Set, ×, 1) がモノイド圏になると言いたかったのですが、正確な話ではないので、必要と興味があればモノイド圏のちゃんとした定義を参照してください。

Setは直積に関してモノイド圏ですが、Setの部分圏となるモノイド圏も作れます。Nは自然数全体の集合、B = {true, false} はブール値〈真偽値〉の集合とします。集合の集合〈類〉 $\mathscr{X}$ を次のように定義します。

$\mathscr{X}$ := {X∈|Set| | X は、1, N, B を成分〈因子〉とする直積の形に書ける}

次のような集合は $\mathscr{X}$ に入ります。

1, N, B
1×1, N×B, N×N
1×1×1, N×B×1, N×N×B

集合圏Setの部分圏Xを次のように定義します。

|X| := $\mathscr{X}$
For A, B∈|X|, X(A, B) := Set(A, B)
結合と恒等射はSetから引き継ぐ。

こうして作ったSetの部分圏 (X, ×, 1) もモノイド圏になります。

さらに別なモノイド圏の例を挙げます。NOを、自然数全体の集合Nの大小順序から得られるやせた圏とします。× を普通の自然数の掛け算として、(NO, ×, 1) はモノイド圏になります。足し算を使った (NO, +, 0) もモノイド圏です。

6つの悪習

冒頭で言った「理解を妨げ、無駄な難解さを生み出している悪習」を列挙しましょう。

集合のあいだの写像と要素対応の区別が曖昧
集合の要素とポインティング写像の扱いが曖昧
射のプロファイルにおいて、圏を省略
多変数関数、多値関数の扱いが曖昧
リスト／タプルの囲み括弧の省略
空白の乱用

最初の3つはこの節で説明します（残りは次節以降）。

写像 f:A → B は集合圏の射です。集合圏特有の事情として、「対象〈集合〉の要素」という概念が使えます。要素 a∈A を選べば、写像による値 b = f(a) ∈B が確定します。fにより、特定要素に対して特定要素が対応することを、次の書き方で表すことにします。

$A\ni a \stackrel{f}{\mapsto} b \in B$

上記の書き方で表される要素対応は、集合のあいだの写像fとは区別すべきものです。要素対応の要素 a∈A は特定された個体なので、他の要素は考えてません。一方、写像fは、集合A全体に渡る対応を一挙に考えたものです。

[補足]
要素対応を形式的に定義したいなら、f:A → B in Set, a∈A, b∈B の3つ組 (f, a, b) を考えて、次の条件を満たすものを、ｆの要素対応と定義すればいいでしょう。

f(a) = b

要素の圏〈category of elements〉（https://en.wikipedia.org/wiki/Category_of_elements 参照）を使うと、要素対応を射として定義できます。
[/補足]

当然ながら、（空集合でなければ）集合には要素がありますが、「要素」概念を使いたくないときがあります。そのとき、その要素をポインティングする写像を代わりに使います。要素 a∈A をポインティングする写像を a^~:1 → A とすると、その定義は：

a^~(0) := a

要素aとポインティング写像a^~はしばしば同一視されますが、同一視というのは一旦は区別してからするものです。ゴッチャにしていいわけではありません。

圏の射fの域と余域を明示したいとき f:A → B と書きます。「A → B」の部分をfのプロファイル〈profile〉と呼びます。複数の圏、例えばCとDを考えているときは、f:A → B in C, g:X → Y in D のように、圏を添えないと射の素性〈すじょう〉がハッキリしません。複数の圏を扱っているのに、プロファイルに圏を書かないと、理解困難な状況になります。

最初の3つの悪習への対処をまとめると：

要素対応は $A\ni a \stackrel{f}{\mapsto} b \in B$ のように書く。もう少し簡略化した $f:a \mapsto b$ や $a \mapsto f(a)$ とかでもよい。
要素aとポインティング写像a^~は区別する。
f:A → B in C のように、「in」に続けて圏（射の生息地）を明示する。

多変数関数と多値関数

2つの集合 A, B があって、集合Aの要素と集合Bの要素を入力とする写像fは、二変数関数または二引数関数と呼びます。同様に、三変数関数、四変数関数、‥‥ 一般的な多変数関数を考えることができます。（言わずもがなですが、「写像」と「関数」は完全に同義語です。）

多変数関数（とりあえず二変数関数）fのプロファイルを、二種類の書き方で書いてみます。

f:A×B → C
f:A, B → C

上の2つのプロファイルは、単に書き方〈表記法〉の違いでしょうか？そうとも言えないのです。実質的に同じなのは事実なのですが、「区別する必要はない」は言いすぎです。区別する必要があります。

圏論のなかで、圏の兄弟のような概念に複圏〈multicategory〉と多圏〈polycategory〉があります。ものすごく大雑把に紹介すると：

複圏の射は複射と呼び、多入力一出力〈n-in 1-out〉の操作を表す。
多圏の射は多射と呼び、多入力多出力〈n-in m-out〉の操作を表す。

通常の圏の射は一入力一出力〈1-in 1-out〉操作を表すものです。写像fを f:A×B → C と書いたとき、fはペア〈二項タプル | 長さ2のリスト〉をひとつだけ受け取って値を返します。つまり、一入力一出力〈1-in 1-out〉なのです。一方 f:A, B → C と書いたら、二入力一出力の関数です。

写像gのプロファイルが g:A → B×C ならば、集合Aの要素をひとつ受け取って、B×Cの要素であるペアをひとつだけ返します。これも一入力一出力〈1-in 1-out〉です。しかし、g:A → B, C ならば、ふたつの値（最初の値はBの要素、二番目の値はCの要素）を返します、多値関数ですね*2。

このように説明すると、「言葉づかい〈日本語の表現〉の違いだけではないか」と思う人も多いでしょう。自然言語〈日本語〉の説明では明確な違いを説明することは無理なのです。そこで、複圏と多圏を持ち出して形式的な違いと関連性を定式化するわけです。「実質的に同じだが、区別する必要がある」に正確な意味を与えます。

モノイド圏Cがあると、Cに付随する複圏と多圏を容易に構成できます。付随する複圏の複射により「Cの対象に対する多入力一出力の射」を表現し、付随する多圏の多射により「Cの対象に対する多入力多出力の射」を表現します。今ここでは、複圏と多圏の話をこれ以上しませんが、興味があれば、次の記事を読んでみてください。

ネーミングルールとして、次を採用しましょう。

モノイド圏Cに付随する複圏を MultiC と命名する。
モノイド圏Cに付随する多圏と PolyC と命名する。

例えば、モノイド圏としてのSetから作られる複圏は MultiSet、多圏は PolySet となります。

MultiSet ：多変数関数の結合を扱う計算体系
PolySet ：多変数多値関数の結合を扱う計算体系

Setの射（写像）、MultiSetの複射（多変数写像）、PolySet の多射（多変数多値写像）のあいだには容易に想像できる対応関係があります。例えば：

(射 f:A×B → C×D) ←→ (複射 f':A, B → C×D) ←→ (多射 f'':A, B → C, D)

これが、「実質的に同じだが、区別する必要がある」状況です。

[補足]
上のネーミングルールの PolyC とは、「対称モノイド多圏（簡約版）」において、対称モノイド圏Cの置換挿入済みの標準簡約多圏〈permutation-inserted standard reduced polycategory〉と呼び、PermStdPoly(C) と書いていた圏のことです。我々が使うすべての多圏が PermStdPoly(C) の形ではありませんが、PermStdPoly(C) なら非常に扱いやすいです。

対称モノイド圏から、標準的な（対称性を持つ）複圏が構成できて、これも使いやすい複圏です。MultiC の意味は、Cから構成された標準的な複圏のことです。

この記事では、モノイド圏の対称性に明示的に触れてはいませんが、実際に使う圏は対称モノイド圏です。したがって、複数の引数の位置の交換、複数の戻り値の位置の交換は自由に出来ます。
[/補足]

なお、この記事では、モノイド圏から作られた複圏／多圏を話題にしていますが、もとになるモノイド圏なしでいきなり出現する複圏／多圏もあるので注意してください。

[補足]
複圏はオペラッド〈operad〉とも呼びます。最近は、オペラッドと呼ぶほうが多い気がします。オペラッドという言葉を使ったときは、複射をオペレーターまたはオペレーションと呼びます。

日本語だと「複圏の複射」「多圏の多射」と語呂がいいのですが、英語の "a multimorphism {of | in} a multicategory", "a polymorphism {of | in} a polycategory" は問題があります。polymorphism がコンピューター／プログラミング関係で別な意味で使われているので衝突を避けて polyarrow, polymap が使われるようです。かまわずに polymorphism を使う人もいますが。

MultiSetというと、データ構造としてのマルチセット〈バッグ〉を連想する人がいるかも知れませんが、偶然の一致で、マルチセット〈バッグ〉とは何の関係もありません。多入力一出力の関数を定式化する枠組みがMultiSetです。
[/補足]

単純プロファイル、複プロファイル、多プロファイル

モノイド圏 C = (C, ×, I) の射 f, g のプロファイルを f:A×B → C, g:A → B×C in C と書いたとき、これは一入力一出力を表すプロファイルです。このような、通常の圏の通常のプロファイルを単純プロファイル〈simple profile〉と呼ぶことにします。

複圏 MultiC では、プロファイルを f:A, B → C in MultiC のようにカンマを区切りに使って書きます。この形のプロファイルを複プロファイル〈multiprofile〉と呼びましょう。多圏 PolyC では、g:A → C, D in PolyC とか h:A, B → C, D in PolyC とかのプロファイルを使います。この形のプロファイルは多プロファイル〈polyprofile〉です。

さて、f:A×B → C, g:A → B×C は単純プロファイルでしたが、f, g が MultiC や PolyC の複射／多射ということは起こり得ないのでしょうか？今までの書き方だと「何とも言えない」のです。つまり、曖昧性が生じます。

曖昧性の原因はリストを囲む括弧を省略しているからです。次のルールを守れば曖昧性は解消されます。

単純プロファイルの矢印の左と右は括弧で囲まない。
複プロファイルの矢印の左は必ず括弧で囲み、矢印の右は括弧で囲まない。
多プロファイルの矢印の左と右は必ず括弧で囲む。

このルールを守れば、次のように判断できます。

f:A×B → C は単純プロファイル、fは C の射
f:(A×B) → C は複プロファイル、fは MultiC の複射
f:(A×B) → (C) は多プロファイル、fは PolyC の多射

リストとして空リストもみとめるので、次のような複プロファイル／多プロファイルがあります。

f:() → B in MultiC
f:(A) → () in PolyC
f:() → () in PolyC

面倒でも、囲み括弧をちゃんと付けて、'in'のあとに射／複射／多射が所属する圏／複圏／多圏を明示する習慣を付ければ、悪習に足を絡め取られて前に進めなくなる事態を避けられます。

なお、プロファイルの'in'の後が圏でも複圏でも多圏でもなんでも、総称してアビタ〈habitat（フランス語） | 生息地〉と呼びます。対象、射、原子的対象のリスト、複射、多射などの圏論的事物が所属する組織体、あるいは生息する地域がアビタです。

縦書き記法

やっと縦書き記法の説明です。(C, ×, I) はモノイド圏とします。Cは集合圏の部分圏とは限りません。例えば、(NO, +, 0) では、台となる圏はNを対象集合とするやせた圏で、モノイド積 × は足し算 +、モノイド単位 I は 0 です。今の「×〈掛け算〉は +〈足し算〉、I〈単位〉は 0〈零〉」のような言い方に違和感をいだく人は「「僕のおとうさん」と「お友達のおとうさん」」をよく読んでください。

さて、射fのプロファイル f:A → B in C を次のように縦書きします。

    A
   --- f in C
    B

横のものを縦にした、それだけです！ ホントにそれだけ！！

要素対応 $A\ni a \stackrel{f}{\mapsto} b \mbox{ in }{\bf Set}$ は次のように縦書きで書くことにします。

    a∈A
   +----+ f in Set
    b∈B

横棒の両端にプラス記号を置いているのは、要素対応であることを強調するためです。これを単なる横棒にすると、ほぼ間違いなく誤解と混乱をまねくので、ここではプラス記号を必ず書きます。

要素概念は集合圏Setでしか意味を持たないので、in Set は省略してもいいでしょう。その他の省略も書いてみると：

    a∈A
   +----+ f
    b∈B

    a∈A
   +----+
    b∈B

    a
   +--+ f
    b

省略部分が増えるにしたがって、誤解と混乱のリスクは高まります。簡潔さとリスクはトレードオフの関係にあります*3。

複射、多射の縦書き

複射、多射のプロファイルにはカンマが入りますが、カンマの代わりに空白も許すとします。この空白は区切り記号としての空白です。f:(A, B) → C in MultiC は、f:(A B) → C in MultiC と書いてもよいとします。

複プロファイル f:(A B) → C in MultiC を素直に縦書きすれば：

  (A  B)
 ------- f in MultiC
   C

ところが、縦書きで囲み括弧を書くのは耐え難い（誰が？）らしく、括弧を付ける習慣はありません。括弧がなくても、「in アビタ」があれば判断できるのですが、アビタも付けない。そのため、曖昧性を解消するために導入したルールが無意味化して、図の解釈はまた曖昧な世界に逆戻り。ムー。

安直な解決策は、アビタを固定してしまって、'in'の後にアビタを書かなくても固定したアビタを補う方法です。アビタを通常の圏に取ると、対象を横に並べることができないので、アビタは複圏または多圏に取ります。多圏が一番柔軟性があるので、アビタは多圏に固定したとしましょう。

多圏では、次の多プロファイルが許されます。

f:() → (B)
g:(A) → ()
g:() → ()

これらを（アビタは省略して）縦書きにすれば：

   
 --- f
  B

  A
 --- g
  


 --- h

一見戸惑いますが、実際に使われているので慣れるしかないです。僕〈檜山〉は、空白に変わる符丁〈便宜的記号〉を置いています。例えば：

  ☆ 
 --- f
  B

  A
 --- g
  ☆

  ☆
 --- h
  ☆

'☆'以外に'*'〈アスタリスク〉, '-'〈ハイフン〉なども使うことがあります。

実例：モノイド積を表す縦書き図

C = (C, ×, I) がモノイド圏だとすると、× をホムセットに制限すると次の写像が得られます。

Prod_A,X,B,Y:C(A, X)×C(B, Y) → C(A×B, X×Y) in Set

射のモノイド積 Prod_A,X,B,Y も記号'×'で書かれるので、

×:C(A, X)×C(B, Y) → C(A×B, X×Y) in Set

この書き方で'×'が4回出現しますが、右から順に次の意味です。

Cの射に対するモノイド積（の一部分）
集合（ホムセット）の直積
Cの対象に対するモノイド積
Cの対象に対するモノイド積

だいぶややこしいので、Cのモノイド積は記号'∧'に置き換えて、多変数関数を複圏 MultiSet の複射〈多変数関数〉と考えましょう。すると：

Prod_A,X,B,Y:(C(A, X), C(B, Y)) → C(A∧B, X∧Y) in MulitSet

または、

∧:(C(A, X), C(B, Y)) → C(A∧B, X∧Y) in MultiSet

これらのプロファイルを縦書きします。

  C(A, X)   C(B, Y)
 ------------------- Prod_A,X,B,Y in MultiSet
     C(A∧B, X∧Y)

  C(A, X)  C(B, Y)
 ------------------- ∧ in MultiSet
   C(A∧B, X∧Y)

考える複圏を MultiSet に固定すればアビタを省略できます。その他、さまざまな省略が可能です（省略しないのが吉ですが）。極端な省略、あるいは略記として、モノイド圏Cのホムセット C(A, X) を X → Y で書く約束をして、省略できそうなものは全部省略すると：

   A → X   B → Y
 ------------------
   A∧B → X∧Y

この極端な省略は実際に使われています*4。が、ちょっとひど過ぎるので、妥協案として、ホムセット C(A, B) の略記は [A → X] のような書き方にして、アビタも適宜付けることにします。

   [A → X]   [B → Y]
 -------------------- ∧ in MultiSet
     [A∧B → X∧Y]

要素対応の縦書き図

前節最後の図は、（二変数の）写像を表す図です。この写像の要素対応を圏Setで考えれば次のようです。

$[A \to X]\times [B \to Y] \ni (f, g) \stackrel{\land}{\mapsto} f\land g \in [A\land B \to X\land Y]$

同じことを、複圏 MultiSet のなかで考えて縦書きにすれば：

   f∈[A → X]   g∈[B → Y]
 +---------------------------+ ∧ in MultiSet
    f∧g∈[A∧B → X∧Y]

要素対応の図なので、横棒の両端にプラス記号を置いてます。

[A → X] はモノイド圏Cのホムセットだったので、次の同値があります。

f∈[A → X] ⇔ f∈C(A, X) ⇔ f:A → X in C

これを使って上の図を書き換えると：

   f:A → X in C   g:B → Y in C
 +-------------------------------+ ∧ in MultiSet
      f∧g:A∧B → X∧Y in C

上段下段に圏Cにおけるプロファイルが出てきているので、これも縦書きにすると：

    A           B
   --- f in C   --- g in C
    X           Y
 +---------------------------+ ∧ in MultiSet
     A∧B
     ---- f∧g in C 
     X∧Y

ここで、次の約束を導入します。'?'の部分に射がラベルされます。

----- ? in C は単に ----- ? と書く。
+---+ ? in MultiSet は ===== ? と書く。

この約束で描くと：

    A        B
   --- f    --- g 
    X        Y
 ==================== ∧
     A∧B
     ---- f∧g
     X∧Y

この描き方は、「自然演繹はちっとも自然じゃない -- 圏論による再考 // 圏論的に自然なリーズニングの例その1」で採用した描画法です。横棒が一本棒（マイナス記号）か二本棒（イコール記号）かは、in C か in MultiSet かを区別するためで、写像か要素対応かの区別は横棒のラベルの有り無しで判断するルールでした（僕はこのルールをハッキリとは書いてなかったと思う、よろしくない）。

図がシンプルになればなるほど情報が欠落するので、次の情報を補完する必要があります。

横棒は射を表すはずだが、その射のアビタはどこか。今の例では in PolyC か in MultiSet か？
横棒が写像（多変数写像）を表す場合、上段下段は集合なのか？それとも集合の要素なのか？（どちらとも解釈できる場合もある。）

同じ描画法が使われていても、表す対象物はまったく違うかも知れないのです。今日は話題にしませんが、Cが2-圏の場合、横棒が2-射を表すことがあります。そもそも、ミソもクソも一緒に横棒で表す図法はダメだろうとは思います。しかし、低コストで描ける代替描画法がないので、今後50年くらいは使われ続けるでしょう。現状の問題点やロングレンジで考えた場合の方向性は、次の記事に書きました。

セマンティクスの話とその他の事例

横書きであれ縦書きであれ、“自然演繹の証明図”風の図や“シーケント計算の証明図”風の図が使える場面は矢鱈に多くて多様です。そうであるなら、「個々の利用場面に影響されない機械的な構文操作に習熟するのがよい」という意見もあるでしょう。確かに、機械的な記号操作のスキルも必要ではあります。しかし、無意味な記号の操作は辛すぎませんかね。僕は嫌だな。

そういった個人的な感情から僕は、ラムダ計算でもシーケント計算でも、常にセマンティクスを一緒に考える主義です。「セマンティック駆動な圏的ラムダ計算とシーケント」という過去記事で次のように書いています。

ラムダ計算といえば、普通はまず構文をキチンと定義して、その構文に意味を割り当てます。構文領域と意味領域を独立に作って、それらを意味写像で結びつけるわけです。そして、どちらかと言えば構文領域のほうが主題です。
それに対してセマンティック駆動（semantic-driven）というのは、意味領域を先に考えることです。意味領域ありきです。構文は、意味領域上の現象を説明したり計算したりするための道具という位置付けです。構文領域の独立性や純粋性には拘らず、構文と意味を混ぜることを躊躇しません。

というわけで、構文的な存在物（記号列や絵図）を見るとセマンティクス〈意味 | 解釈〉を割り当てないと気が済まないのです。今回は、モノイド圏Cと集合圏Set、それから構成した複圏／多圏 MultiC, PolyC, MultiSet, PolySet を想定してセマンティクスを構成（あるいは想像）しています。

この記事冒頭で挙げた事例のセマンティクスを考えてみましょう。最初に次の図。

  A   B
 -------
  A∧B

これは情報が少なすぎますが、2つの解釈が思いつきます。ひとつは、モノイド圏Cの恒等射 id_A∧B:A∧B → A∧B in C の、複圏 MultiC での対応物で、(A, B) → A∧B in MultiC という複プロファイルを持つ複射です。論理の習慣に従って、この複射の名前を ∧-intro とする*5と、次のように解釈できます。

  A   B
 ------- ∧-intro in MultiC
  A∧B

あるいは、(A, B) → (A∧B) in PolyC という多プロファイルを持つ多射の可能性もあります。

  A   B
 ------- ∧-intro in PolyC
  A∧B

また別な解釈として、上記の図が上部にもっと伸びていたとします。

  X   Y
  :   :
  :   :
  A   B
 -------
  A∧B

X から A に至る（左の）経路で表現される射を f:X → A in C、Y から B に至る（右の）経路で表現される射を g:Y → B in C とすると、最下段の追加で X∧Y → A∧B の射が得られます。つまり、最初の図の見えてない部分も想定すると、次の図に相当するのかも知れません。

  f:X → A    g:Y → B
 +---------------------+ Prod_X,A,Y,B in MultiSet
    f∧g:X∧Y → A∧B

これは既に出てきた図です。以下は復習（繰り返し）となりますが、圏Cのホムセットを使って書けば：

  f∈C(X, A)   g∈C(Y, B)
 +-----------------------+ Prod_X,A,Y,B in MultiSet
    f∧g∈C(X, A∧B)

この図を圏Set内で解釈して横書きの要素対応で書けば：

$\mathcal{C}(X, A)\times \mathcal{C}(Y, B) \ni (f, g) \stackrel{Pair_{X,A,Y,B}}{\mapsto} \langle f, g\rangle\in \mathcal{C}(Y, A\land B) \mbox{ in }{\bf Set}$

写像としては：

$Prod_{X,A,Y,B} : \mathcal{C}(X, A)\times \mathcal{C}(Y, B) \to \mathcal{C}(X\land Y, A\land B) \mbox{ in }{\bf Set}$

再び複圏 MultSet 内で解釈して縦書きにすると：

  C(X, A)   C(Y, B)
 -------------------- Prod_X,A,Y,B in MultiSet
    C(X∧Y, A∧B)

こんな具合で、横書きと縦書き、要素対応と写像を入れ替えることにより、状況・事情を確認します。

次の図は簡単な形をしています。

   A
  ---
   A

これはおそらく次の意味でしょう（書いてない情報は想像補完する）。

   A
  --- id_A in C
   A

横書きにすれば：

id_A:A → A in C

もし、複射／多射ならば：

id_A:(A) → A in MultiC
id_A:(A) → (A) in PolyC

そして、次の図は、恒等射 id_A のポインティング射を表現しています。

   ☆
 -------
  A → A

☆は空白の代替記号です。

   
 ------ (id_A)^~ in MultiSet
  C(A, A)

横書きにしてみると：

(id_A)^~:() → C(A, A) in MultiSet

MultiSetにおける空リストは、Setでは1と解釈します。

(id_A)^~:1 → C(A, A) in Set

id_A∈C(A, A) だったので、ポインティング写像を考えることが出来ます。

最後に次の図は、三段論法（「三段論法とは何か？」参照）と呼ばれるリーズニングを表しています。

  A → B   B → C
 --------------- 
    A → C

次の解釈が自然でしょう。

  C(A, B)   C(B, C)
 ------------------- Comp_A,B,C in MultiSet
    C(A, C)

横書きすれば：

Comp_A,B,C:(C(A, B), C(B, C)) → C(A, C) in MultiSet

Set内で解釈すれば：

Comp_A,B,C:C(A, B)×C(B, C) → C(A, C) in Set

*** TBD ***

*1:縦書き図が推奨できる描画法だとまったく思っていません。が、実際に使われているし、今後も使われ続けるので、縦書き図の必要性は確実にあります。

*2:現実のプログラミング言語で、多値関数があまり使われてないことに関しては「なぜ、多値関数は人気がないのだろう」という記事があります。

*3:僕は、「とても簡潔だがサッパリ理解できない」よりは「とても煩雑だが頑張れば理解できる」ほうを選びます。

*4:シーケント計算は、極端な省略記法から出発します。ただし、背後の意味を考えると極端な省略でも、「無意味な形式的体系としては何ら問題ではない」という主張に反論は出来ません。

*5:上から下への変化が、記号'∧'を導入〈introduction〉したように見えるので、∧-intro という名前にします。