モノイド閉圏の事例： ブロック式

その他 特例

具体的な結果を示すには具体的な計算が必要で、往々にして計算はドブ板作業になります。ドブ板作業を少しでも軽減するために、ツール（計算デバイス）を整備・改善します。

内容：

ブロック式構文

視認性・可読性・理解容易性を改善するために、ラムダ記法にブロック式という構文を導入する。とはいえ、囲み記号として角括弧 '[', ']' を新規に追加するだけ。

角括弧は、λ0, λ1, λ01 で始まるラムダ式と、ALSO, OR 接続詞の組み合わせを囲むために使う。角括弧で囲まれた部分をブロック式〈block expression〉と呼ぶ。ブロック式は次の3種類に限定する。

  1. グラフ射を表現する： [λ0... ALSO λ1...]
  2. ボックス積からのグラフ射を表現する： [λ0... ALSO λ1... OR λ1...]
  3. 変形を表現する： [λ01...]

その他の用途では、今までどうり丸括弧を使う。角括弧は、必ずグラフ射か変形を表す（ようにする）。

ブロック式に角括弧を使うので、hom(A, B) を [A, B] と書く記法は採用できない。

値の型の表記

  • 式の値の型は、「∈ B」のような書き方で示すが、このとき「∈1B」や「∈B(1)」とは書かない。頂点・辺の区別（要素の次元）は文脈から読み取る。

文脈から読み取るのが負担になることもあるので、規則を変更する。

  1. 式の値が頂点であるときは、「∈B(0)」と書く。
  2. 式の値が辺であるときは、「∈B(1)」と書く。
  3. 単に「∈B」と書くことも許す。そのときは、（読む側は）「∈B(0)」か「∈B(1)」かを文脈から読み取る。

特に、値をホムグラフに取るようなグラフ射（高階グラフ射）のときは次の書き方を許す。

  1. hom(B, C)(0) = Hom(B, C) なので、「∈hom(B, C)(0)」の代わりに「∈Hom(B, C)」と書いてよい。
  2. B (0→1) C の形の変形の全体を Defm(B, C) と書くことにする。
  3. hom(B, C)(1) ⊆ Defm(B, C) なので、「∈hom(B, C)(1)」の代わりに「∈Defm(B, C)」と書いてよい。

高階グラフ射の表現

ホムグラフに値を取るグラフ射を高階グラフ射〈higher-order graph morphism〉と呼ぶ。F:A→hom(B, C) が高階グラフ射のとき、Fをラムダ式で表現する。

まず、単純なグラフ射ブロックを使って：

F = [
 λ0a∈A.( F(0)(a) ∈hom(B, C)(0))
 ALSO
 λ1a→a'∈A.( F(1)(a→a') ∈hom(B, C)(1))
]

値の型を具体的に書いて：

F = [
 λ0a∈A.( F(0)(a) ∈Hom(B, C))
 ALSO
 λ1a→a'∈A.( F(1)(a→a') ∈Defm(B, C))
]

F(0)(a) と F(1)(a→a') をブロック式で書けば：

F(0)(a) = [
 λ0b∈B.( F(0)(a)(b) ∈C)
    /* ∈C(0) とは書かなかった */
 ALSO
 λ1b→b'∈B.( F(0)(a)(b→b') ∈C)
    /* ∈C(1) とは書かなかった */
]

F(1)(a→a') = [
  λ01b∈B.( F(1)(a→a')(b) ∈C)
    /* ∈C(1) とは書かなかった */
]

これらを先の式に代入して：

F = [
 λ0a∈A.(
   [
     λ0b∈B.( F(0)(a)(b) ∈C)
     ALSO
     λ1b→b'∈B.( F(0)(a)(b→b') ∈C)
   ]  ∈Hom(B, C))
 ALSO
 λ1a→a'∈A.(
   [
     λ01b∈B.( F(1)(a→a')(b) ∈C)
   ] ∈Defm(B, C))
]

記号の乱用で、F(0), F(1) の下付き添字を省略すれば、

F = [
 λ0a∈A.(
   [
     λ0b∈B.( F(a)(b) ∈C)
     ALSO
     λ1b→b'∈B.( F(a)(b→b') ∈C)
   ]  ∈Hom(B, C))
 ALSO
 λ1a→a'∈A.(
   [
     λ01b∈B.( F(a→a')(b) ∈C)
   ] ∈Defm(B, C))
]

事例として、f:A□B→C をカリー化した高階グラフ射 F:A→hom(B, C) を新しい記法で記述してみる。

F:A→hom(B, C) :=
[
 λ0a∈A.(
   [
     λ0b∈B.( f(a, b) ∈C)
     ALSO
     λ1b→b'∈B.( f(a, b→b') ∈C)
   ]  ∈Hom(B, C)
 )
 ALSO
 λ1a→a'∈A.(
   [
     λ01b∈B.( f(a→a', b) ∈C)
   ] ∈Defm(B, C)
 )
]

F = Φ(f) なのだから、Φ（ΦA,B,Cを略記）自体は次のように書ける。

Φ:Hom(A□B, C)→Hom(A, hom(B, C)) := λf∈Hom(A□B, C).(
  [
   λ0a∈A.(
     [
       λ0b∈B.( f(a, b) ∈C)
       ALSO
       λ1b→b'∈B.( f(a, b→b') ∈C)
     ]  ∈Hom(B, C)
   )
   ALSO
   λ1a→a'∈A.(
     [
       λ01b∈B.( f(a→a', b) ∈C)
     ] ∈Defm(B, C))
  ] ∈Hom(A, hom(B, C))
)