Think Stitch
PRINCIPIA  最近の更新


限量子のはなし

SyncStitch は次の5つの演算子について、対応する限量子を持っています。

演算子限量子
altxalt
ndcxndc
seqxseq
parxpar
aparxapar

限量子という言葉は論理学の全称限量子 ∀ や存在限量子 ∃ から取った言葉です。 これが通じるかどうかちょっと不安に感じたので、その説明をしたいと思います。

和の記号 Σ

高校で(総)和の記号 Σ を習いました。

添字を集合 I から選ぶように一般化して、次のようにも書くことができます。

添字を集合で指定すると、足し合わせていく順序が決まりません。 もっとも最初の記号だって、順番が決まっていたわけではありません。 簡単のために I = {1,2,3,...,n} とすると、 前から順番に足したり、

後ろから順番に足したり、

逆順に足したってかまいません。

結果はすべて同じになります。 ただし添字の集合 I が有限の場合だけを考えています。 (無限の場合は、足し合わせる順序を変えると結果が変わることがあります。)

このように足し合わせる順序に依存しない理由は、足し算 + が次の2つの性質を持っているからです。

交換律:
結合律:

見ての通り、足し合わせる順序をひっくり返しても、順序を入れ替えてもかまわないということです。

さらに加えて、足し算には足しても変わらない数 0 があります。 これを単位元といいます。

これのおかげで、I が空集合の場合でも和の記号に意味を持たせることができます。

さらに添字の集合を分割して、2つの和に分けることもできます。 上の規則のおかげで、A = {} や B = {} でもかまいません。 しかし、A と B に共通する要素があってはいけません。 重複して加えることになってしまうからです。 これが条件 A ∩ B = {} のついている理由です。

積の記号 Π

足し算に対する和の記号 Σ と同じように、かけ算に対する積の記号もあります。 これは高校では習いませんけど、ギリシャ文字の π の大文字 Π で表します。

添字を集合で表すことができるのも同じです。

足し算同様、かけ算も交換律、結合律を見たし、単位元 1 を持ちます。

したがって次の規則が成り立ちます。

全称限量子 ∀

全称限量子とはなんかすごい名前ですけど、要は足し算をまとめた記号 Σ を作ったのと同じように、論理学でいう「かつ」をまとめたものです。「かつ」の記号は ∧ で、全称限量子の記号は ∀ です。 意味は次のようになります。

添字とその集合を書く位置が違いますけど、まあ単なる習慣というか流儀の違いだと思います。

かつ ∧ も交換律と結合律を満たし、単位元 true を持ちます。true は真の意味です。

したがって次の規則が成り立ちます。

和や積の場合と違って、A ∩ B = {} の条件がついていません。 なぜかというと、「かつ」は次の法則を満たすからです。

冪等律:

これのおかげで、重複して計算してもかまわないからです。

存在限量子 ∃

存在限量子 ∃ は「または」∨ をまとめて書いたものです。 他のものと同じように交換律、結合律を満たし、単位元 false を持ちます。 さらに「かつ」と同じように、冪等律を満たします。

最大値 max

大小関係のある要素からなる集合 A の中で、いちばん大きいものを次の記号で表すことがありますよね。 ただし A は空集合ではないとします。

いま、2つの要素 a, b のうち、大きい方を次のような演算子で表すことにします。

すると max A は次のように書くことができます。 トーナメントで最大値を求めているということですね。 見ての通り、これについても限量子を定義できそうです。

交換律、結合律、そして冪等律が成り立つことがわかります。

したがって次のような限量子を定義することができるでしょう。

添字の集合を分解する規則も成り立ちます。

しかし、これらの規則には添字の集合が空集合ではないという条件がつきます。 なぜかというと、max には単位元がないからです。

もしマイナス無限大というものがあるとしたら、max の単位元と考えることはできますけど・・・。

最小値 min

最小値 min についても、最大値 max と同様に限量子を定義することができます。

ここまでのまとめ

以上6つの演算子についてまとめると、次のようになります。

演算 交換律 結合律 冪等律 単位元
加算 + × 0
乗算 × × 1
論理積 ∧ true
論理和 ∨ false
max なし(-∞)
min なし(+∞)
  • 交換律と結合律を満たしていれば限量子を定義できます。
  • 冪等律を満たしている場合は、添字の集合を分解するときに重複があってもかまいません。
  • 単位元がある場合には、添字の集合が空集合の場合を定義することができ、限量子の値は単位元になります。

ちょっと余談

最大値 max と 最小値 min の限量子は、演算子の記号を大きくしたものを使いました。 これは合理的だと思いますし、そうしている教科書もあります。 そこで勢い、次のように書いてもいいんじゃないかと思うんですけどね。

前の2つについては、確かにそう書いている教科書もあります。 でも、後の2つは1度しか見たことがありません。 この記号を使っていると自然で、逆に全称限量子 ∀ と「かつ」 ∧ が逆向きであることがとても気になります。 それでも伝統の重さに負けて、これらを使うのはやめました。 (読む人に評判がとても悪かったのです。)

CSP の演算子

SyncStitch の各演算子は CSP の記号では次のように書きます。

各演算子の規則は次の通りです。 演算子の名前の後に書いてある記号は、上の記号のテキスト表現です。

演算 交換律 結合律 冪等律 単位元
alt [] STOP
ndc |~| なし
seq ; × × SKIP
par [|X|] × なし
apar [A||B] × なし

seq 以外は交換律と結合律を満たすので、限量子を定義できます。だたし、SyncStitch では添字を集合ではなくリストで指定します。seq の場合は交換律を満たさないので,演算の順序を保たなければなりません。添字をリストで指定するので,リストと同じ順序で演算するようにしてあります。(2013/12/26 修正)

2つの並行合成については、インターフェイスやアルファベット指定とぶつかるので、添字の指定を上につけてあります。

上の規則の中で、気になる点がいくつかあると思います。

並行合成 (par P Q) は冪等律を満たしません。

なぜかというと、P が非決定性を持つかもしれないからです。 例えば P = (ndc (! a SKIP) (! b SKIP)), X = {a, b} とすると、P はデッドロックしないのに (par X P P) はデッドロックすることがあります。

結合律は自明ではありませんが、まあ、直観的に納得できる範囲かと思います。

問題はアルファベット指定による並行合成の結合律です。 そもそもアルファベット指定による並行合成の結合律を定義していません。 結合の際のアルファベットを決めていないからです。 定義は次の左辺になります。 そして式全体が結合律です。

アルファベット A をしゃべるプロセス P と、アルファベット B をしゃべるプロセス Q を合成したプロセスは、A ∪ B をしゃべるというわけです。 しかし、結合律はおよそ自明とはほど遠いものです。これについては「CSP を知っている人への補足」にまわすことにして、ここでは結果を信じていただくことにします。

以上のように、CSP の演算子は足し算や「かつ」などと同じように交換律(seq 以外)と結合律を満たすので、限量子を定義できるというわけです。 (alt) = STOP, (seq) = SKIP なのに (ndc) や (par X) が定義できないのは、単位元がないからです。

補足

  • ここで説明した限量子については、A Logical Approach to Discrete Math(邦訳:コンピュータのための数学)に詳しく出ています。 前にも紹介したかな?。邦訳が手に入りません (T_T)。
  • alt は交換律を満たすので、(alt P Q) = (alt Q P) です。実際 SyncStitch の Process Explorer は、この2つを同じプロセス(状態)と見なします。 並行合成 par も交換律を満たしますが、Process Explorer は (par X P Q) と (par X Q P) を同じプロセスとは見なしません。 その理由は、プロセス木やプロセス式の表示を定義と同じ順序にして、解析を容易にするためです。 検査ではもちろん同じプロセスとなります。 この選択は状態数を抑えるという意味では不利なので、将来的に変更するかもしれません。
  • 非決定的選択と最小値の記号が同じなのは偶然ではありません。 The Theory and Practice of Concurrency を見てください。
  • 関数型言語の多くは高階関数 fold(の族)を持ってます。 これは限量子とほとんど同じですね。 SyncStitch の限量子と同じく、添字は数学的な集合ではなく、リスト等順序を持ったものが多いと思います。 この場合、結合の順序を決めることができるので、交換律や結合律を満たさない演算に対しても適用することができます。seq はこの例です。
  • 最大値や最小値を扱うプログラムの正当性を考えるときに、±∞ があると考えると証明が簡単になる場合があります。 最大値・最小値だけじゃなくても、比較の問題でも使えることがあります(2分探索とか)。

CSP を知っている人への補足

CSP を知っている人に CSP の話をするというのも変ですけど。

非決定的選択 ndc が単位元を持っていないこと

非決定的選択 ndc が単位元を持っていないことは重要です。 なぜかというと、正当性関係は次のように定義されているからです。

もし Q が単位元だとすると、すべてのプロセスに対して正しい実装ということになります。 そんなプロセスがあるはずはありません。 あったらいいですけど。 ただし、プロセスの「意味」を何とするかで少し結果が変わってきます。 詳しくは Roscoe さんの The Theory and Practice of Concurrency を見てください。

上の関係は、集合の包含関係や論理学の含意でも成り立ちます。 こうすると感じがつかみやすいと思います。

アルファベット指定による並行合成の結合則

アルファベット指定による並行合成の結合則は、表示的意味論を使うと証明することができます。

例えば安定失敗モデルを使うとします。 発散がない場合だけ考えます。 アルファベット指定による並行合成の failures は次のように定義されています。 (例えば Concurrent and Real-time Systems: The CSP Approach を見てください。)

これを使って結合律各辺の failures を計算すると、結果が同じであることを確認できます。 見た目は恐ろしいですけど、結構簡単です。

2013/08/31
2013/12/26 seq が交換律を満たすとなっていた点を修正しました。ご指摘感謝。
© 2013,2014,2015 PRINCIPIA Limited