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

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

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

［参照用 記事］

はじめての圏論 その第5歩：変換キューの圏

雑記／備忘

しりとりの圏HShiriは単なる“お遊び”だし、行列の圏Matは所詮（高校の）“数学”だし、やっぱり現実離れしているじゃん -- と思ってます？ そうでもないのよね。多くの物理現象／計算現象、電気回路のような工学的な対象までも圏で定式化できるんですよ。例えば、量子テレポーテーション／エンタングルメントの、コンパクト閉圏を使った計算（「幼稚園児のための量子力学とその周辺」参照）はその良い例でしょう（つっても、僕は物理がサッパリわからんのだけどさ）。

それでまー、第三の例として今回はソフトウェア的なネタを出そう、と。なにがいいかなー？ 僕が大好きなパイプ＆フィルター（「パイプ＆フィルターの思い出」参照）の圏論的な定式化（の単純化した一例）にします。FIFO（First In/First Out）バッファを内蔵したフィルター達からなる圏を紹介します。

内容：

変換キュー（バッファ付きフィルター）

バッファとはデータを溜め込む装置ですが、先に入れたデータが先に取り出されるバッファはFIFOバッファ、またはキュー（queue）と呼びます（「待ち行列」という訳語もあります）。キューのインターフェースは次のような感じでしょう。

public interface Queue<T> {
  boolean isEmpty(); // キューがカラッポかどうか
  void post(T item); // キューにデータを入れる
  T get(); // キューからデータを取り出す
}

Tはデータ項目の型です。例外を使うと多少ややこしくなるので、データが取り出せないときはnullを返すことにします。そして、nullをポストしても何もおきません。

単なるキューはデータを一時的に貯めるだけですが、入れたデータを取り出すと変換されるようなキューを考えましょう。例えば、小文字を大文字に変換するtoupperのような変換です。変換機能を備えたキューを変換キューと呼ぶことにします。変換キューのインターフェースは次のよう。

public interface TransQ<X, Y> {
  boolean isEmpty(); // キューがカラッポかどうか
  void post(X item); // キューにデータを入れる
  Y get(); // キューからデータを取り出す
}

Xが入力データの型、Yが出力データの型です。キューのサイズ（容量）は無制限だ（いくらでもデータを貯められる）とします。ハナシを単純化するために、変換はバッファの蓄積状態／その他の状態には無関係で、データ項目だけを見て行うとします。

変換キューの結合

fが、“型Xのデータ”を“型Yのデータ”に変換する変換キューであるとき、f:X→Yと書くことにします。こうして矢印記法で書くと、なんだかfが圏の射のような気分がしますね（後で実際に射にします）。例えば、toupper:Character→Character、kansuji:Integer→String。toupperは小文字→大文字変換、kansujiは整数125を文字列"百二十五"に直すような変換のつもり。

さて、f:X→Y, g:Y→Z であるとき、fとgの結合f;gを定義します。fがクラスFのインスタンス、gがクラスGのインスタンスだとして、例えば次のようなコードを書けばいいでしょう（あくまで雰囲気に過ぎないけど）。

class FG<X, Y, Z> implements TransQ<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 void post(X x) {
    f.post(x);
  }
  public Z get() {
    if (g.isEmpty()) {
      if (f.isEmpty()) {
	return null;
      }
      g.post(f.get());
    }
    return g.get();
  }
}

これだと、fのバッファ領域ばかり使って不公平ですが、まー、いいとしましょう（fのバッファの半分をgに移すとか、やりようはあります）。また、この方法ではFGという新しいクラスを作りましたが、実行時にインスタンスであるfとgを直接繋ぐようなフレームワークも作れますね。

プログラムの同値性

※この節は、雰囲気がわかればそれでいいので読み流してもいい。

さて、変換キューの結合が“圏の結合”の条件を満たすことを示したいのですが、圏の条件はすべて等式で記述されています。等式にはイコール記号が出てきますね。つまり、「等しさ」を判定するわけ。となると、2つの変換キュー（として動作するプログラム）が「等しい」とはどういうことかを定義する必要があります。

プログラムの等しさ（同値性）の定義はけっこう難しい問題です。「ソースコードの字面が同じこと」なんて定義はうまくないので、利用者から見て（ブラックボックスとして）区別がつかないなら同じとみなすのがいいでしょう。この同値性は「振る舞い同値」（behavioral equivalence）とか呼ばれます。

振る舞い同値の具体的な定式化として、2つの状態空間のあいだの対応関係を明白に設定して、「双模倣性」（bisimilarity）を使う方法と、初期状態からの行動記録が同じであることを根拠にする「観測的識別不可能性」（observationally indistinguishability）を使う方法があります。ここでは、観測的に識別不可能（すぐ下に定義）なときに、同じ変換キューとみなすことにします。

観測的に識別不可能であること*1を、ホーア式を使って構文的に定義しましょう（ホーア式に関しては「極小プログラミング言語とホーア論理」とか、https://m-hiyama.hatenablog.com/search?q=ホーア式 から適当に拾って見てください）。まず、単純文を次のように定めます。

  • post(x);は単純文。postの引数はリテラルか変数。
  • yをY型の変数としてy = get();（代入文）は単純文。

いくつかの変数x1, x2, ... のあいだの等式（例えば、x1 == x2 とか x3.equals(x4)とか）、isEmpty()（値はブール値）から論理記号により組み立てられた論理式をP, Qなどとして：

  • ホーア式は、P {単純文の並び} Q の形。

論理式P, Qにも単純文にも変数が登場しますが、次の条件を付けておきます。

  • 変数の値は前もって初期化しておいてもいいし、代入文で値を入れてもいい。
  • ただし、1つの変数は1つの代入文でしか使わない。（代入文による値の書き換えは行わない。）

以下で使うホーア式は、P（事前条件）が (isEmpty())のものだけにします。別な言い方をすると、初期状態からの動作だけを問題にします。

2つの変換キュー（として動作するプログラム）が同じ（観測的に識別不可能）とは、

  • 事前条件が(isEmpty())であるどんなホーア式に対しても、2つの変換キューが同じ値（真偽）を取ること

です。詳細はともかくとして、「どんなテストをしても、振る舞いの違いが見つからない」と考えればいいでしょう。

圏TransQ

プログラムの同値性が定義できた（ってことにする）ので、圏TransQを構成できます。まず、圏の対象集合ですが、これはデータ型の集合として適当に決めます。例えば、|TransQ| = {Character, Integer, String, Date}とかでもいいです（ほんとにテキトーでいい）。X, Y∈|TransQ|、つまりXとYが許されたデータ型だとして、射f:X→Yとは、“型Xのデータ”を“型Yのデータ”に変換する変換キューです。ただし、同じ振る舞いをするプログラムはイコールと見なします。

  • dom(f) = 変換キューfの入力データ型
  • cod(f) = 変換キューfの出力データ型

型Xに対するidXは無変換キュー（貯めるだけのバッファ）として定義します。2つの変換キューの結合は既に定義しました。cod(f) = dom(g)のときだけf;gが定義できるということは、キューの入出力が強く型付けされていることを意味しますね。dom(f;g) = dom(f)、cod(f;g) = cod(g)、dom(idX) = com(idX) = X は明らか。

さて、すべての変換キュー達が圏となるためには、次が要求されます：

  • (f;g);h = f;(g;h)
  • f:X→Y として、idX;f = f;idY = f

この等式を厳密に示すのはけっこう面倒ですが、直感的には納得がいくだろうと思います。

もう少し補足

今回の変換キューは、データ項目ごとに変換するだけなので、バッファリングを有効利用してません。例えば、重複するデータ項目を削除するようなこと（uniq）は想定してません。しかし、状態依存の複雑な処理をいれても、変換キュー達はやはり圏を構成します。また、この例では、フィルターどおしが1本の非同期データ通信チャネルにより繋がっているイメージですが、複数チャネルで繋ぐような構成を圏論で定式化することもできます。並列処理を導入することもできます。複数チャネル／並列処理を導入すると、ずっと難しくなるのは確かですけど（「高次元のパイピング」参照）。

*1:システムの初期状態どおしが観測的に識別不可能、というのが正確な表現です。