並列実行の定式化

その他
集合演算（主に直和）

集合演算は：

  1. 直積： A×B
  2. 直和： A + B

直和は、直感的には「AとBが交わらないように置いたもの」だが、集合論内で扱う場合は次のように定義する。

  • A + B := ({1}×A)∪({2}×B)
    = {(n, x)∈{1, 2}×(A∪B) | (n = 1 ∧ x∈A) ∨ (n = 2 ∧ x∈B)}

ここで出てきた 1 または 2 のことを弁別子〈discriminator〉または弁別タグと呼ぶ。もちろん、弁別タグは 1, 2 以外でも区別さえできれば何でもよい。(n, x) を、x@n（x@1 または x@2）と書くと便利である。

直和の要素は、パターンマッチングcase文で処理する。

case x ∈ A＋B of
  a@1, a∈A ⇒ ...,
  b@2, b∈B ⇒ ...
end

意味を日本語で書けば：

A + B の要素 x を場合分けする
  x が a@1 の形で a∈A のとき ...,
  x が b@2 の形で b∈B のとき ...
場合分け終わり

直和は論理の"or"に対応するので、関数定義を次のように簡略に書いてもよい。

f(a@1) = ... or f(b@2) = ...
基本関数
  1. ΔA : A→A×A in Total
    ΔA(a) := (a, a) ∈A×A
  2. ∇A : A+A→A in Total
    ∇(a@1) := a ∈A or ∇(a@2) := a ∈A
  3. δA : A→A+A in ND
    δA(a) := {a@1, a@2} ⊆A+A
  4. γA : A×A→A in ND
    γA(a, b) := {a, b} ⊆A
  5. EA : A×A→A in Partial
    EA(a, b) := if (a = b) then a else ⊥
  6. π1A,B : A×B→A in Total
    π1A,B(a, b) := a ∈A
  7. π2A,B : A×B→B in Total
    π2A,B(a, b) := b ∈B
  8. ι1A,B : A→A+B in Total
    ι1A,B(a) := a@1 ∈A+B
  9. ι2A,B : B→A+B in Total
    ι2A,B(b) := b@2 ∈A+B
  10. ⊥A,B : A→B in Partial
    ⊥A,B(a) = ⊥
基本コンビネータ

プログラムを関数〈写像〉として扱う場合の、各種並列実行の定義：

  1. For f:A→X, g:B→Y in Total,
    f×g : A×B → X×Y
    (f×g)(a, b) := (f(a), g(b))
  2. For f:A→X, g:B→Y in Total,
    f\oplusg : A+B → X+Y
    (f\oplusg)(x) := case x ∈A+B of a@1, a∈A ⇒ f(a)@1, b@2, b∈B ⇒ g(b)@2 end
  3. For f:A→X, g:A→Y in Total,
    <f, g> : A → X×Y
    <f, g>(a) := (f(a), g(a))
  4. For f:A→X, g:B→X in Total,
    [f, g] : A+B → X
    [f, g](x) := case x ∈A+B of a@1, a∈A ⇒ f(a), b@2, b∈B ⇒ g(b) end
  5. For f:A→X, g:A→X in Partial,
    f & g : A → X
    (f & g)(a) := if (f(a) = g(a)) then f(a) else ⊥

順次実行が、fの実行終了後にgが開始するのに対して、上記の並列実行は、f, g が同時に実行開始してもよい。

基本関数や基本コンビネータの定義を、TotalからPartialへ、PartialからNDへと拡張するのは比較的に容易だが、圏論的な性質はガラッと変わってしまうことがあるので十分な注意が必要である。例えば、集合／関数の直和は、NDでは圏論的な直積（かつ直和）になる。

問題

次の等式を証明せよ。集合添字は適切に補う（それも問題の一部）。証明は、定義に基づき集合論を使って行うこと。当然ながら、プログラミングの直感（当てにならない）を使ってはいけない。

  1. <f, g>;π1 = f
  2. <f, g>;π2 = g
  3. <f;π1, f;π2> = f
  4. ι1;[f, g] = f
  5. ι2;[f, g] = g
  6. [ι1;f, ι2;f] = f
  7. <f, g> = Δ;(f×g)
  8. [f, g] = (f\oplusg);∇
  9. f & g := Δ;(f×g);E
  10. δ;(f\oplusg);∇ = Δ;(f×g);γ

δ;(f\oplusg);∇ または Δ;(f×g);γ で定義される関数を f + g と書く。

  • For f:A→X, g:A→X,
    f + g : A → X

次の等式を証明せよ。集合添字は適切に補う。

  1. γ = π1 + π2
  2. (f + g) + h = f + (g + h)
  3. f + g = g + f
  4. f + f = f
  5. f + ⊥ = f
  6. ⊥ + f = f
  7. (f + g);h = f;h + g;h
  8. f;(g + h) = f;g + f;h

f + g の直感的説明が次のどれでもよいことを確認せよ。

  1. 最初にコイントス。どっちのプログラムを実行するか決めて1つだけ実行。
  2. 2つを同時に実行する。どちらの結果を採用するかコイントス。
  3. 2つを同時に実行する。謎の原因で速度が変わる状況（雑音による遅延）で、早く終わったほうを採用。
並列結合の名称

並列結合は複数あるが、それらを明確に区別する習慣がなかった（酷い）ので、広く合意された名称はない。圏論からの名称、ローカルな名称なら次のとおり。用語のバリエーションの書き方は「用語のバリエーション記述のための正規表現」を見よ。

  1. f×g ： （関数の）直積
  2. f\oplusg ： （関数の）直和
  3. <f, g> ： （関数の）{デカルト}?{ペアリング | ペア }
  4. [f, g] ： （関数の）{デカルト}?{コペアリング | コペア }
  5. f & g ： （関数の）タンデム結合
  6. f + g ： （関数の）選択的並列結合

例えば、概念的な f×g を、実際のハードウェア+OSの上で、時分割方式でやるか、マルチコア機能でやるか、マルチCPU構成でやるか、などは全然別な話である。具体的な実行方式の定式化（のヒント）は次を参照。

コンビネータ・プログラミングをする場合は、並列結合コンビネータに（演算子だけではなく）名前が必要なので、命名しておく。タンデム結合はほとんど使わないので無視する。

並列結合 コンビネータ名称
直積 Prod(f, g)
直和 Sum(f, g)
ペア Pair(f, g)
コペア Copair(f, g)
選択的並列結合 Choice(f, g)

コンビネータのプロファイル：

  Total(A, X)   Total(B, Y)
  -------------------------- Prod
     Total(A×B, X×Y)

  Total(A, X)   Total(B, Y)
  -------------------------- Sum
     Total(A+B, X+Y)

  Total(A, X)   Total(A, Y)
  -------------------------- Pair
     Total(A, X×Y)

  Total(A, X)   Total(B, X)
  -------------------------- Copair
     Total(A+B, X)

  ND(A, X)   ND(A, X)
  -------------------------- Choice
     ND(A, X)