モノイド閉圏の事例： データブロック、適用、代入計算

その他 特例

表題の記法・概念を説明します。まだ、計算の準備。

内容：

写像ブロック

ブロック記法を導入しましたが、一般的に f:A→X, g:B→Y, h:C→Y in Set に関して [f ALSO g] は写像の直和になり、[g OR h] は写像のコタプルになります。

ここでの記法 集合圏での標準的記法
[f ALSO g] f + g : A+B→X+Y
[g OR h] [g, h] : B+C→Y
[f ALSO g OR h] f + [g, h] : A+B+C→X+Y

ブロック記法に関する計算法則は、（必要なら）写像の直和／写像のコタプルの性質から導くことができます。

既に使っているブロック記法は写像〈関数〉を表現しているので、写像ブロック〈関数ブロック〉と呼ぶことにします。

データブロック

関数ブロックと類似の構文のデータ表現も導入します。Aを単純グラフとして、a∈A(0), i∈A(1) だとして、{a ALSO i} をAのデータブロックと呼びます。

A□B をボックス積グラフとして、(a, b)∈(A□B)(0), (i, b)∈A(1)×B(0) (a, j)∈A(0)×B(1) だとして、{(a, b) ALSO (i, b) OR (a, j)} をA□Bのデータブロックと呼びます。

データブロックの実体（セマンティクス）は：

  • {a ALSO i} : {1, 2}→A(0)+A(1)
  • {(a, b) ALSO (i, b) OR (a, j)} : {1, 2, 3}→(A□B)(0)+(A(1)×B(0))+(A(0)×B(1))

写像として意味づけできるので、（必要なら）この定義からデータブロックの性質を導くことができます。

データブロックのセマンティクスはタプルと同じですが、構文的にはタプルとは違います。例えば、{a ALSO a→a'} に出現する2つのaは同じ頂点とは解釈しません。ALSOの左右で、変数のスコープは独立しています。

適用

写像〈関数〉とデータの適用〈評価〉を、写像ブロックとデータブロックに対しても定義します。

  • [f(0) ALSO f(1)]({a ALSO i}) = {f(0)(a) ALSO f(1)(i)}
  • [f(0) ALSO f(1)1 OR f(1)2]({(a, b) ALSO (i, b) OR (a, j)}) = {f(0)(a, b) ALSO f(1)1(i, b) OR f(1)2(a, j)}

({...}) が煩雑なので、丸括弧は省略可能としましょう。

  • [f(0) ALSO f(1)]{a ALSO i} = {f(0)(a) ALSO f(1)(i)}
  • [f(0) ALSO f(1)1 OR f(1)2]{(a, b) ALSO (i, b) OR (a, j)} = {f(0)(a, b) ALSO f(1)1(i, b) OR f(1)2(a, j)}

なお、図式順の適用は次のようにドットで書きます。

  • {a ALSO i}.[f(0) ALSO f(1)] = {a.f(0) ALSO i.f(1)}
  • {(a, b) ALSO (i, b) OR (a, j)}.[f(0) ALSO f(1)1 OR f(1)2] = {(a, b).f(0) ALSO (i, b).f(1)1 OR (a, j).f(1)2}

適用とイータ同値

ラムダ式では、一般に次（イータ同値）が成立します。

  • f = λx∈X.(f(x))

fが写像ブロックとして書けるときも同様なので：

f:A→B =
[f(0) ALSO f(1)]:A→B = 
λ{a ALSO i}∈A.(
   [f(0) ALSO f(1)]{a ALSO i} ∈B
)


f:A□B→C =
[f(0) ALSO f(1)1 OR f(1)2]:A□B→C =
λ{(a, b) ALSO (i, b) OR (a, j)}∈A□B.(
 [
   f(0)
   ALSO
   f(1)1
   OR
   f(1)2
 ]{(a, b) ALSO (i, b) OR (a, j)}
 ∈ C)

また、次も成立します。

λ{a ALSO i}∈A.(
   [f(0) ALSO f(1)]{a ALSO i} ∈B
) =
λ{a ALSO i}∈A.(
   {f(0)(a) ALSO f(1)(i)} ∈B
) = 
[
  λ0a∈A.( f(0)(a) ∈B)
  ALSO
  λ1i∈A.( f(1)(i) ∈B)
]


λ{(a, b) ALSO (i, b) OR (a, j)}∈A□B.(
 [
   f(0)
   ALSO
   f(1)1
   OR
   f(1)2
 ]{(a, b) ALSO (i, b) OR (a, j)}
 ∈ C)
=
λ{(a, b) ALSO (i, b) OR (a, j)}∈A□B.(
 {
   f(0)(a, b)
   ALSO
   f(1)1(i, b)
   OR
   f(1)2(a, j)
 } ∈ C)
=
[
   λ(0)(a, b)∈A□B.( f(0)(a, b) ∈C)
   ALSO
   λ(1)(i, b)∈A□B.( f(1)1(i, b) ∈C)
   OR
   λ(1)(a, j)∈A□B.( f(1)2(a, j)  ∈C)
]

代入計算

グラフ射の結合 f;g をラムダ記法で計算するとき、代入計算が必要になります。代入〈置換〉の表現にも角括弧や波括弧が使われますが、既に使ってしまったので、別な記号を割り当てます。

  • /(式1 / 変数=式2)/

これで、「式1のなかに登場する変数を式2で置換することを示します。

一般に、代入計算は次のように使います。

  x.(f;g)
 = (f;g)(x)
 = ( (λy∈Y.g(y)) \circ f )(x)
 = /( g(y) / y = f(x) )/