並行システム論 4/17

黒板の先生の文字が読みにくい…教科書に書いてあることも多いから無理してメモらなくても良いかなあ。

length
L1: #<> = 0
L2: #<x> = 1
L3: #<s^t> = #<s> + #<t>
L4: #<t↑(A∪B)> = #<t↑A> + #<t↑B> - #<t↑(A∪B)>
L5: s≦t ⇒ #s≦#t
L6: #tn = n*(#t)

Frequency of occurence of action
S↓x = #(S↑{x})

ex) S = <abcada>
    S↓a = #(<abcada>↑{a})
         = #(<aaa>) = 3

--

Semantics of a process
Trace: {process}→{trace}

L1: Trace(STOP) = {<>}
L2: Trace(c→P) = {t | t=<> ∨ t_0=c ∧ t'∈Trace(P)}
                = {<>}∪{<c>^t | t ∈ Trace(P)}

L3: Trace(c→P|d→Q)
     = {t | t=<> ∨ (t_0=c ∧ t'∈Trace(P))
                 ∨ t_0 = d ∧ t'∈Trace(Q)}

L4: Trace(x:B→P(x)) = {t | t=<> ∨ t_0∈B ∧ t'∈Trace(P(t_0))}
        ↑
    Finite set of actions

L5: Trace(uX:A.F(X)) = Trace(STOP)∪Trace(F(STOP))∪Trace(F(F(STOP)))∪…
                     = ∪_m Trace(Fn(STOP))
    X = F(X)

ex: αM_A = A
      M_A = (x:A → M_A)
      M_A = uX:A F(X)
        where F(X) = (x:A → X)
    Trace(M_A) = A* ....(1)
    A = {a,b}, A* = {<>,<a>,<b>,<aa>,<ab>
                     <ba>,<bb>,<aaa>,<aab>,...}

(proof of (1))
 A* = ∪_n≧0 {s | s∈A* ∧ #s≦n}

We prove the following
∀n(Trace(Fn(STOP_A)) = {s|s∈A* ∧ #s≦n})

i) n=0
(L.H =) Trace(STOP_A) = {<>} (= R.H)

ii) Trace(Fn+1(STOP_A))
   = Trace(x:A → Fn(STOP_A))
   = {t|t=<> ∨ (t_0∈A ∧ t'∈Trace(Fn(STOP_A)))}
   = {t|t=<> ∨ (t_0∈A ∧ t'∈{s|s∈A* ∧ #s≦n})}
   = {t|t=<> ∨ (t_0∈A ∧ t'∈A ∧ #t≦n+1)}
   = {t|t=<> ∨ #t≦n+1}
   = {s|s=<> ∨ #s≦n+1}

∀P(<>∈Trace(P))
∀P∀s∀t(s^t∈Trace(P) ⇒ S∈Trace(P))...Q2
∀P(Trace(P)⊆(αP)*)...Q1

--

after (process contruction function)
s∈Trace(P)
P/s 軌跡sに記録されている全ての動作を行ったPが
    この後とる振る舞いと同じ動作をするプロセス

L1: P/<> = P
L2: P/s^t = (P/s)/t
L3: (s:B → P(x))/<c> = P(c)
L3A: (c→P)/<c> = P
L4: Trace(P/s) = {t|s^t∈Trace(P)}
                  where s∈Trace(P)

ex (1) ∀s∈Trace(P)   P/s≠STOP
   (2) cyclicety

--

Renaming function f.

f  : A->B    f*(s↑A)≠f*(s)↑f(A)...Q3
f* : A*->B*  f(A) = {f(a)|a∈A}

Interleaving.
L1: <>int.l<t,s> ... if t=<>, s=<>
L2: s int.l<t,u> <=> s int.l <u,t>
                      a   c
                      :   :
                      b   d
L3: .....略

--

v  it appears in the end of trace
   it shows the process has property stoped

s;t              s;{v} = s(¬(<v>∈(s)'))
￣￣

L1: s;t = s if s does not contain v
L2: s^<v>;t=...
L3: ...........略