このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

［参照用 記事］

はじめての圏論 第6歩：有限変換キューと半圏

雑記／備忘

第5歩で変換キューを紹介しましたが、そのとき次の仮定を置きました。

  1. バッファ容量に制限（上限）はない。
  2. 変換は、プログラムの内部状態に依存しないで行う。

2番目の仮定を取り除いて「状態に依存した複雑な変換」を許しても、ハナシが面倒になるだけで、状況が本質的に変化することはありません。しかし、バッファ容量を有限（上限がある）にしてしまうと、圏論がうまく使えなくなります。

有限変換キュー（バッファ容量が有限な変換キュー）達が圏にはならないこと、そして、そこから圏論的な状況を回復する手順は、ソフトウェア的にも代数的にもとても面白いので紹介しておきます。ちょっと特論的な話題なので、圏の一般論のほうに興味がある方は、この第6歩をスキップしてもかまいません。

内容：

有限変換キュー

バッファ容量が有限で固定長の変換キューを考えます。バッファの容量（定数値）はgetSize()で得られるとしましょう。そのインターフェースは次のよう。

public interface BoundedTransQ<X, Y> {
  boolean isEmpty(); // キューがカラッポかどうか
  boolean isFull(); // キューがイッパイかどうか
  int getSize(); // バッファ容量（データ項目が何個貯められるか）
  void post(X item); // キューにデータを入れる
  Y get(); // キューからデータを取り出す
}

バッファがイッパイのときpostすると、データ・ロストが起きます。好ましくないけど、いたしかたない。

有限変換キューf:X→Yとg:Y→Zの結合は、次のようなクラスのインスタンスで実現されるでしょう（コードは雰囲気です）。

class FG<X, Y, Z> implements BoundedTransQ<X, Z> {
  F<X, Y> f;
  G<Y, Z> g;

  public FG() {
    f = new F<X, Y>();
    g = new G<Y, Z>();
  }
   
  public boolean isEmpty() {
    return f.isEmpty() &amp;&amp; g.isEmpty();
  }
  public boolean isFull() {
    return f.isFull() &amp;&amp; g.isFull();
  }
  public int getSize() {
    return f.getSize() + g.getSize();
  }
  public void post(X x) {
    if (f.isFull()) {
      if (g.isFull()) {
        return; // データはロストする
      }
      g.post(f.get());
    }
    f.post(x);
  }
  public Z get() {
    if (g.isEmpty()) {
      if (f.isEmpty()) {
        return null;
      }
      g.post(f.get());
    }
    return g.get();
  }
}

バッファ容量が0だとキューとして機能しない（すべてのデータをロストする）ので、getSize() >= 1 という制限（不変表明ですね）を付けます。*1

有限変換キュー達は圏になるか

有限変換キューの場合も、入出力が型付けされていることから、cod(f) = dom(g) のときに限り f;g が定義されます。振る舞い同値（初期状態からの動作が観測的に識別不可能）なときにイコールだとして、(f;g);h = f;(g;h) も成立します。有限変換キューの結合は“圏の結合”のように思えます。

では、型Xに対する恒等射idXを探しましょう。size(f;g) = size(f) + size(g) （f.getSize() を、size(f)とも書く）が成立しているので、idXのサイズに関して：

  • size(idX;f) = size(idX) + size(f)
  • idX;f = f だから、size(idX;f) = size(f)
  • これらの右辺を比較すれば、size(idX) + size(f) = size(f)

以上から、size(idX) = 0 でなくてはなりませんが、サイズ（バッファ容量）が0の変換キューは存在しないので、結局、idXは存在しないのです。

圏から恒等射を除いたら半圏になる

圏の定義から恒等射idをスッパリと除いてしまうと、それは半圏（semicategory）を定義します。S = (|S|, S, dom, cod, ;) が半圏であるとは、結合演算 f;g が cod(f) = dom(g) のときにだけ定義され、それが結合法則を満たすことです。idは最初から存在しないので、idに関する条件は一切ありません。

前節で述べたことは、有限変換キュー達は圏にはならないが半圏にはなっていることを示しています。半圏は、恒等射（単位のようなもの）がないぶんだけ不自由になりますが、圏と似た議論がある程度は通用します。

みーんな一緒にしてみる

第5歩で導入した圏TransQは、無限（無制限）バッファを持つ変換キューからなるのでした。ちなみに、必要に応じてメモリを確保すれば、無限バッファをエミュレートできるので、無限変換キューはいたって現実的なものです（最近では固定長バッファのほうが少ないでしょう）。

無限変換キュー達は圏をなし、有限変換キュー達は半圏にしかならないのですが、ここで、無限変換キューと有限変換キューを全部寄せ集めてみます。インターフェースは、BoundedTransQと同じでいいとします（でも名前は変えたほうがいいね）。ただし、無限変換キューでは：

  1. isFull()は、常にfalseを返す。
  2. getSize()は、定数UNLIMITED（例えば-1を使う）を返す。

UNLIMITEDの意味は∞（無限大）なので、サイズの値の範囲は{1, 2, 3, ..., ∞}となります。サイズの足し算は、n + ∞ = ∞ + n = ∞、∞ + ∞ = ∞ として計算します。

こうしてできた、すべての無限／有限変換キューの全体をMixedTransQとしましょう。dom, cod, ;（結合）は、MixedTransQの上でもうまく定義できます。問題は恒等射です。型Xのデータを変換しない単なる無限キューqXは、TransQの恒等射だった（だから、idXと書いていた）のですが、MixedTransQでは恒等射になるでしょうか？ …… ダメです。f:X→Yが有限変換キューのとき、qX;f は無限変換キューになります。有限変換キューと無限変換キューは同じ（振る舞い同値な）プログラムとみなせないので、qX;f = f は成立しません。

結論を言えば、MixedTransQも圏にはならないのです（半圏にはなってますが）。しかし、何も変換しない無限キューqXは注目すべき存在で、恒等射ではありませんが、恒等射に似た性質を持ち、細工をして恒等射にすることもできます。このことは、簡単な代数的な議論でわかります（次節以降）。

疑似恒等射を持つ半圏

少しだけ一般的／代数的議論をします。S = (|S|, dom, cod, ;)が半圏だとして、さらに、x∈|S|ごとにqidx:x→x という射が割り当てられているとします。qidを疑似恒等射（quasi-identity）と呼びましょう。疑似恒等射は恒等射である必要はありませんが次は満たすとします。

  • qidx;qidx = qidx -- ベキ等性

何もしない無限キューは疑似恒等射の条件を満たしています。

半圏Sが疑似恒等射を備えているとき、疑似恒等射を持つ半圏（semicategory with quasi-identities）と呼びましょう。MixedTransQに何も変換しない無限キューqX達を一緒に考えると、これは“疑似恒等射を持つ半圏”になっています。

半圏のなかから圏を探し出す

MixedTransQは“疑似恒等射を持つ半圏”ですが、そのなかに圏TransQが埋め込まれていると考えていいですよね。size(f) = ∞ であるような変換キュー、つまり無限変換キューは圏TransQの射になっています。sizeを使わずに無限変換キューを選び出せないでしょうか？ -- 無限変換キューを特徴付ける代数的条件は意外と簡単です。f:X→Y がMixedTransQの射（有限または無限の変換キュー）だとして：

  1. qX;f = f
  2. f;qY = f

一番目の等式が成立しているとして、size(qX;f) = size(qX) + size(f) = ∞ + size(f) = ∞、よってsize(f) = ∞ となります。2番目が成立していても同じこと。qXのサイズが∞であることがミソです。

等式 qX;f = f をソフトウェア的に解釈すると、fの内部に無限の入力バッファがあることです。qXを入力側に繋いでも振る舞いが変わらないということは、fがもともと内部に無限入力バッファを備えていることを意味しますから。

純粋に等式だけ（代数的条件）として考えると、qX;f = f と f;qY = f は独立で、片一方からもう一方を導けないので、2つの等式をともに満たす射をフルバッファ付き射（fully buffered morphism）と呼ぶことにしましょう。

「フルバッファ付き」は、いかにもソフトウェア的な形容詞です*2が、実際には“疑似恒等射を持つ半圏”における純粋に代数的な条件です。S = (|S|, S, cod, dom, qid, ;)が“疑似恒等射を持つ半圏”であるとき、圏C = (|C|, C, cod, dom, id, ;)を次のようにして作れます。*3

  1. Cの対象の集合は、Sの対象の集合と同じとする。|C| = |S|。
  2. Cの射の集合は、半圏Sのフルバッファ付き射の全体とする。C⊆S。
  3. cod, dom, ;はSのものをそのまま使う。
  4. CのidはSのqidとする。

次のことを、純代数的に（等式だけに基づいて）示してみてください（簡単な練習問題）。

  1. fとgがフルバッファ付きなら、f;g もフルバッファ付きになる。
  2. qidXはフルバッファ付きである。
  3. フルバッファ付きの射に関しては、qidX達が恒等射になっている。つまり、単位法則が成り立つ。

任意の射のフルバッファ化（パイプの秘密）

Sが“疑似恒等射を持つ半圏”であるとき、フルバッファ付き射だけを選び出すと圏が作れます。それだけではなくて、Sの射をフルバッファ化できます。f:X→Yに対して、f' = qidX;f;qidY とすると、f'はフルバッファ付きになります。なぜなら：

   qidX;f'  //↓f'の定義より
 = qidX;(qidX;f;qidY) //↓結合法則
 = (qidX;qidX);f;qidY //↓ベキ等性
 = qidX;f;qidY //↓f'の定義より
 = f'

 f';qidY = f' も同様。

なお、

   f';g'
 = (qidX;f;qidY);(qidY;g;qidZ)
 = qidX;f;(qidY;qidY);g;qidZ
 = qidX;f;qidY;g;qidZ

なので、fとgの間にはさむ無限バッファqidYは1個に節約できます。

Unix流のパイプラインがうまく動くひとつの理由は、OS／シェルがバッファを持たないフィルターもフルバッファ化してから結合するからです。

*1:サイズが0のキューを認めても実害はありません。データを捨てるデバイスとして使えます。

*2:もっと適切な用語が必要ですね。

*3:Cがまったくつまらない圏になってしまうかもしれません。