イベントのR構造と状態空間
あたらめて、msched -- meeting scheduler ね。
ラベルLを固定する。ボトム⊥を入れて、Lはミート半束の構造を持つ。アフィン時間Tの区間の全体も共通部分でミート半束。これらの直積をとり、ボトムの部分をつぶす（つぶし方は複数ある）とまたミート半束。こうやって作ったイベントの半束(Ev, ∧, Θ) が舞台。物理で言えば配位空間。∧から導かれる順序は⊆で表す。
もう少しイベント間に定義できる基本関係：
- a∧b が空である ⇔ aとbは分離している、離れている
- a∧b が点イベント ⇔ aとbは隣接している、接触している
- a∧b が空か点 ⇔ aとbは無衝突である。
2つのイベントが衝突していればダブルブッキング。通常は不整合とするが、不整合もとりあえずは許す。不整合も「普通に」扱わないとダメだってことは、文書のvalidationでさんざんに経験したこと。不整合を拒絶するアプローチはどうせ破綻する。そもそも「不整合」という概念や用語を入れるべきじゃないかもしれない。
相対イベント
a, bがイベントで、a⊆b であるとき、組(a, b)を相対イベントと呼ぶ。「bのなかで起きたa」という意味。あるいは、bがタイムコンテナで、「bのなかでアロケートされたa」という感じか。bはaの親イベントってことになる。
任意のイベントaを相対イベントとみなす方法は2つある。
- (a, a)とする。
- a = (A, i) として、(A, T)を親とする。
イベントの和
a = (A, i), b = (B, j)が隣接しているとき、隣接の定義から A = B となる。iとjの集合論的合併は再び時区間になる。(A, i∪j) を、aとbの和と定義する。
イベントの族Kが次の条件を満たすとする。
- a, b∈K、a≠b なら、aとbは無衝突である。
- a∈K に対して、aと隣接するイベントb∈Eが存在する。
上の条件を満たす族に対しては、和（総和）が定義できる。よって、そのような族を総和可能（summable）と呼ぶことにする。
イベントの族Kが総和可能のとき、その和を ΣK と書く。
原子イベントと有効イベント
AE⊆Ev を天下りに与えて、AEの元を原子イベントと呼ぶ。次の条件を入れておく。
- 空イベント、点イベントは原子イベントには入らない。原子は必ず拡がりを持つのだ！
- 2つの異なる原子イベントは無衝突である。接触は許す、貫入はダメ。
与えられたAE上で、(A, i)が有効イベントとは、「原子イベント、または有限個の原子イベントの和として書けること」。定義より、空イベントや点イベントは有効イベントになりえない。
R構造
ラベル集合Lと原子イベントの集合AEを固定する。すると、その上で有効イベントの集合EEが確定する。Lとは別にラベルの集合Rを用意する。Rは何でもいいが、通常は有限集合である。
イベントのR構造、またはRイベント構造は次のように定義される。
- 有限な台集合D⊆EE。
- r∈Rに対してD上の二項関係が対応している。
特殊なケースとして台集合Dは空であってもよい。Rは空ではないと仮定する（最低でも1つの記号を含む）。R構造は、Dを頂点集合とする、辺ラベル付き有向グラフとなる。r∈Rを固定すると、単純有向グラフになる。R構造はRグラフと言ってもいいだろう。
R構造は、ある瞬間での状態データと考えるので、我々の考察の領域は、Rを固定してすべてのR構造からなる集合である。システムの状態遷移はR構造の空間のなかで軌跡を描く。これから、R構造の空間＝状態空間に対するオペレーションを定義していく。オペレーションはアトミック（トランザクション）である。
オペレーション＝コマンドを定義するとは、
- コマンドの事前条件をR構造の言葉で記述する。
- コマンドの効果をR構造の言葉で記述する。
- 状態に対する不変条件（述語）を記述する。
コマンドの定義とかはまた次。
