檜山正幸のキマイラ飼育記 このページをアンテナに追加 RSSフィード

キマイラ・サイトは http://www.chimaira.org/です。
トラックバック/コメントは日付を気にせずにどうぞ。
連絡は hiyama{at}chimaira{dot}org へ。
蒸し返し歓迎!
ところで、アーカイブってけっこう便利ですよ。タクソノミーも作成中。今は疲れるので作っていません。

2016-09-16 (金)

関数型プログラミングとオブジェクト指向について、何か書く、かも

| 15:37 | 関数型プログラミングとオブジェクト指向について、何か書く、かもを含むブックマーク

「関数型プログラミングはオブジェクト指向の正当な後継」なの?」を書いていて次のようなことを思いました: テクノロジーに関する思索を語るのは推奨されるべき事だと思いますが、ベーシックな知識に裏打ちされてないと、解釈困難で意味不明になりがちです。せっかくの経験や思いがうまく伝わらないことになります。

知識は大切だな、とは思っているので、ちょっと気になりそうなトピックに関して、ベーシックな知識の入り口を解説する記事を書いてきました。

公開年を見るとわかるように、いずれも10年近く前です。一度書いてしまうと、同じことを繰り返し書く気にはなれないので、このテの入門記事を書くことはなくなってしまいました。

表題の「関数型プログラミングオブジェクト指向」とかは、今でも興味を持つ人は多いのでしょうが、(僕自身にとっての)新しい切り口がなかなか見つからない。「なんかないかな?」と見渡してみると、型クラスあたりかな、と。

型クラスは重要で面白い話題だと思います。ただね、例によって概念も用語法も混乱していて、それを整理するのがすごく負担。そもそも型クラスって何? の定義を確定するのが容易じゃない。

元祖・型クラスみたいなHaskellの型クラスは、およそ指標(signature)のことです。Standard MLでは素直にsignatureと呼んでます。しかし、Standard MLのsignatureは(structure, functorと共に)モジュール機構を意図しているので、多相な型システムとは微妙に違う気がします。

CoqやIsabelleの型クラスとなると、指標だけではなくて公理を書けます。よって、型クラスは形式セオリー(または形式仕様)のことになります。公理(条件、制約、表明)を書けない型クラスというのは、人間だけが知っている暗黙の思いに支えられている点で不十分で脆弱なものです。

例えば、Haskell型クラスの定番の例であるEqクラス:

class Eq a where
  (==) :: a -> a -> Bool

こんなもんで等号の性質を規定したことには全然なりません。Coq型クラスなら、

Class Setoid A := {
  equiv : relation A ;
  setoid_equiv :> Equivalence equiv
}.

Equivalenceは、反射律(Reflexive)、対称律(Symmetric)、推移律(Transitive)をまとめた記述で、等号(同値関係を表す記号)として満たすべき制約まで記述してます。これなら、二項関係equivが等号にふさわしい関係であることが保証されます。

CoqやIsabelleの型クラスのインスタンス化では、公理(要求される制約)を満たすことの証明を要求されます。通常のプログラミングで、型定義の際に証明を要求されるのは現実的ではありません。しかし、指標だけでは上っ面の構文を規定しただけで、型の内実は何も制約してません。「x == y を x < y と具体化してはいけない」は人間側のモラルに過ぎません。

「指標+公理」という意味の型クラスには、CoqやIsabelleの型クラスがいいのですが、ややこし過ぎる、しかしHaskell型クラスやML指標では構文だけで貧弱過ぎる、という現状。

「指標+公理」の記述には、CafeOBJのような形式仕様記述言語が一番いいような気がするんですが、CafeOBJを知っている人/使っている人が少な過ぎて、実効性がありません。実は、Categorical InformaticsのFQL/OPLも「指標+公理」の説明には好適な素材・道具なんですが、ユーザーの少なさはCafeOBJと同様の問題です。


関数型プログラミングにもオブジェクト指向にも関係があって、今後重要度を増すであろう「型クラス」ですが、今述べた(愚痴った)ような事情で(あと、C++のコンセプトは宙ぶらりんだし)、説明の方針も題材も定まりません。でも、いつか、何か書く、かも。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20160916

2016-09-15 (木)

一般化されたマイヒル/ネロードの定理 3:オートマトンの振る舞いと観測

| 12:45 | 一般化されたマイヒル/ネロードの定理 3:オートマトンの振る舞いと観測を含むブックマーク

ソフトウェアの設計と実装では、サブシステムやコンポネントの内部構造を明かすべきではない、と考えられています。アプリケーションプログラムは、サブシステム/コンポネントの公式のインターフェイスにだけ依拠すべきだ、となります。それを守れば、サブシステム/コンポネントの内部構造が変わっても(インターフェイスが不変なら)アプリケーションはそのまま動き続けるでしょう。

上記のような原則や、それからの帰結を一般化オートマトンの文脈で定式化してみます。

内容:

  1. 隠蔽原則
  2. 復習:構文と意味
  3. 振る舞い
  4. オートマトンの振る舞いと観測
  5. 非退化指標/非退化オートマトン
  6. 振る舞いの反カリー化表現と観測手順
  7. リファクタリング補題と観測の関手性
  8. 今回のまとめ

隠蔽原則

一般化オートマトンの典型的な例は、伝統的オートマトンや特定のインターフェイスに対する実装クラスなどです。これらのオートマトンは内部構造を持ちます。しかし、その内部構造を知ることは出来ないという仮定を置きます。この仮定を情報隠蔽原則(information hiding principle)、または単に隠蔽原則と呼びましょう。「実装の細部を利用者に漏らしてはならない」というアレです。

しかしですね、現実には内部構造(=実装の詳細)が見えちゃうこともあるんですよね。なので、隠蔽原則は、「内部構造を知り得るにしても、それを利用してはならない」という利用者側の規範だと捉えるのが実際的でしょう。

我々の設定において知ってはいけない内部構造(実装の詳細)とは、オートマトンの状態空間のことです。F:Φ→Setオートマトンのとき、xが隠蔽頂点ならF(x)は型xの状態空間です。そのようなF(x)がどんな集合であるかは何も分からないということです。状態空間F(x)の正体は完全に未知(不可知)なのですから、F(x)からの写像やF(x)への写像の正体もサッパリ分かりません

一方で、xが可視頂点(x∈(S∪D))なら、F(x)は既知の値空間であり、完全に理解できます。既知の値空間(例:整数値の空間、真偽値の空間)のあいだの関数もまた完全に理解できるとします。

徹底した隠蔽原則の支配下において、我々は何が出来るでしょうか? -- この問題意識が、マイヒル/ネロードの定理の源泉です。そして、マイヒル/ネロードの定理が教えてくれる答は、「頑張れば、知りたいことは何でも分かる」です。

「頑張る」とは何をすることでしょう? 「知りたいこと」とは何でしょう? 今後、これらに正確な定義を与えていくことにします。

復習:構文と意味

一般化されたマイヒル/ネロードの定理 2:文化的なギャップを乗り越えるための対訳表」で述べたように、このテの話題で最大の難関は言葉・用語法・記法の問題だと思います。もう一度言葉の一覧表を示しておきます。「くどい」と思われる方はこの節をスキップしてください。以下、Φ = (Φ, S, D), C = FreeCat(Φ), Hid = |Φ|\(S∪D) です。

モノ グラフ理論 圏論 形式的プログラム構文論 説明
|Φ|の要素 頂点 対象 ソート記号 型の名前
Φ(x, y)の要素 (生成系の)射 オペレーション記号 基本手続きの名前
C(x, y)の要素 パス オペレーション記号の列 プログラムコード
Dの要素 開始頂点 開始対象 開始ソート記号 コンストラクタの引数の型の名前
Sの要素 識別頂点 識別対象 識別ソート記号 クエリーの値の型の名前
D∪S の要素 可視頂点 可視対象 可視ソート記号 既知の型の名前
Hidの要素 隠蔽頂点 隠蔽対象 隠蔽ソート記号 不可知な型の名前
s∈S, x∈Hid として Φ(s, x)の要素 コストラクタ辺 コンストラクタ射 コンストラクタ記号 コンストラクタの名前
x∈Hid, d∈D として Φ(x, d)の要素 クエリー辺 クエリー射 クエリー記号 クエリーの名前
x, y∈Hid として Φ(x, y)の要素 コマンド辺 コマンド射 コマンド記号 コマンドの名前

これらは指標グラフΦ、指標圏Cに関連する概念で、すべては構文的存在物です。意味は、関手 F:CSet によって与えられます。意味を与える関手Fがオートマトンそのものです。Fの行き先は集合圏なので、集合と写像の世界です。構文に対応する意味的存在物は次のように呼びます。

モノ 呼び名
x∈(D∪S) として F(x) 値空間
s∈S として F(s) 開始値空間
d∈D として F(d) 識別値空間
y∈Hid として F(y) 状態空間
s∈S, x∈Hid, c∈Φ(s, x) として F(c) コストラクタ写像
d∈D, x∈Hid, q∈Φ(x, d) として F(q) クエリー写像
x, y∈Hid, f∈Φ(x, y) として F(f) コマンド写像

ΦやCに属するモノ(頂点、辺、パス)とSetに属するモノ(集合、写像)は徹底的に区別しましょう。そうでないと、話がワヤクチャになります。

例として、整数スタックの指標グラフを再掲します。(thisがマズかったなー、という話は「整数スタックの例」に追記で強調されてます。マズイけど、そのまま。)

この例において:

  • 開始頂点:{void, int}
  • 識別頂点:{boolean, intError}
  • 可視頂点:{void, int, boolean, intError}
  • 隠蔽頂点:{this}
  • コンストラクタ辺:{emptyStack, singletonStack}
  • クエリー辺:{isEmpty, top}
  • コマンド辺:{pop}∪{push(n) | n∈Z}

可視頂点には、前もって実際の集合が割当てられています。その割当ては固定化関手Kで行われます。

  1. K(void) = 1 = {0}
  2. K(int) = Z = {... -1, 0, 1, 2, ...}
  3. K(boolean) = B = {true, false}
  4. K(intError) = Z∪{error}

この例の指標をΨとして、オートマトン G:Ψ→Set を定義するとは、次のモノを決めることになります。

  1. 集合 G(this)
  2. 写像 G(emptyStack):1→G(this)
  3. 写像 G(singletonStack):Z→G(this)
  4. 写像 G(isEmpty):G(this)→B
  5. 写像 G(top):G(this)→Z∪{error}
  6. 写像 G(pop):G(this)→G(this)
  7. n∈Zごとの写像 G(push(n)):G(this)→G(this)

数学的な記法ではなくて、実在のプログラミング言語でGを書き下してみましょう。TypeScriptを使ってみます。

// IntStack.ts

// intがないのでナンチャッテ定義
// 名前がintになっているだけ
type int = number;

class IntStack {
    private list_: int[]; // G(this) = List(Z) 隠蔽されている
    constructor() {
        this.list_ = [];
    }
    // メイヤー先生のクエリ
    isEmpty() : boolean {
        return (this.list_.length == 0);
    }
    top() : int {
        if (this.isEmpty()) {
            throw new Error("error");
        }
        return this.list_[this.list_.length - 1];
    }

    // メイヤー先生のコマンド
    pop() : void {
        if (this.isEmpty()){
            return; // ちと分かりにくいが、何もしない
        }
        this.list_.pop();
    }
    push(n : int) : void {
        this.list_.push(n);
    }

    // 生成子(コンストラクタ)
    // TypeScriptネイティブのコンストラクタを使って
    // static関数として実装
    static emptyStack() : IntStack {
        return new IntStack();
    }
    static singletonStack(n : int) : IntStack {
        var stk = new IntStack();
        stk.push(n);
        return stk;
    }
}

振る舞い

Φ = (Φ, S, D), K:ΦvisSetとして、部分固定指標Φ/Kに対して、振る舞いと呼ばれるモノを定義します。振る舞い(behavior, behaviour)とは、s∈D, d∈D で添字付けられた写像の族 bs, d:C(s, d)→Set(K(s), K(d)) のことです。ここで、C = FreeCat(Φ) です。振る舞いは英字小文字ボールド体で示すことにします -- a, b などは指標グラフΦの辺、指標圏Cの射を表すことがあるので区別したいのです。

伝統的オートマトンの部分固定指標Φ/Kについて、その振る舞いを見てみます。Φ/Kが伝統的オートマトンの部分固定指標なら、|Φ| = {0, 1, 2}, S = {0}, D = {2}, Φ(0, 1) = {i}, Φ(1, 1) = Γ, Φ(1, 2) = {t}, K(0) = 1, K(2) = B となります。振る舞いは b0, 2 だけで決まるので、b0, 2を単にbと書きます。

振る舞いの定義より、b:C(0, 2)→Set(1, B) という写像です。C(0, 2) ¥stackrel{¥sim}{=} C(1, 1) = Γ* です。Γ = Φ(1, 1) で、Γ* はΓのクリーニスターです。一方、Set(1, B) ¥stackrel{¥sim}{=} B なので、結局 b*B とみなしてかまいません。

b*B に対して、b-1(true) はΓ* の部分集合です。逆にΓ* の部分集合から、写像 Γ*B が決まります。Γ* の部分集合とは、アルファベットΓの形式言語に他なりません。つまり、伝統的オートマトンにおける振る舞いと形式言語は1:1対応するのです。

部分固定指標Φ/Kに対して、その振る舞いの全体からなる集合をBeh[Φ/K]とします。Φ/Kが伝統的オートマトンの部分固定指標の場合は、上で述べたとおり、Beh[Φ/K]はアルファベットΓ上の言語の集合と同じものです。Γ上のすべての形式言語からなる集合をLang(Γ)とすると、

整数スタックの例では、振る舞いbは次の写像達からなります。

  1. bvoid, boolean:C(void, boolean)→Set(1, B)
  2. bvoid, intError:C(void, intError)→Set(1, Z∪{error})
  3. bint, boolean:C(int, boolean)→Set(Z, B)
  4. bint, intError:C(int, intError)→Set(Z,Z∪{error})

bint, intErrorの値の実例を幾つか出しましょう。次のパス(Cの射はΦのパス)を取ります。

  1. singletonStack;top
  2. singletonStack;push(2);push(3);top
  3. singletonStack;pop;top

これらのパスに対する値は:

  1. bint, intError(singletonStack;top) = λn∈Z.n
  2. bint, intError(singletonStack;push(2);push(3);top) = λn∈Z.3
  3. bint, intError(singletonStack;pop;top) = λn∈Z.error

オートマトンの振る舞いと観測

Φ/Kが任意の部分固定指標として、F:Φ→Set をΦ/K上のオートマトンとします。つまり、F∈|Autom[Φ/K]| 。記号Fは、F:Φ→Set と F:CSet の両方を表します(「プレオートマトンの定義」参照)。関手FのホムセットC(x, y)への制限をFx, yと書くことにします。

オートマトンFの振る舞いbは、簡単に定義できます。

  • bs, d := Fs, d

要するに、関手Fを、SからDへのホムセットに制限したものがFの振る舞いです。オートマトンFにその振る舞いを対応させることを振る舞い観測(behavior/behaviour observation)、または単に観測(observation)と言います。

振る舞い観測は、(オートマトン |→ 振る舞い) という対応なので、Obs:|Autom[Φ/K]|→Beh[Φ/K] という写像になります。この定義からは、Obsは関手にはならないように思えますが、実は関手になります(後述)。

Aが伝統的オートマトンで、Fが対応する関手オートマトンだとします。このとき、Fの振る舞いは、伝統的オートマトンAが受理する形式言語と同じことです。この事実を示すことは良い練習問題です。やってみてください。

一般的関手オートマトンFをその振る舞いから調べることは、伝統的オートマトンを受理言語から調べる方法の一般化になります。伝統的マイヒル/ネロードの定理の一般化も、このラインに沿って行います。

非退化指標/非退化オートマトン

今後、振る舞い全体の集合Beh[Φ/K]を道具に使うのですが、指標グラフ Φ = (Φ, S, D) によっては振る舞いが無意味化することがあります。振る舞いbは、S×Dで添字付けられることになりますので、S×Dが空だと振る舞いは無意味になってしまいます。そこで次の条件を付けます。

  • 開始頂点族Sは空ではない。
  • 識別頂点族Dは空ではない。

Hid = |Φ|\(S∪D) として、Hidが空の場合も面白くありません。次の条件も追加します。

  • 隠蔽頂点族Hidは空ではない。

S, D, Hのすべてが空でない指標を非退化指標(non-degenerate signature)と呼びます。非退化指標Φを定義域とするようなオートマトン F:Φ→Set非退化オートマトン(non-degenerate automaton)と呼ぶことにします。非退化条件を満たさないモノは、退化した指標/オートマトンです。

今後扱う指標/オートマトンは、非退化であると仮定します。退化オートマトンでは観測が出来ません。

振る舞いの反カリー化表現と観測手順

b∈Beh[Φ/K] のとき、s∈, d∈D に対して bs, d:C(s, d)→Set(K(s), K(d)) ですが、少し変形しておくと取り扱いが便利になります。次の形です。

  • bs, d:K(s)×C(s, d)→K(d)

bs, dは、bs, dの反カリー化になっています。

集合圏SetのホムセットSet(K(s), K(d))は、集合の指数でもあるので、

  • bs, d:C(s, d)→K(d)K(s) in Set

と書けます。集合圏はデカルト閉圏なので、反カリー化により指数を直積に直して、

  • (bs, d):K(d)×C(s, d)→K(s) in Set

ここで、(-)は反カリー化する演算子とします。ほんとは (-) にしたかったんですが(そのほうが辻褄が合う)、「s, d」が下付きなので「∨」は上付きにしました。

  • bs, d := (bs, d)

と定義して、bの反カリー化bが出来上がります。

bでもbでも何の変わりもありませんが、オートマトン F∈Autom[Φ/K] の振る舞いを求める行為(つまり観測)は、bに基づいて次のように記述できます。

  1. 開始値(開始値空間の要素) u∈F(s) を選ぶ。
  2. プログラムコード(Cの射) f∈C を選ぶ。
  3. 実行系F上で、uをfに適用する。
  4. 評価結果(実行結果) F(f)(u)∈F(d) を見る。

このような、開始値/プログラムコードを選んでの個別観測行為をタクサンタクサン繰り返すことが、Fの観測です。観測行為の総体をObsで表すと、Obs(F)が実行系Fの振る舞いとなります。

リファクタリング補題と観測の関手性

次に述べる命題は、とても簡単に示せますが、意外な結果です。人によっては当たり前かも知れませんが、僕は驚きました。この結果を使えば、圏Autom[Φ/K]の構造を探れるな、と期待が持てたのでした。

Obsの定義から、s∈S, d∈D を任意に選んだとき、Fs, d = Gs, d を示せばいいわけです。αが自然変換であることから、次の図式が可換になります。

F(s) -αs→G(s)
|         |
F(f)       G(f)
↓         ↓
F(d) -αd→G(d)

ところが、オートマトンはS, D上では固定化関手Kと一致するので、F(s) = G(s) = K(s), F(d) = G(d) = K(d), αs = idK(s), αd = idK(d) となり、

  • F(f) = G(f)

が成立します。fは任意なので、「任意の f∈C(s, d) に対して F(f) = G(f)」が成立し、Fs, d = Gs, d が言えます。QED.

F→G または G→F のどちらか一方向でも準同型写像があれば、FとDは同じ振る舞いを持ちます。隠蔽原則の支配下にある我々に出来ることは振る舞い観測だけなので、準同型写像で結ばれた2つのオートマトンF, Gを区別することは出来ません。別な言い方をすると、準同型写像 α:F→G があるなら、振る舞いを一切変えずにインターフェイスΦ/Kの実装をFからGに(あるいはGからFに)取り替えることが出来るのです。準同型写像αはリファクタリングと捉えられます。もっと正確に言うと、準同型写像の存在がリファクタリングの正当性の保証を与えます。

Φ/Kを(一部実装付き)のインターフェイス、Φ/K-オートマトンをインターフェイスの実装、振る舞い観測は網羅的ブラックボックス・テストと解釈できます。FとGの振る舞いが一致することは、「実装FをGに取り替えても気付かれない」という意味でリスコフ置換可能性です。次のように言っていいでしょう。

  • Fの振る舞いとGの振る舞いは一致する ⇔ FとGはリスコフ置換可能である

メイヤーオートマトンに関するマイヒル/ネロードの定理を宣伝する」では次のように説明しています。

メイヤーオートマトンは、Command-Query分離されたインターフェース(メイヤー指標)の実装ですが、「アプリケーションプログラムから見て区別が付かない」とは、どんなに頑張ってテストしても挙動の食い違いを発見できない、ことです。

どんなに頑張ってテストしても挙動の食い違いを発見できないなら、それは異なる実装と考える必要はなくて、(事実はどうあれ)「同じ実装」とみなして差し支えありません。この「同じ」という概念がリスコフ置換可能性としての同値関係です。

この節の冒頭で出した「オートマトン準同型写像(自然変換) α:F→G があるとき、Obs(F) = Obs(G)」は、「リファクタリングしても振る舞いは変わらない」と読めます。もう少し正確に言うと:

  • Gを構成した。
  • FからG(あるいはGからF)への準同型写像が存在する。
  • このとき、GはFをリファクタリングして作った、と言ってよい。
  • なぜなら、FとGは同じ振る舞いを持つから。

この点を鑑み、「オートマトン準同型写像(自然変換) α:F→G があるとき、Obs(F) = Obs(G)」という命題をリファクタリング補題として参照します。

リファクタリング補題から、「振る舞い観測は関手と考えてよい」ことが導けます。

  • α:F→G in Autom[Φ/K] に対して Obs(f) = idObs(F) = idObs(G) と定義すると、ObsはAutom[Φ/K]から離散圏とみなしたBeh[Φ/K]への関手となる。

離散圏とは、恒等射だけを射とする圏です。この関手性は、定義を知っていれば簡単に示せるのでやってみてください。

今回のまとめ

隠蔽原則とは次のことです:

  • サブシステム/コンポネントの実装者は、内部構造(実装の詳細)を利用者に知らせてはならない。
  • サブシステム/コンポネントの利用者は、仮に内部構造を知り得るにしても、その情報を利用してはならない。
  • 我々のモデルにおいて、サブシステム/コンポネントとは一般化されたオートマトンであり、内部構造とは状態空間のことである。

隠蔽原則の支配下において可能なことは、ブラックボックス・テストだけです。テスト対象プログラムコード f∈C(s, d) と開始値 u∈K(s) を選んで実行すると、識別値 F(f)(u)∈K(d) が得られます。この行為を網羅的に行うと、K(s)×C(s, d)→K(d) が得られるますが、カリー化すれば、C(s, d)→Set(K(s), K(d)) ともみなせます。

網羅的ブラックボックス・テストの概念を抽象化すると、振る舞いの集合Beh[Φ/K]と観測関手 Obs:Autom[Φ/K]→Beh[Φ/K] として表せます。Obsが(離散圏への)関手であることは、次のリファクタリング補題から従います。

αの存在は実装者視点からのリファクタリングの正当性保証であり、Obs(F) = Obs(G) は利用者視点で「FとGは区別できない(リスコフ置換可能である)」ことです。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20160915

2016-09-13 (火)

「関数型プログラミングはオブジェクト指向の正当な後継」なの?

| 11:33 | 「関数型プログラミングはオブジェクト指向の正当な後継」なの?を含むブックマーク

オブジェクト指向を知っている人々に、「関数型もオブジェクト指向と大差ないよ、大丈夫だよ」とお誘いする記事は大いに存在意義があると思います。

上記の記事は、そういう目的を持って書かれたのでしょう。その内容(目次)は次のようです(僕のこの記事の目次じゃないよ)。

  1. 対象読者
  2. なぜこの記事を書こうと思ったのか?
  3. なぜ関数型プログラミングはわかりにくいのか?
  4. オブジェクト指向の負の遺産を捨てよう
  5. 関数型プログラミングの概要
  6. 「阿吽の呼吸」とも言うべき使いやすさの拡張
  7. 型にまつわる考察
  8. まとめ

最初のほうを読むと、言ってることはまっとうで好感を持てます。が、「5. 関数型プログラミングの概要」の節あたりから雲行きが怪しくなって、ちょっと何言ってるかわかんない((c)サンドウィッチマン)。

檜山のこの記事の内容:

  1. 真面目なポエム
  2. モナドっておいしいの?
  3. オブジェクトは仮想機械
  4. そもそも関数とは何?
  5. 制御構造不要なら楽ちん!
  6. それで結局、関数型プログラミングオブジェクト指向の後継なの?

真面目なポエム

「んんんーー??」と思って「はてなブックマーク」コメントをチェックしたら、id:kmizushimaさんが「ポ、ポエムだー!!」と叫んでいました。

僕の言葉で言えば、retemoさんによる当該Qiita記事は「具体的じゃない」ものです。僕の「具体的/抽象的」の用法は、たぶん標準的日本語とズレていて、「具体的じゃない」は、「掴み所がない」とか「あやふや過ぎる」といった意味で使います(抽象的かどうかとは無関係)。詳細は次の記事:

retemoさん記事は、何か言いたいことがあるのは確かだし、それがひどくトンチンカンだとも思いません。具体性に欠けるので、“ちょっと何言ってるかわかんない”(kmizushimaさんの言う“ポエム”)になっているのでしょう。“何言ってるかわかんない”けど、「真面目さ」が感じられて、僕の好感はさほど損なわれませんでした。

意味不明な記述を僕なりに解釈・注釈し(それが無理な所もあります)、多少の補足をしてみます。解釈に推測が入るので、「たぶん…らしい/でしょう」の表現が多用されます。歯切れ悪いけど、推測だからね。

このテの話題は、当ブログ「キマイラ飼育記」で10年以上に渡って扱ってきたものですから、掘り返せば、たいていのことが過去記事にあります。再度説明する代わりに適宜リンクを挿入します。大部分の説明を参照にしても、それなりに長い記事になってしまいました。

混乱が起きないように注意しておくと、引用はすべてretemoさん記事からです。自分の記事は引用してません。参照のみです。それでも参照と引用が混乱しそうなところには横線を入れて区切ってます。

モナドっておいしいの?

関数型プログラミングはオブジェクト指向の正当な後継である - Qiita 3.なぜ関数型プログラミングはわかりにくいのか?》

関数だけをとっても理解しづらいのですが、さらに高度な概念で構成されるモナドについては聞けば聞くほど混乱が増すばかりです。

この問題をなんとか改善しようと言葉を選んでいるケースもあるのですが、それはそれで「詩的」というか「俳句的」というか、”ふんわり"し過ぎな傾向があります。

同感です。“ふんわり”し過ぎを避けて、でも厳密過ぎもしないレベルの説明を書いたことがあります(10年以上前)。

同様な趣旨、具体例で(9年以上前):

圏論に慣れてきたら、「モナドとは自己関手圏のモノイドなり」と理解するのが良いでしょう。

圏論? 全然わからん!」なら、シリトリから始めましょう(これも10年たった)。

オブジェクトは仮想機械

関数型プログラミングはオブジェクト指向の正当な後継である - Qiita 4.オブジェクト指向の負の遺産を捨てよう》

オブジェクト指向のオブジェクトは[...snip...]古き良きチューリングマシンから今日の仮想化技術までを含む「抽象的な概念」としてのコンピュータです。

オブジェクトを仮想機械とみなすのも共感・賛同します

ここで言う仮想機械は、あくまで概念的なステートマシンです。

ステートマシンは「状態」と「遷移」、そして遷移を引き起こす「イベント」で構成されます。イベントにはトリガーやガード条件を含まれていて、「制御」と言いなおすことができます。同様に状態と遷移も「変数」及び「演算」と言い換えることができます。この「変数、演算、制御」がプログラミング言語や抽象的コンピュータの3大要素です。

僕は「言い換え」はしないほうがいいと思いますが、まー、ここは好みの問題としましょう(突っ込まない)。「イベント」はラベル付き状態遷移系(labeled transition system)のラベル、オートマトンの入力記号のようなものだろう、と、たぶん。「制御」が何を意味するか? ハッキリとは理解できませんでした。ガード条件を引き合いに出しているので、状態点に対する述語(状態空間上で定義された真偽値関数)をp、遷移を引き起こす関数(状態空間上の自己写像)をaとして、

  • if (p(x)) then a(x)

のような条件付き実行を「制御」と呼んでいるのでしょう。

実際、クリーネ代数の演算(順次結合、非決定性選択、非決定性繰り返し)に、if (p) then a というスタイルの「制御」(ガード付きの実行)を入れると、whileプログラムをシミュレートできます。

よって、「順次結合、非決定性選択、非決定性繰り返し」を暗黙に前提した上で、仮想機械としてのオブジェクトが「変数(状態)」「演算(遷移)」「制御(ガード条件)」から構成される、とするのは、悪くない定式化だと思います。

これら4つがオブジェクト指向を代表する技術トピックでしょう。[...sinp...]この4大トピックが1つ目の「定性的な物差し」です。

「これら4つ」とは、次のことらしいです。

  1. 継承と多態性の技術
  2. 独立したオブジェクト間をメッセージングでつなぐ技術
  3. 問題領域の区割りと仮想機械の区割りを関連付ける技術
  4. 仮想機械間の役割分担

僕は、原則だのトピックが4つだ5つだ、という数え上げには興味がないので、どうでもいいですが、「定性的な物差し」ということですから留意しておきましょう。「物差し」と言っているのは、これら4項目において、オブジェクト指向と関数型を比較しようじゃないか、という意図(らしい)です。

そもそも関数とは何?

関数型プログラミングはオブジェクト指向の正当な後継である - Qiita 5. 関数型プログラミングの概要》

関数型プログラミングの関数の特徴を簡潔に理解しようとすると、注目すべきは「参照透過性、関数合成、部分適用」の3つです。これらを順に見ていきましょう。

参照透過性は「入力が同じなら必ず同じ答えを返す」と書いてあるので、関数の純粋性と同じ意味ですね。あいにく僕は、純粋があまり好きじゃないです。

好き嫌いの話なので、別にいいとしましょう。関数合成の話も簡単だからいいとしましょう。んで、部分適用の話:

「部分適用」というのは「複数の引数を受け取る関数」に対して部分的に引数を渡すと、関数からは「足りない分の引数を取る関数」が返ってくる機能(というか技術)です。つまりたくさんの引数を持つ関数を段階的に実行することができます。

これはいい説明だと思います。でも、この説明の前後がなんか変。

[部分適用は]名称から「関数合成」と関係してそうなことは想像ができると思います。

名称から言ったら「関数適用」と関係するでしょ。「たくさんの引数を持つ関数を段階的に実行する」のは合成(composition)を繰り返してるんじゃなくて、適用(application, evaluation)を繰り返してます。

部分適用の説明の後で、「他にも」として、カリー化や高階関数が紹介されてますが、部分適用が出来るのはカリー化された高階関数だからであって、別な機能じゃないです。もっとも、部分適用を構文的利便性と解釈するなら、それを実現しているメカニズムがカリー化/高階関数だとは言えるので、「縁の下の力持ち」という文言を考慮すれば、これもまーいいか。

制御構造不要なら楽ちん!

「5. 関数型プログラミングの概要」のサブセクション「モナドのない関数型なんて」になると、だいぶ解釈が苦しくなります。retemoさんはモナドの雰囲気を伝えたいらしいのですが、僕は理解できません。

モナドは多様だということで、次のような記述があります(太字強調は檜山)。

  1. IOモナドはインターフェース役であることが一目瞭然
  2. ArrayモナドやDictionaryモナドあるいはリスト・モナドが構造役であることも疑う余地はない
  3. モナドは合成関数を作ってサービス役にもなれる
  4. モナドの主な使い方は「保持役(状態役)に暗黙の制御構造を付与すること」になります

この「ナントカ役」に関する知識が僕はないので分からないのかも知れません。センテンスレベル/パラグラフレベルでは“ちょっと何言ってるかわかんない”のですが、全体として「明示的な制御構造が不要になるから便利!」と訴えているのは伝わります

例えば、Optionalモナド(Maybeモナド)なら、次のような明示的if文が不要になる、ということでしょう。

if (isUndefined(x)) {
 // xの値が未定義のときの処理
} else {
 // xの値が存在するときの処理
}


それ[Optionalモナド]が本領を発揮するのは関数をOptionalチェーンで繋げる時です。

「Optionalチェーン」と言っているのは、Optionalモナドのクライスリ結合のことでしょう。条件分岐しながらの関数合成がスッキリするから便利だ、と。実際、そのとおりです

Listモナドのmap関数であれば、List.map(f)(x) と書けば、次のforループを不要にしてくれます。

  var y = [];
  for (var i = 0; i < x.length; i++) {
    y.push(f(x[i]));
  }
  return y;

制御構造要らん、あー、便利だ。と、たぶん、そんなことをretemoさんは言いたいのでしょう。

関数型プログラミングはオブジェクト指向の正当な後継である - Qiita 6.「阿吽の呼吸」とも言うべき使いやすさの拡張》

「継承と多態性の技術」は、1つのメソッド名で型に応じた別個のメソッドを自動的に呼び分けることができます。つまりは型をパラメータとしたswitch文的な条件分岐が暗に含まれているわけです。

「継承と多態性」はswitch分岐(型case)を不要にしてくれた、モナドもif分岐やfor繰り返しを不要にしてくれる、どっちも制御構造を不要にするから似てるよね、という話だと思います。

分かりきった手続きについての言及を省略した、言い換えれば「阿吽の呼吸」とも言うべき、そのユーザーフレンドリーな「暗黙の制御構造」の応用範囲をモナドは広げてくれるわけです。実際、多態性とモナドの使用感はよく似ています。

確かに、抽象化により煩雑な記述が省略できる点で多態性とモナドは似てなくもないですが、くくりが大雑把過ぎるかな、とは思います。このくくりなら、オーバーロードも入れちゃってもいい気がします。

それで結局、関数型プログラミングオブジェクト指向の後継なの?

疲れてきた。残りは急ぎ足。

残りの4つの節も、“ちょっと何言ってるかわかんない”表現が多いですが、特に難儀だったのは:

関数型プログラミングはオブジェクト指向の正当な後継である - Qiita 7. 型にまつわる考察》

「構造を抽象化した型」は「ジェネリックC++ではテンプレート、Haskellでは型コンストラクタ)」で、「扱いを抽象化した型」は「インターフェース(Swiftではプロトコル、Haskellでは型クラス)」であり、オブジェクト指向関数型プログラミングのいずれにも存在しています。

「構造」と「扱い」という言葉が分からなくて、一見では意味不明なんです…

ジェネリック」は型パラメータを具体化して型を返す、という意味らしいので、「構造を抽象化」するとは、具体型から型パラメータへの置き換え、かな、たぶん。「インターフェイス」が「扱いを抽象化」と言っているのは、具体的なメソッド群から実装を剥ぎとって名前だけにした、ってこと、かな、たぶん。

このへんは、ソート、指標、モデルといった概念で理解するのがいいと思いますよ。

できればインスティチューションで分析したいところ。割と圏論バッキバキだったりするんだけど:


Haskellでは型同士の継承をサポートしていませんが、型クラスから型インスタンスへの継承はできるため、それを利用した多態性の実現が可能です。

「型クラスから型インスタンス」は文字通りインスタンス化であって継承とは言わないでしょ。言ってもいいのかな? …… やっぱり、区別したほうがいいと思います。

型クラスの話題だとCoqになってしまうけど、多少は参考になるかも↓

さて、「オブジェクトは仮想機械」で挙げた「オブジェクト指向の4大技術トピック」に関しては、若干の説明の後で:

つまり実はオブジェクト指向の4大技術トピックは全て関数型プログラミングに継承されているわけです。

プログラミング言語AあるいはパラダイムAのメカニズムは、プログラミング言語BあるいはパラダイムBでシミュレートできる、逆のシミュレートもできる、という状況は多いです。そうなると、BがAの後継者とか進化形というよりは、A, Bお互いがメタ・ポジションを取りあう(実際は互角、割と不毛な)議論になるんじゃなかろうか。


[...snip...]どう見てもオブジェクト指向関数型プログラミングは直系ではありませんが、[...snip...]

歴史的経緯や、言語設計者の意図の観点からは、「関数型プログラミングオブジェクト指向の正当な後継である」と主張するには無理がありますよね。

こうしてみると表面上はかなり違って見えるオブジェクト指向関数型プログラミングが深い部分で繋がっていることが感じられます。

それを言うと、何だって深い部分では繋がってます。

関数型プログラミングオブジェクト指向の正当な後継であるというのはもはや極論ではないと思われます。

retemoさんの言いたいことは、おそらく、

  1. オブジェクト指向から関数型への移行には、それほど大きな障壁はないよ。
  2. 高水準の設計の技法・スキルは流用できるよ。

こんなことかな。そうなら異論はありません。ただ、それならそうと直截に言えばいいわけで、背景に無理筋な主張をあえて持ってくる必要があったんでしょうか? -- という疑問は残ります。

いずれにしても、retemoさんには経験と思いがあるのは確かでしょうから、事例、サンプルコード、図などを交えながら経験と思いをケレン味無く語れば、本来の目的である「オブジェクト指向関数型プログラミングの関係」を伝えることが出来るのではないでしょうか。

2016-09-12 (月)

「ミンナは間違っている」思考がなぜ生じるのか

| 10:04 | 「ミンナは間違っている」思考がなぜ生じるのかを含むブックマーク

一週間前に(悪い意味で)評判になったブログ記事:

ちょっとした火傷だったら、
キッチンのガス等で患部をあぶるっていいですよ。。

これはマズイ。真に受ける人が出たらどうするんだ、と思います。

「火傷はあぶる」の根拠は同種療法という考え方だそうで:

火傷をしたところは
冷やすのではなく
温めることで
早くよくなります


火傷しているところに
熱い蒸気をあてる
ここが同種療法の原理!

どうして、こう考えるのでしょう? ナイフで指を切ったらもうチョイ切り開くとか、頭を強打したらさらにボカスカ叩くとか、食中毒したらアタったものをさらに食べ足してみるとか、同種療法とはそういうものでしょうか。

「火傷はあたためる☆」のなかで、

普通は火傷をすると、すぐに流水等で冷やしますよね。。

と書いているので、多くの人が火傷を冷やすことはご存知の上で、あえて常識の逆を推奨しているわけです。

各種の陰謀論や、「相対性理論は間違ってる」説が後を絶たないので、「ミンナは間違っている」思考をする人は一定数いるようです。大多数の人が過ちを犯していたり、少数派の意見に軍配が上がることは確かにあります。しかしそれは稀です。稀なる事態への警告なら分かるのですが、ほとんど常に「ミンナは間違ってる」と考える常時逆張り思考は理解に苦しみます。

「なんでそんなふうに考えるのだろう」と不思議なんですが、比較的容易に自尊心の満足/自己肯定感を得られるから、かな? と考えます。「多数派であるミンナは間違っている、少数派・異端である私が正しい」と思えば、マイノリティがエリートに一転します。

現代の医学・科学・工学などは、それを正しく理解することは知的にシンドイ作業となります。安直、それゆえに分かりやすい批判(間違っている)を受け入れることは知的ハードルが低いし、「少数派の我々だけが正しいことを知っている」という思いは心地いいのかも知れません。

このテの問題で頭が痛いのは、「常識=既存理論を無批判に信じる輩こそ思考停止している。バカはお前だ」タイプの反論が常に可能だし、「では、多数派である常識=既存理論をチャンと勉強してみては」という説得もほぼ無意味なことです -- それが出来る人なら最初から安直な批判に与しない。暗澹たる気分になります。

「ミンナは間違っている」思考に陥ってしまうと、そこから抜け出すのは難しいだろうと思います。なので、それはもうショーガナイ、諦めましょう。しかし、実害があるような誤情報を流されるのは困ります。誤情報を抑制したり、訂正情報が行き渡る算段は必要でしょう。

「火傷 あたためる」でgoogle検索すると、「火傷はあたためる」を推奨する記事と否定する記事が混じりあっています(検索順位は日々変化するでしょうが)。「火傷はあたためる」を推奨する情報は、検索1ページ目に出て欲しくないな。

sodasoda 2016/09/14 10:18 ホメオパシーは世界的に有名なトンデモ医学なので、ツッコミどころしかないのは、いたしかたないかと…
https://ja.wikipedia.org/wiki/%E3%83%9B%E3%83%A1%E3%82%AA%E3%83%91%E3%82%B7%E3%83%BC

m-hiyamam-hiyama 2016/09/14 11:31 sodaさん、
> ツッコミどころしかないのは、いたしかたないかと…
ハマってしまった人は救えない気がします。でもね、子供に「火傷は温める」とか教えてしまうのは、ほんとにほんとにやめて欲しい。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20160912

2016-09-09 (金)

一般化されたマイヒル/ネロードの定理 2:文化的なギャップを乗り越えるための対訳表

| 10:42 | 一般化されたマイヒル/ネロードの定理 2:文化的なギャップを乗り越えるための対訳表を含むブックマーク

もともとのマイヒル/ネロードの定理は、形式言語理論のなかに位置付けられるものです。しかし僕は、プログラム意味論のなかでマイヒル/ネロードの定理を捉えています。一般化されたマイヒル/ネロードの定理は、プログラムの構文と意味に関して様々なことを教えてくれます。そのこと(の一部)は次の記事に書きました。

リアルな問題に対して、マイヒル/ネロードの定理は具体的に応えて(答えて)くれます。しかし、この「リアルさ」「具体性」がなかなか伝わらない。どうしてでしょう? 大きな障害は文化的なギャップだろうと思います。

リアルな問題に共感してくれる人が相手であっても、圏論を使った議論をすると、往々にしてアブストラクト・ナンセンス(抽象的空論)と敬遠されてしまいます。一方、圏論を理解している人でも、リアルな問題に馴染みがなければ動機が分からず、「なんのためにソレやってんの?」となります。

このギャップはなんとかしたいのですが、難しい問題ですね。せめて、言葉の翻訳規則くらいは提供しましょう。異なる文化で使われている言葉はまるで違っていて、翻訳なしには理解不能ですから。

引き続く節で、「一般化されたマイヒル/ネロードの定理 1:準備と事例」で導入した圏論グラフ理論形式言語理論などの言葉が、プログラム/ソフトウェアでは何に対応するのかを説明していきます。

内容:

  1. プログラムのモデルとしての一般化オートマトン
  2. 指標グラフに関する言葉
  3. 指標圏に関する言葉
  4. 関手に関する言葉

プログラムのモデルとしての一般化オートマトン

一般化されたマイヒル/ネロードの定理 1:準備と事例」において僕がセットアップしたのは、プログラムの構文論と意味論のための枠組です。これは、形式言語理論/オートマトン理論の枠組を一般化しています。しかし、プログラム意味論としては極めて限定的でプアなものです。

プログラムに制御構造はなくて、出来ることは順次実行だけです。if文(条件分岐)もwhile文(繰り返し)もなく、再帰も出来ません。プアですよね。非決定性分岐は簡単に入れられますが、今回はそれも入れてません。

プログラムの基本構成素である関数や手続きは1引数だけです。引数なしはユニット型(シングルトン型)の1引数で表せます。多引数を単一タプル引数でシミュレートすれば、それほど大きな制限ではないかも知れません。でも、引数を持つ状態遷移コマンドなどのモデル化は苦しくて、小細工が必要です。小細工の例は「整数スタックの例」のpush(n)を参照してください。

そういう事情で、一般化オートマトンはプログラムのモデルとしては不十分ですが、その分、取り扱いやすい面が多々あります。簡単なモデルからも有用な情報・知見を得ることが出来るのです。

指標グラフに関する言葉

言葉の対訳表を示します。簡単な説明は表内にありますが、補足的な説明は表の後に書きます。

モノ グラフ理論 形式的プログラム構文論 説明
Φ (有向)グラフ 構文構成素の集合 インターフェイス定義
|Φ|の要素 頂点 ソート記号 型の名前
Φ(x, y)の要素 オペレーション記号 手続きの名前

指標グラフΦは、プログラムの構文を決めるものです。構文は、使える型の名前と手続きの名前を提示すれば決まります。「手続き」という言葉は、「関数、メソッド、命令(インストラクション)、サブルーチン、アクション」などと呼ばれている概念を総称的に表すために使います。

次の表のなかで、Φの隠蔽頂点の集合をHidとします。Hid = |Φ|\(S∪D) です。

モノ グラフ理論 隠蔽代数の理論など 説明
S∪D の要素 可視頂点 可視ソート記号 組み込みの値型の名前
Hid の要素 隠蔽頂点 隠蔽ソート記号 ユーザー定義オブジェクト型の名前
x, y∈(S∪D) として Φ(x, y)の要素 可視辺 可視オペレーション記号 組み込み関数の名前

組み込みの値型(value type)とは、整数型や真偽値型のことです。文字列型も、イミュータブルなら値型と考えていいでしょう。ユーザー定義せずとも始めから使える型/手続きの名前が可視ソート記号/可視オペレーション記号で、グラフ上では可視頂点/可視辺と呼ぶのです。

次の表を理解するには、メイヤー先生の「Command-Query分離の原則」が必要です。「メイヤー先生の偉大さとCommand-Query分離」を参照してください。

モノ 説明
s∈S, x∈Hid として Φ(s, x)の要素 コンストラクタの名前
Sの要素 コンストラクタの引数となる型の名前
d∈D, x∈Hid として Φ(x, d)の要素 クエリーの名前
Dの要素 クエリーの値となる型の名前
x, y∈Hid として Φ(x, y)の要素 コマンドの名前
x∈Hid として Φ(x, x)の要素 遷移コマンドの名前
x, y∈Hid, x≠y として Φ(x, y)の要素 変容コマンドの名前

S, Dなどの頂点の部分集合を導入するのは、コマンドとクエリーを区別する手段としてです。他に、伝統的オートマトンの始状態と終状態を真似るため、という動機もあります。

コマンド(の名前)は、さらに遷移コマンド(transition command)と変容コマンド(mutation command)に分けています。遷移コマンドは同一の状態空間内の移動で、異なる状態空間に飛び移るのが変容コマンドです。遷移コマンドは、圏では自己射(endomorphism)になります。

指標圏に関する言葉

以下、C = FreeCat(Φ) であると仮定して、C指標圏(signature category)と呼びます。

モノ グラフ理論 圏論 説明
Φ グラフ 自由圏の生成系 インターフェイス定義
C 全てのパスの集合 自由圏 全てのプログラムコードの集合
|Φ| = |C| の要素 頂点 対象 型の名前
C(x, y) の要素 パス プログラムコード
f;g パスの連接 射の結合(合成) プログラムコードの順次結合

指標グラフΦにより、型と基本手続き(primitive procedure)の名前が提示されます。頂点が型の名前、辺が基本手続きの名前でした。Φから作られた自由圏Cは、基本手続きをもとに作られた全てのプログラムコードを表現します。基本手続きを複合する方法は順次結合(sequential composition)だけです。

指標Φが次のような形をしているとき、それは伝統的オートマトンの指標です。

この特殊な状況では、次の言葉を使います。

モノ ラベル付き遷移系 オートマトン 説明
Γ = Φ(1, 1) ラベル集合 アルファベット 遷移コマンド名の集合
Φ(1, 1) の要素 ラベル 字(letter)、語 遷移コマンド名
C(1, 1) の要素 ラベル列 語、文 プログラムコード
id1 空列 空語、空文 空プログラムコード

隠蔽頂点(隠蔽ソート)がただ1つしかない場合がラベル付き遷移系や伝統的オートマトンです。プログラムにおけるクラスのインターフェイスでは、唯一の隠蔽ソート(図では頂点1)がthisやselfとなります。[追記]thisやselfは型の名前そのものというより、変数のように使われるので、正確には「thisやselfが走る領域に付ける名前・番号」とか言うべきでした。[/追記]

関手に関する言葉

指標グラフΦと指標圏Cは、プログラムの構文を定義します。プログラムの意味を定義するのが関手 F:CSet です。プログラムの意味は実装(implementation)と呼んでもいいでしょう。

モノ 説明
F:Φ→Set インターフェイスΦの実装
K:ΦvisSet 組み込み部分の事前実装
x∈(S∪D) として F(x) 型xの値空間
y∈Hid として F(y) 型yの状態空間
a∈Φvis(x, y) として K(a) = F(a) 組み込み関数aの表示的意味
b∈Φ(x, y) として F(b) 基本手続きbの表示的意味
f∈C として F(f) プログラムfの表示的意味

x∈|Φ| は型の名前で、F(x)∈|Set| が実際の型(データ領域)となる集合です。ここでは、「型の意味は集合(Sets-as-Types)」という素朴な立場をとっています。x∈Hid とは、名前xがオブジェクトの型(クラス)を表すことです。そのときのF(x)は、オブジェクト状態の集合なので状態空間(state space)と呼ぶのです。一方、組み込み型の値の集合は値空間(value space)です。

f:x→y in C は、単なるプログラムコードであり、構文的な存在です。x, y も単なる名前と考えます。それに対して、F(f):F(x)→F(y) は集合のあいだの写像です。集合と写像に対して、プログラム的なニュアンスを付けるために次のような呼び名で区別するのです。

  • 値空間
  • 状態空間
  • 値空間のあいだの組み込み関数
  • ユーザー定義のコンストラクタ
  • ユーザー定義のクエリー・メソッド
  • ユーザー定義のコマンド・メソッド(遷移と変容)

集合と写像何の色も付いてない味気ないものです。無味無臭の集合/写像に、プログラミング上の役割を(間接的に)付与する手段が、開始頂点族Sと識別頂点族Dだったのです。


上記の対訳表により、関手オートマトンを構成している Φ, S, D, K, F の現実的な対応物が了解できると思います。この対応(翻訳)を適用すれば、抽象的な構成や言明から、現実的な意味を汲み取ることができるでしょう。

実は、ここに書かなかった“論理との対応”もあります。クエリー名が述語記号に対応し、引数なしコンストラクタ名は定数記号に対応します。関手Fは、個体項や論理式の意味論(=モデル)です。論理もまた異なる文化圏なので、まったく違った言葉が使用されます。同じ内実に対して、言葉だけがどうしてこうも大量にあるのか!? と溜め息が出ますが、まー、言ってもしょうがない。

2016-09-08 (木)

一般化されたマイヒル/ネロードの定理 1:準備と事例

| 13:32 | 一般化されたマイヒル/ネロードの定理 1:準備と事例を含むブックマーク

一般化されたマイヒル/ネロードの定理について「いつかキチンと書こう」と思いながら10年が経過してしまいました。「もっと一般化したい」「前提を減らしたい」「キレイにまとめたい」「高次元化したい」とかの希望はあるのですが、それを言っているとさらに先延ばしになってしまうので、とりあえず現時点でハッキリと言えることを、なるべく正確に記述することにします。

一回に書き切れる量ではないので、何度かに分けます。でも、次回が数年先にならないように努めます。

内容:

  1. 今までの経緯=先延ばしの歴史
  2. 用語法の注意
  3. プレオートマトンの定義
  4. 伝統的オートマトン
  5. 反変オートマトンオートマトンの双対
  6. 整数スタックの例
  7. 指標グラフの操作:制限と除去
  8. 開始頂点族、識別頂点族、固定化関手
  9. オートマトンの定義:開始と識別の構造
  10. 今回のまとめ

シリーズ記事リンク:

今までの経緯=先延ばしの歴史

マイヒル/ネロードの定理のソフトウェア的解釈を、僕が最初にメモっているのは、2006年5月のようです。

6年後の2012年4月の記事「メイヤー代数、メイヤー指標、メイヤーオートマトン」において:

到達可能性と識別可能性という概念を使い、マイヒル/ネロード(Myhill/Nerode)風の定理を導きます -- この話は長くなるのでまた別な機会にしましょう。

記事タイトルに含まれる「メイヤーオートマトン」(Mayer automaton)は、通常の定義に比べて一般化されたオートマトンのことです。上記引用記事の10日ほど後の記事「メイヤーオートマトンに関するマイヒル/ネロードの定理を宣伝する」で、メイヤーオートマトン(=一般化されたオートマトン)に対するマイヒル/ネロードの定理が示せたら何が嬉しいのか、どんなご利益があるのかを説明しています。

その後、関連する概念や予備知識の説明を少しだけしたことはあります(下の記事など)。

しかし、完全な記述はないので、これからチャント書こうと思います。過去の記事への参照はしますが、説明を丸投げはしないで、なるべく自己完結的になるようにします。ただし、一般性が高い予備知識まで再度説明することはしません。また、動機や背景の説明は省略することが多くなると思います。←けっこう詳しく書くつもり。

用語法の注意

これから扱う“オートマトン”は、一般化されたオートマトンです。これは、数年前に僕がメイヤーオートマトンと呼んでいたものと同じです。単に「オートマトン」と言ったら、一般化されたオートマトンを意味することにします。つまり、

形式言語理論/オートマトン理論の教科書にあるような通常のオートマトンは、伝統的オートマトン(traditional automaton)と呼ぶことにします。伝統的オートマトンについても、一般化されたオートマトンについても、後でチャント定義します。

伝統的オートマトンに対するマイヒル/ネロードの定理(Myhill–Nerode theorem)は、正規言語とオートマトンの関連を述べた定理ですが、正規言語には特に拘らない定式化をします。一般化されたマイヒル/ネロードの定理は、一般化されたオートマトンに対するマイヒル/ネロードの定理のことです。単に「マイヒル/ネロードの定理」と言ったら、一般化されたマイヒル/ネロードの定理を意味することにします。つまり、

  • 一般化されたマイヒル/ネロードの定理=一般化されたオートマトンに対するマイヒル/ネロードの定理=マイヒル/ネロードの定理

基本概念を準備して補題を積み重ねれば、一般化されたマイヒル/ネロードの定理に到達します。全体の構図は頭にありますが、細部まで詰めたことはないので、それをこれからやる予定です。

プレオートマトンの定義

ここでは、(一般化された)オートマトンとして関手オートマトンを採用します。関手オートマトンについては、次の過去記事で扱ってますが、必要な事項はすぐ下で述べます。

オートマトンは始状態(初期状態)と終状態を持ちますが、それらは後で付加することにして、プレーンな状態遷移系に相当するプレオートマトンから考えましょう。プレオートマトン(preautomaton)とは、Cを小さい圏として、F:CSet という形の関手Fのことです。ただし、圏Cはグラフ(有向グラフ)から自由生成されたものに限定します。Φをグラフとして、CC = FreeCat(Φ) と書けることを常に前提するわけです。グラフをギリシャ文字大文字で書く理由は後(「伝統的オートマトン」の節)で説明します。グラフから自由生成された圏(自由圏、パスの圏、道の圏)については、次の記事を参照してください。

グラフと圏のあいだには次の随伴関係があります。

  • CAT(FreeCat(Φ), Set) ¥stackrel{¥sim}{=} GRAPH(Φ, Forget(Set))

ここで、CATは“必ずしも小さくない圏”の圏、GRAPHは“必ずしも小さくないグラフ”の圏です。大きな圏Setが含まれるので「必ずしも小さくない」という断り書きが必要になります。FreeCat:GRAPHCAT は自由生成する関手で、Forget:CATGRAPH は忘却関手です。

この随伴関係 FreeCat -| Forget があるので、自由圏FreeCat(Φ)からの関手とグラフΦからのグラフ準同型写像は1:1に対応します。この1:1対応により、関手とグラフ準同型写像を同じ記号で表すことがあります(記号の乱用です)。例えば、(F:FreeCat(Φ)→Set) ←→ (F:Φ→Set) のように、同じFで関手とグラフ準同型写像を表します。

プレオートマトンとは自由圏からの関手だったので、F:FreeCat(Φ)→Set または F:Φ→Set としてプレオートマトンを表すことになります。関手Fが値を取る圏をSet以外にすると、別種のプレオートマトンを定義できます。例えば、F:Φ→Rel なら、Fは非決定性プレオートマトンです。kを適当な体として、F:Φ→Vectk なら、Fはk-線形プレオートマトンになります。しかしここでは、関手の値の圏はSetに限ります。つまり、決定性プレオートマトンだけを考えることになります。

後(「オートマトンの定義:開始と識別の構造」の節)で述べるように、プレオートマトンオートマトンの差はたいしてないので、プレオートマトンオートマトンと呼ぶこともあります。特に強調したいときだけ「プレ」を付けることにします。

伝統的オートマトン

伝統的オートマトンを、先に定義した関手(プレ)オートマトンとみなす方法を見ておきましょう。

伝統的オートマトンは、A = (Γ, Q, δ, q0, T) として定義されます。ここで:

  1. Γはアルファベット(alphabet)です。どんな集合でもかまいません。伝統的にアルファベットはΣで表されることが多いのですが、大文字シグマを別な意味で使う可能性があるので大文字ガンマ(Γ)を使いました。
  2. Qは状態空間(state space)です。空でなければどんな集合でもかまいません。文字Sを使わなかったのは、Sを後で別な意味で使うからです。
  3. δは遷移写像(transition map)で、δ:Q×Γ→Q。これも何の制限もありません。
  4. q0始状態(initial state)。q0∈Q なら何でもいいです。
  5. Tは終状態(final state, terminal state)の集合で、T⊆Q。Tは空でない部分集合です。

A = (Γ, Q, δ, q0, T) から、グラフΦと関手 F:Φ→Set を作ります。再度注意しますが、関手とグラフ準同型写像を適宜同一視しています。F: Φ→Set は、ホントは関手じゃないけど、C = FreeCat(Φ) の関手に一意的に拡張できるので、“関手”とも呼びます。

これから作るグラフΦは、伝統的オートマトンAの指標グラフ(signature graph)、または単に指標(signature)と呼びます。インスティチューション理論では、指標をギリシャ文字大文字で表す習慣があるので、それに従ってギリシャ文字大文字を使ったのです。

Φはグラフですが、圏と同様な記法を使って、頂点の集合を|Φ|、x, y∈|Φ| に対して2頂点のあいだの辺の集合をΦ(x, y)で表します。伝統的オートマトンAに対する指標グラフΦは次の通りです。

  1. |Φ| = {0, 1, 2}
  2. Φ(0, 1) = {i}
  3. Φ(1, 1) = Γ
  4. Φ(1, 2) = {t}
  5. それ以外のΦ(n, m)は空集合

指標グラフΦは、アルファベットΓだけから決まり、その他の構成要素は関与してないことに注意してください。以下は、Γ = {a, b} の場合の指標グラフです。

次に、F:Φ→Set を定義します。(定義にインフォーマルなラムダ記法を使ってます。ラムダ記法については、過去記事「JavaScriptで学ぶ・プログラマのためのラムダ計算」、「絵を描いて学ぶ・プログラマのためのラムダ計算」などを参照してください。)

  1. F(0) = 11は特定された単元集合、1 = {0})
  2. F(1) = Q
  3. F(2) = BBは真偽値の集合で B = {true, false})
  4. F(i):1→Q は、0|→q0 で決まる写像
  5. a∈Γ に対するF(a):Q→Q は、λs∈Q.δ(s, a) で決まる写像
  6. F(t):Q→Bは、s∈Tならtrue、そうでないならfalseで決まる写像

以上で、伝統的オートマトン A = (Γ, Q, δ, q0, T) から指標グラフΦと関手(グラフ準同型写像)F:Φ→Set が決まりました。FはAの情報をすべて持っているので、関手Fから伝統的オートマトンAを再現できます

  1. Γ = Φ(1, 1)
  2. Q = F(1)
  3. δ(s, a) = F(a)(s) (F(a):Q→Q)
  4. q0 = F(i)(0) (F(i):1→Q)
  5. T = F(t)-1(true) (F(t):Q→B

反変オートマトンオートマトンの双対

決定性オートマトンだけの範囲では、双対性の議論はあまりキレイにまとまりません。僕が何か見落としているのかも知れないですが、非決定性オートマトンまで含めないと本質的にうまくいかない、って可能性もあります。しかしそれでも、双対を考えることは重要なテクニックです。

先に注意したように、グラフ準同型写像 F:Φ→Set に対応する関手も同じFで表します。C = FreeCat(Φ) とすると、F:CSet (関手) とも書きます。以下、CはFreeCat(Φ)の意味で使います。

オートマトンFはCからの共変関手でしたが、反変関手 G:CopSet を考えることもできます。関手として反変であるオートマトン反変オートマトン(contravariant automaton)と呼びます。余オートマトン(coautomaton)、反対オートマトン(opposite automaton)でもいいと思います。加群との類似では左オートマトン(left automaton)と呼ぶべきでしょうが、左右の区別は書き方で変わってしまうので、「左」「右」を積極的に使う気はありません。

オートマトン F:CSet があるとき、「Fの双対」が標準的に作れるかというと、それは出来ません。集合圏Setには標準的双対の概念がないからです。でも、人為的・恣意的な双対なら作れます。適当に V∈|Set| を選んで、Vに関して双対な反変オートマトンを構成します。

まず、集合圏SetにV-双対性を導入します。

  • 集合Xに対して、X*V := VX。ここで、VXは、XからVへの写像の全体からなる集合(関数集合、指数)。
  • 写像 φ:X→Y に対して φ*V:Y*V→X*V を、φ*V(ρ:Y→V) := φ;ρ と定義する。これは、φを前結合(pre-compose)しての引き戻しです。

X|→X*V と φ|→φ*V を一緒にすると、(-)*V:SetopSet という反変関手が定義できます。V = B = {true, false} のとき、(-)*Vは反変ベキ集合関手と同じものです。この V = B のケースが最もよく使う双対性です。

オートマトン F:CSetV-双対オートマトン(V-dual automaton)F*Vを次のように定義します。

  • x∈|C| に対して、F*V(x) := F(x)*V
  • f∈C(x, y) に対して、F*V(f) := F(f)*V

FのV-双対オートマトンは反変オートマトンであることに注意してください。Gが反変オートマトンである場合は、GのV-双対オートマトンを作ると共変オートマトンになります。V-双対により反変と共変が入れ替わります。

正確には「共変オートマトンFのV-双対な反変オートマトン」とか言うべきですが、反変・共変は文脈で判断してください。また、Vを固定している状況では、F*Vを単にF*と書くことがあります。

A = (Γ, Q, δ, q0, T) を伝統的オートマトンとして、F:Φ→Set を対応する関手オートマトンとします。V = B と固定して、Fの双対オートマトン F* = F*B を考えてみましょう。以下、Pow(X)はXのベキ集合です。

  1. F*(0) = B1 ¥stackrel{¥sim}{=} B
  2. F*(1) = BQ ¥stackrel{¥sim}{=} Pow(Q)
  3. F*(2) = BB ¥stackrel{¥sim}{=} Pow(B)

同型である集合は互いに置き換えても実質は同じなので、次のように定義してしまいましょう。

  1. F*(0) = B = {true, false}
  2. F*(1) = Pow(Q)
  3. F*(2) = Pow(B) = {{}, {true}, {false}, {true, false}}

i:0→1, t:1→2 と a:1→1(a∈Γ)に対するF*の値は次のようになります。

  1. F*(i):Pow(Q)→B は、λX∈Pow(Q).(if (q0∈X) then true else false)。
  2. F*(a):Pow(Q)→Pow(Q) は、λX∈Pow(Q).{y∈Q | F(a)(y) ∈X}。
  3. F*(t):Pow(B)→Pow(Q) は、{true}|→T, {false}|→(Tの補集合) で定義される写像

これで、Fの双対である反変オートマトンF*が定義できました。この例から分かるように、FとF*は強い対称性を持っているわけではありません。始状態と終状態が入れ替わっているようにも思えますが、実際には対称性は歪んでいます。対称性を得るには、個別の工夫が必要ですから、安易に対称性を期待してはダメです。

整数スタックの例

伝統的オートマトン以外のオートマトンの例も出しておきましょう。整数値を積むスタックを考えます。

スタックのインターフェイスを記述しましょう。インターフェイス記述言語は擬似言語ですが、なんらかのプログラミング言語を知っていれば意味はすぐ分かるでしょう。メイヤー先生については、「メイヤー先生の偉大さとCommand-Query分離」を参照してください。

interface IntStack {
 query: // メイヤー先生のクエリ
    isEmpty : this -> boolean;
    top : this -> int throws Error;
 command: // メイヤー先生のコマンド
    pop : this -> this;
    push : this, int -> this;
 creator: // 生成子(コンストラクタ)
    emptyStack : void -> this;
    singletonStack : int -> this; // 単一の要素を持つスタック
}

自分自身を表す暗黙のソート(型キーワード)thisを省略せずに書いています。popは例外を投げずに、空スタックに対しては何もしないだけとします。

[追記]thisはマズかったなー。thisの用法は、自分自身を表す型じゃなくて、変数のように使いますね。型は大文字始まりThisにして、this∈This とか、そんな感じにすればよかった。あるいは、interfaceの見出しに使ったIntStackを型の名前に使うか。

実際のthisの用法とは食い違いますが、絵(下)もあるので、モノグサしてそのままです。[/追記]

このインターフェイスIntStackに対応する指標グラフをΨを具体的に作りましょう。まず、|Ψ| = {this, void, boolean, int, intError} とします。intErrorは、例外が起きるかも知れない整数値の型です。グラフの辺に関して、pushだけは細工をします。pushは整数引数をもつので、引数の値ごとに1本の辺を作ります。push(0), push(1), push(-1), ... などがそれぞれ1本の辺になります。辺の集合は次のとおり:

  1. Ψ(this, boolean) = {isEmpty}
  2. Ψ(this, intError) = {top}
  3. Ψ(this, this) = {pop}∪{push(n) | n∈Z}
  4. Ψ(void, this) = {emptyStack}
  5. Ψ(int, this) = {singletonStack}
  6. その他のΨ(x, y)は空集合

指標グラフΨの形状は次のようになります。Ψ(this, this)は無限本の辺を持つので描き切れません。

次に関手 G:Ψ→Set を定義します。以下、List(Z)は整数のリストの集合です。

  1. G(this) = List(Z);
  2. G(void) = 1 = {0}
  3. G(boolean) = B = {true, false}
  4. G(int) = Z
  5. G(intError) = Z∪{error}

G(isEmpty), G(top), G(pop), G(push(n)), G(emptyStack), G(singletonStack) は、まーそれらしく定義します。すると、G:Ψ→Set は関手(グラフ準同型写像)となります。

指標グラフの操作:制限と除去

(プレ)オートマトンの指標としては、任意のグラフ(有向グラフ)を使えます。制限は何もありません。あえて指標グラフと呼ぶ理由は:

  • そのグラフΦから自由圏FreeCat(Φ)を作ることを前提している。
  • 出来た自由圏FreeCat(Φ)から集合圏Setへの関手を考える心積もりがある。

指標グラフに対する2つの操作をここで定義しておきましょう。

|Φ|はグラフΦの頂点の集合を表すのでした。X⊆|Φ|、つまりXを頂点全体の部分集合とします。新しいグラフΨを次のように定義します。

  • |Ψ| = X
  • Ψ(x, y) = Φ(x, y) (x, y∈X)

こうして作られるΨは明らかにΦの部分グラフになります。グラフ理論では、頂点の部分集合Xによる誘導部分グラフ(indueced subgraph)と呼ぶことが多いですが、ここでは圏論ぽい言葉使いをして、充満部分グラフ(full subgraph)と呼びましょう。充満部分グラフは、頂点の集合をXに制限したグラフとも言えます。ΦをXに制限したグラフ(充満部分グラフ)をΦ@Xと書くことにします。

同じく X⊆|Φ| として、|Φ|からXを取り除いて新しいグラフを作ることもできます。これは、「\」を差集合として、|Φ|\X にΦを制限することと同じです。念のために詳しく書くと:

  • |Ψ| = |Φ|\X
  • Ψ(x, y) = Φ(x, y) (x, y∈(|Φ|\X))

このΨを、ΦからXを除去したグラフと呼んで、Φ\X と書くことにします。定義より:

  • Φ\X = Φ@(|Φ|\X)

開始頂点族、識別頂点族、固定化関手

伝統的オートマトンには、始状態と終状態がありますが、一般化された(プレ)オートマトンには始状態/終状態の概念がまだありません。これから、始状態/終状態に類似の概念を導入します。そのためには、指標グラフに構造を与える必要があります。

Φを任意の指標グラフとします。頂点集合|Φ|の2つの部分集合S, Dを考えます。S⊆|Φ|、D⊆|Φ|、SもDも空でもかまいません。SとDの相互の関係(例えば「交わらない」など)は特に仮定しません。

上記の状況で、Sに属する頂点を開始頂点(starting vertex)、Dに属する頂点を識別頂点(distinguishing vertex)と呼びます。そして、集合Sは開始頂点族(family of starting vertexes)、集合Dは識別頂点族(family of distinguishing vertexes)と呼びましょう。

伝統的オートマトンの場合は、S = {0}, D = {2} です。開始頂点も識別頂点も1個ずつしかありません。それが伝統的オートマトンの特徴です。整数値を積むスタックでは、S = {void, int}, D = {boolean, intError} です。

グラフΦを、頂点の集合S∪Dに制限した部分グラフΦ@(S∪D)をΦvisとも書きます。visはvisible(可視)の意味です(由来は後述)。Φvisの定義を念のため書くと:

  1. vis| = S∪D
  2. x, y∈S∪D に対して、Φvis(x, y) = Φ(x, y)

vis| に属する頂点を可視頂点(visible vertex)と呼びます。定義から、可視頂点は開始頂点または識別頂点のことです。Φの部分グラフΦvis可視部分グラフ(visible subgraph)と呼びます。

可視頂点でない頂点は隠蔽頂点(hidden vertex)と呼びます。グラフΦから頂点の集合S∪Dを除去した部分グラフΦ\(S∪D)をΦhidとも書きます。hidはhidden(隠蔽)の意味です。Φの部分グラフΦhid隠蔽部分グラフ(hidden subgraph)と呼びます。

可視/隠蔽という呼び方は、ゴグエン(Joseph Goguen)などの隠蔽代数(hidden algebra)理論に由来します。隠蔽代数も指標により定義されますが、指標に登場する頂点を可視と隠蔽に分類するのです。ただし隠蔽代数では(他の多くの文脈でも)指標に関する用語法はグラフ理論とは異なる言葉を使います。

グラフの用語 指標に固有な用語
頂点 ソート記号(または単にソート)
オペレーション記号(または単にオペレーション)
可視頂点 可視ソート記号(または単に可視ソート)
隠蔽頂点 隠蔽ソート記号(または単に隠蔽ソート)
パス

可視ソート記号は、“既知の集合(型)”を表す記号、隠蔽ソート記号は“不可知な集合(型)”を表す記号です。両端が可視頂点(可視ソート)である可視辺(可視オペレーション)は、“既知の写像”を表すことになります。

したがって、可視頂点/可視辺(可視ソート/可視オペレーション)には前もって実際の集合/写像を割当てておきます。その割当てを K:ΦvisSet とします。Kはグラフ準同型写像ですが、関手ともみなします(関手なら FreeCat(Φvis)→Set)。Kは可視部分グラフの意味を固定するために使うので、固定化関手(fixtur functor)と呼びましょう。

可視/隠蔽の区別は、関手データベースでも使っています。次の図で、水色が可視頂点、ピンクが隠蔽頂点です。詳しくは「一般関手モデル:相対スキーマと相対インスタンス」を参照してください。

伝統的オートマトンの場合は、可視部分グラフは2個の頂点{0, 2}からなる離散グラフ(辺はない)で、K(0) = 1, K(2) = B で定義される K:{0, 2}→|Set| を固定化関手と思ってもかまいません。

これから考える指標グラフΦには、開始頂点族Sと識別頂点族Dが組み込まれているとして、Φ = (Φ, S, D) のように記します(記号の乱用)。また、固定化関手Kも入れた (Φ, K) = (Φ, S, D, K) をΦ/Kと略記します。ΦとKを組みにしたΦ/Kを、部分固定指標グラフ(partially fixed signature graph)、または単に部分固定指標(partially fixed signature)と呼びます。なお、「一般関手モデル:相対スキーマと相対インスタンス」では、部分固定指標グラフと同等な概念を相対スキーマと呼んでいます。

オートマトンの定義:開始と識別の構造

開始頂点族Sと識別頂点族Dが指定された指標グラフを Φ = (Φ, S, D) のように書きます。開始頂点族/識別頂点族を持つ指標Φと固定化関手 K:ΦvisSet を組にした部分固定指標Φ/Kがあるとき、Φ/K-オートマトン(Φ/K-automaton)とは、関手 F:Φ→Set であり、可視部分グラフΦvis上では固定化関手Kと一致するものです。言い方を換えると、(FをΦvisに制限した関手) = K という等式が成立します。

F, G:Φ→Set が2つのΦ/K-オートマトンのとき、FからGへのオートマトンオートマトン準同型写像)とは、関手Fから関手Gへの自然変換のことだとします。ただし、可視頂点上では自然変換の成分が恒等射となっているとします。αがオートマトン射であることは、α:F→G と書きますが、αを自然変換とみなすときは、α::F⇒G:CSet のようにも書きます。

Φ/K-オートマトンとそのあいだのオートマトン射の全体からなる圏をAutom[Φ/K]と書くことにします。なお、Autom[-]という記法は「形式言語理論のための代数」でも使っていますが、今回の定義とは異なります。

最初に定義したプレオートマトンは、指標グラフが何の構造も持たず(SやDが指定されてない)、固定化関手Kも指定されてない状況で定義されました。Ψを無構造の(SやDが指定されてない)指標グラフとして、プレオートマトンの圏をPreAutom[Ψ]とすれば、忘却関手 Forget:Aotom[Φ/K]→PreAutom[Ψ] を定義できます。ここで、ΨはΦのS, Dを忘れたプレーンな指標グラフです(Kも忘却します)。

実は、プレオートマトンオートマトンとみなす方法があります。Φ = (Φ, S, D) で、SもDも空集合のときは、可視部分グラフΦvisは空グラフです。固定化関手は空グラフ(空圏)からの関手なので一意に決まります(が、無意味です)。つまり、S = D = 00空集合)の場合は、SもDも指定しないのと同じです。よって、プレオートマトンオートマトンの特殊ケースとみなせます。

SまたはDが空の場合は:

  • Φ = (Φ, 0, 0) -- Φは無構造、Φvisは空で、固定化関手Kは無意味。
  • Φ = (Φ, S, 0) -- Φは開始頂点族だけを持つ、固定化関手Kは Φvis = Φ@S 上で定義される。
  • Φ = (Φ, 0, D) -- Φは識別頂点族だけを持つ、固定化関手Kは Φvis = Φ@D 上で定義される。

ここで注意を述べておきます; 開始頂点族と識別頂点族はデータ入出力ではありません。データ入出力を考えたいならまた別な定式化が必要です。データ入出力に対して、開始/識別と同じテクニックを使えることがありますが、開始/識別の構造を入出力に寄せ過ぎるのは好ましくありません。

今回のまとめ

今回やったことは、圏Autom[Φ/K]を定義したことです。Φは開始頂点族と識別頂点族を持つ指標 Φ = (Φ, S, D) であり、Kは固定化関手 K:ΦvisSet です。圏Autom[Φ/K]の対象が我々が扱うべきオートマトンですが、その実体は集合値関手です。したがって、圏Autom[Φ/K]は関手圏です。実際、オートマトンのあいだの射(準同型写像)は自然変換です。

今回、圏Autom[Φ/K]を定義した方法は、一般関手モデルとほとんど同じです。興味があれば、次の記事が参考になるでしょう。

(一般化された)マイヒル/ネロードの定理は、圏Autom[Φ/K]の構造を詳しく調べることで得られます。

2016-09-06 (火)

驚愕のバンビ達

| 15:11 | 驚愕のバンビ達を含むブックマーク

リオ・オリンピックでは、日本の卓球が男女とも活躍しました。福原愛選手や伊藤美誠選手が幼少の頃からハードトレーニングで育成されたことはよく知られています。なので、卓球というのは早い時期から英才・神童達が活躍するもんなんかな? とナントナク思っていました。

この動画を見て驚いたわ。「バンビ」とは小学2年生以下のことだそうです。

D

トラックバック - http://d.hatena.ne.jp/m-hiyama/20160906

2016-09-03 (土)

双模倣(bisimulation)

| 12:23 | 双模倣(bisimulation)を含むブックマーク

状態遷移系の同値性の定義として双模倣(bisimulation)があります。"bisimulation"と一単語だけでgoogle検索すると、血糊を付けた女の子達の歌ばっかりヒットするんですけど。最近じゃなくて2014年3月リリースの曲らしいです。

双模倣を調べたいなら、"bisimulation transition" とか "bisimulation equivalence" とかです。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20160903

2016-08-30 (火)

テンソル積の作り方 2: 双加群の場合、小さい圏の場合

| 12:28 | テンソル積の作り方 2: 双加群の場合、小さい圏の場合を含むブックマーク

昨日の「テンソル積の作り方」は、線形代数の復習という意味合いがもちろんありますが、別な目的もあります。色々なものに対してテンソル積を考えたいことがあるんです。なので、一般的なテンソル積のフレームワークがあれば便利だろうと思ったわけです。

テンソル積で難しいのは、実際のテンソル積を構成するところです。しかし、事前に「テンソル積とは何であるべきか」をハッキリさせておかないと構成にかかれません。また、「テンソル積は作れそうにない、無理だ」と判断するにもテンソル積の要件が必要です。

ベクトル空間のテンソル積と同様に定義できるテンソル積の例を2つ出します。2つの例において、テンソル積として期待する条件は述べますが、その存在は示しません(よく分かってないので示せません)。これらのテンソル積は、実際に欲しいものなんですが、その背景と動機も今日は触れません。

可換環上の双加群テンソル

P, Q, Rが可換とは限らない環(多元環)とします。Pが左から、Qが右から作用する両側加群を、(P, Q)-双加群と呼びます。Aが(P, Q)-双加群、Bが(Q, R)-双加群のとき、A¥otimesQBと書かれるテンソル積を定義しましょう。

M2([A, B], X)は、2-複線形写像の集合とします; 基本的にはベクトル空間のときと同じですが、非可換環上の双加群なので、多少複雑になります。u:A×B→X が2-複線形写像である(つまり、u∈M2([A, B], X))とは、次のことです。以下で、P左作用、R右作用を「・」で表します。

  • Xは(P, R)-双加群である。
  • 任意の b∈B に対して、
    • u(x + x', b) = u(x, b) + u(x', b)
    • p∈P として、u(p・x, b) = p・u(x, b)
  • 任意の a∈A に対して、
    • u(a, y + y') = u(a, y) + u(a, y')
    • r∈R として、u(a, y・r) = (a, y)・r
  • q∈Q として、u(x・q, y) = u(x, q・y) (Qによる左作用、右作用も「・」)

ベクトル空間のときと同じように圏M2[A, B]を定義します。この圏の射は、(P, R)-双加群の線形写像 f:X→Y であって、2-複線形写像u, vに対して u;f = v を満たすものです。

圏M2[A, B]の始対象 t:A×B→T があるとき、T = A¥otimesQB と定義します。A×Bからの任意の2-複線形写像は、A¥otimesQBからの線形写像で表現可能となります。

(P, R)-双加群XとYのあいだの線形写像の全体をL(X, Y)と書くことにすれば、次の同型が成立します。

  • M2([A, B], X) ¥stackrel{¥sim}{=} L(A¥otimesQB, X)

係数環P, Q, Rを省略せずに添えたほうが分かりやすいかもしれません。

  • M2(P, Q, R)([A, B], X) ¥stackrel{¥sim}{=} LP,R(A¥otimesQB, X)

圏のテンソル

小さな圏C, Dに対して、それらのテンソルC¥otimesDを考えたいと思います。ここで考えるテンソル積は、アーベル圏のドリーニュ・テンソル積とは異なります。

反射的有向グラフの圏をGraphと書きます。小さい圏Cの結合を忘れ、有向グラフ構造と恒等射だけにしたものをU(C)とすると、忘却関手 U:CatGraph が定義できます。

忘却関手UによるCat(C, D)の像をFunc(C, D)と書くことにします。Func(C, D)はCat(C, D)と事実上同じ集合ですが、Func(C, D)⊆Graph(U(C), U(D)) です。Func(C, D)の要素は、関手的グラフ写像(functorial graph-map)と呼べます。

次に、MFunc2([C, D], X)を定義します。これは、2-複関手的グラフ写像(2-multifunctorial graph-map)の集合です。その定義は、ベクトル空間の2-複線形写像を定義したときと同じ考えに従います。

F:U(C)×U(D)→U(X) in Graph が2-複関手的グラフ写像だとは、A∈|C| を固定しての F(A, -):U(D)→U(X) と、B∈|D|を固定しての F(-, B):U(C)→U(X) がいずれも関手的グラフ写像になることです。

圏MFunc2[C, D]もベクトル空間のときと同じ要領で定義して、その圏の始対象として C×DC¥otimesD が定義されます。

以上のように、ベクトル空間のときの枠組を引き写して、圏のテンソル積の要件を定義できます。さて、この要件を満たすテンソル積を実際に構成可能でしょうか? 僕には絶望的に思えます。このままではとても無理そうです。しかし、条件を付けたり細工をすれば、テンソル積相当の圏を構成できる可能性は残っています。

「ダメだから諦めよう」とか「別な工夫をしてみよう」という判断も、要件・仕様が明確になってハジメテ出来ることなので、“テンソル積のフレームワーク”は無駄ではないと思います。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20160830

2016-08-29 (月)

テンソル積の作り方

| 13:34 | テンソル積の作り方を含むブックマーク

モノイド圏のモノイド積を“テンソル積”と呼ぶことがあります。この意味のテンソル積は最初から「在る」もので、「作る」ものではありません。では、最初はテンソル積がないのだけど、頑張って「作る」とき、どんな作り方をするのでしょうか?

単に「作る」と言っても曖昧なので、ベクトル空間のテンソル積を事例に、その「作り方」を反省的に眺めてみようと思います。

内容:

  1. ベクトル空間のテンソル積の要件
  2. テンソル積の構成には2つの圏が必要
  3. 「双」はやめる
  4. LとM2の定義
  5. 圏M2[A, B]と、AとBのテンソル
  6. 射のテンソル
  7. インデックス付き圏のセクションとしてのテンソル
  8. モノイド圏の構成

ベクトル空間のテンソル積の要件

ベクトル空間と線形写像の圏をVectとします。スカラー体(係数体)は何でもいいので、特に明示しません。今、A, B∈|Vect| に対してA¥otimesBを定義したいわけです。ベクトル空間のテンソル積A¥otimesBは、A×B上の双線形写像を線形化するような空間として規定されます。

f:A×B→X が双線形写像(bilinear map)だとは、2変数のどちらか一方を固定したとき、もう一方の変数に関して線形になることです。A×B上のXに値を取る双線形写像の全体をBL([A, B], X)と書くことにします。それと、AからBへの線形写像の全体はL(A, B)(Vect(A, B)と同じ)とも書きます。そのとき我々は、次の同型を期待します。

  • BL([A, B], X) ¥stackrel{¥sim}{=} L(A¥otimesB, X)

この同型が成立するようにA¥otimesBを決めましょう、と言うことです。

テンソル積の構成には2つの圏が必要

「ベクトル空間のテンソル積はなんか難しいな」とは思っていましたが、改めて作る手順を確認してみると、「あー、やっぱりコリャ難しいわ」と感じます。

例えば、ベクトル空間の直和A¥oplusBに関して言えば、A¥oplusBは圏Vectの双積(圏論的な直積かつ直和)なので、圏Vect内で自己完結する定義ができます。しかし、テンソル積に関しては、圏Vectだけでは定義ができません。なぜなら、途中で双線形写像という概念が出てくるからです。

双線形写像を圏Vectのなかで探しても見つかりません。なにしろ、Vectの射は線形なので、非線形である双線形写像が(線形に退化する双線形写像を除けば)Vect内にあるはずがないのです。

双線形写像の全体であるBL([A, B], X)をどうやって作るのか? いったん、集合圏Setに持っていって作業するしかありません。つまり、忘却関手 U:VectSet を使うのです。A, B, X∈|Vect| に対して、Set(U(A)×U(B), U(X))を考えて、この部分集合としてBL([A, B], X)を構成することになります。

Vectにおけるテンソル積を定義するために、デカルト構造を持った背景圏Setと、Setへの忘却関手を使わざるを得ないのがウザいところです。Vectだけで何とかならないか? とは思いますが、何も思い付きません。諦めて、Setの助けを借りることにします。

「双」はやめる

テンソル積の議論と直接の関係はないのですが、用語法として「双線形写像」を使うのはやめます。ここから先は代わりに、2-複線形写像(2-multilinear map)にします。その理由を以下に述べましょう。

linear map, bilinear map, multilinear mapを一般的な(Vectとは限らない)文脈で使うときは、morphism, bimorphism, multimorphismと言うといいと思います。これを翻訳すると、射、双射、複射ですが、双射だとbijectionと区別できません。非負整数値nに対するn-multimorphismを定義すれば、n = 2 の場合がbimorphismなので、bimorphismの代わりに「2-multimorphism=2-複射」を使えばいいでしょう。

そもそも「双」が無闇に使われ過ぎなんです。→「「余」と「双」の使い方がバラバラ

以下では、BL([A, B], X)の代わりにM2([A, B], X)と書きます。M3([A, B, C], X)なども同様な意味です(今日は使いませんが)。M1([A], X) = L(A, X)、M0([], X) = L(0, X) です。

LとM2の定義

U:VectSet は忘却関手です。U(A), U(f) などを、括弧を省いて UA, Uf とも書きます。A, B∈|Vect| に対して、ホムセットのあいだの写像 UA,B:Vect(A, B)→Set(UA, UB) が定義できます。関手Uは忠実(faithful)なので、UA,Bは単射写像です。UA,Bの像をL(A, B)とします。定義より、L(A, B)⊆Set(UA, UB) で、Vect(A, B) ¥stackrel{¥sim}{=} L(A, B) です。

次に、M2([A, B], X)をSet(UA×UB, UX)の部分集合として定義しましょう。以下の3段落がM2([A, B], X)の定義です。

a∈UA を a:1→UA とみなします。ここで1は単元集合で、Setの特定された終対象(かつ直積の単位)とします。a×idUB:1×UB→UA×UB となりますが、UB ¥stackrel{¥sim}{=} 1×UB なので、a~:UB→UA×UB が定義できます。f∈Set(UA×UB, UX) に対して、結合(合成) (a~;f):UB→UX が作れます。

任意の a:1→UA に対して、(a~;f)∈L(B, X) のとき、fは第2変数に関して偏線形(partially linear)と呼びます。同様に、第1変数に関して偏線形が定義できます。fが第1変数に関しても第2変数に関して偏線形なとき、2-複線形(2-multilinear)と呼びます。3以上のnに関しても同様にn-複線形(n-mulitilinear)が定義できます。1-複線形は単なる線形、0-複線形な写像はゼロベクトルをポイントするだけの写像です。

Set(UA×UB, UX)のなかで2-複線形な写像を集めるとSet(UA×UB, UX)の部分集合ができるので、それをM2([A, B], X)とします。当然に、M2([A, B], X) ⊆ Set(UA×UB, UX) です。

圏M2[A, B]と、AとBのテンソル

次に、圏M2[A, B]を定義します。M2[A, B]の対象は、2-複線形写像 u∈M2([A, B], X) です。ただし、Xは固定してなくて任意のベクトル空間を動かしていいとします。ベクトル空間や集合が対象なのではなくて写像が対象ですから注意してください。u∈M2([A, B], X), v∈M2([A, B], Y) がM2[A, B]の2つの対象のとき、f:u→v in M2[A, B] は、f:X→Y という線形写像であって、次の図式が可換となるものです。

A×B == A×B
u|  v|
 ↓   ↓
 X --f→Y

等式で書けば u;f = v です。射の結合は、線形写像の結合で、恒等射はidXとします。M2[A, B]が圏になることは容易に確認できます。

2つのベクトル空間AとBのテンソルtensor product)とは、圏M2[A, B]の始対象のことです。t:A×B→T がM2[A, B]の始対象としましょう。tは2-複線形写像で、Tはベクトル空間です。始対象であることから、任意の2-複線形写像 u:A×B→X に対して、一意的に f:t→u in M2[A, B] が存在します。これは、f:T→X in Vect が決まることを意味します。

つまり、任意の2-複線形写像 u:A×B→X に対して、線形写像 f:T→X が一意的に対応します。このfが2-複線形写像uの線形化です。そしてTが線形化の定義域となるベクトル空間なので、T = A¥otimesBです。

もっと正確に言うと、圏の始対象が存在しても一意的には決まらないので、特定の始対象を圏から選び出す関数をinitとして、A¥otimesB := init(M2[A, B]) と定義します。T = A¥otimesB の意味は、「Tは選び出された特定の始対象であり、それがA¥otimesBを与える」ということです。t:A×B→T (T = A¥otimesB)は2-複線形写像ですが、t(a, b) = a¥otimesb と書かれます。同じ記号¥otimesを使ってますが、A¥otimesBは構成されたベクトル空間であり、a¥otimesb はt(a, b)の略記です。ベクトル空間としてのテンソル積 T = A¥otimesB と、ベクトルのテンソル積 t(a, b) = a¥otimesb は区別しましょう。

以上の定義が有効であるためには、A, B∈|Vect|に対して、圏M2[A, B]に始対象が存在することを保証する必要があります。存在が分かれば、すべての始対象が同型であるので、適当な一個を選べばいいことになります。実際の線形代数では、始対象を具体的に構成して存在を示しています(ここでは割愛)。

射のテンソル

f:A→A', g:B→B' が線形写像だとします。fとgのテンソル積 f¥otimesg:A¥otimesB→A'¥otimesB' も構成しましょう。

そのためにまず、圏Vectを二乗した圏Vect×Vectを考えます。Vect×Vectの対象は、(A, B), (A', B')のようなベクトル空間のペアで、射は f:A→A', g:B→B' に対する(f, g)のような線形写像のペアです。

  • f:A→A' in Vect, g:B→B' in Vect ⇔ (f, g):(A, B)→(A', B') in Vect×Vect

Vect×Vectの射(f, g)があると、M2[A', B']→M2[A, B] という関手を誘導します。誘導された関手を (f, g)* と書くことにします。その定義は:

  • v∈|M2[A', B']| とは、vが v:UA'×UB'→UX という2-複線形写像であることなので、(f, g)*(v) を (f×g);v とする。

(f, g)*(v) := (f×g);v を変数を使って書くと:

  • ((f, g)*(v))(x, y) := v(f(x), g(y)) (x∈A, y∈B)

vが2-複線形、fとgが線形ならば、v(f(x), g(y)) はA×B上の2-複線形写像となるので、|M2[A', B']|→|M2[A, B]| という写像が定義されました。この対応は、射に対しても拡張できて、全体として関手 M2[A', B']→M2[A, B] となります。この関手を同じ記号を流用して (f, g)*:M2[A', B']→M2[A, B] と書きます。

t':A'×B'→T' が圏M2[A', B']の始対象とします。つまり、T' = A'¥otimesB' です。圏M2[A', B']の始対象t'は、関手(f, g)*を使って圏M2[A, B]に持ってこれます。それは (f, g)*(t'):A×B→T' となります。(f, g)*は、2つの線形写像fとgを使った“引き戻し”です。

圏M2[A, B]にも始対象がありますから、それを t:A×B→T、T = A¥otimesB とします。tは始対象なので、tから(f, g)*(t')への射が一意的に決まります。その唯一の射を f¥otimesg と決めます。定義から f¥otimesg:T→T'、つまり f¥otimesg:A¥otimesB→A'¥otimesB' です。

インデックス付き圏のセクションとしてのテンソル

(A, B)|→M2[A, B] という対応は、実はインデックス付き圏(indexed category)になっています。Vect×Vectの対象に対して、それぞれ圏M2[A, B]が割当てられていて、Vect×Vectの射に対しては関手が(反変に)対応します。(f, g)*を、M2[f, g]:M2[A', B']→M2[A, B] と書けば事情がより明らかになるでしょう。

ベクトル空間のテンソル積は、各ペア(A, B)に対して、(A, B)から生えている圏M2[A, B]内の始対象を1個選ぶような選択関数、別な言い方をするとセクションになっています。射(f, g)に対しても同様に、グロタンディーク平坦化した圏のなかの射f¥otimesgを割当てているので、テンソル積は圏のファイブレーションに対するセクション関手になります。

M2だけでなくM3, M4, … あるいは M0, M1Vectn(n = 0, 1, 2, 3, 4, ...)上のインデックス付き圏になり、始対象を選ぶセクションを定義できます。ちなみに、M0[] ¥stackrel{¥sim}{=} Vect、M1[A] ¥stackrel{¥sim}{=} A/Vect です。A/VectはAのアンダー圏です。

Vect×Vect上にインデックス付き圏を作るなんて随分と技巧的だなー」と思うかも知れませんが、Setの直積(デカルト積)の定義だって似たようなもんです。A, B∈|Set| に対して、両足をA, Bに固定したスパン A←X→B の圏Span[A, B]を考えて、各Span[A, B]ごとに終対象を選んでいくと直積が出来上がります。テンソル積の構成と同じようなもんでしょ。

Vectに限らず、一般的な圏Cと忘却関手(忠実関手)U:CSet があれば、Cに関する2-複射(2-morphism)の集合やインデックス付き関手 M2[-, -]:(C×C)opCAT を定義できます。ファイバーごとに始対象の存在が保証されるなら、始対象セクションとしての“テンソル積”が定義できます。

モノイド圏の構成

今まで述べた方法で、(-)¥otimes(-):Vect×VectVect は作れます。しかし、この対応が二項関手であることさえ確認していません。作り出したテンソル¥otimesが、モノイド圏のモノイド積となることを確認するには次の作業が必要です。

  • ¥otimesが二項関手であることを確認する。これは、¥otimesの交替律(interxchange law)を示すこと。
  • 単位対象として、スカラー体と同型なベクトル空間Iを選んで固定する。
  • 結合律子α、左単位律子λ、右単位律子ρを定義する。
  • α, λ, ρが自然同型であることを確認する。
  • マックレーンの五角形・三角形の可換性が成立することを確認する。

これらの事項が確認できれば、作ったテンソル¥otimesと、関連する構成要素達の組 (Vect, ¥otimes, I, α, λ, ρ)がモノイド圏であると言えます。作った後、目的の仕様を満足するかどうかの検査がけっこう大変です。