![アクターコンフィグレーションの例
10
a b
1 (メッセージ)
2つのアクターaとbが存在しており、
アクターaへ1というメッセージが配送中
[ 1]a , [ 2]b || a 1](https://image.slidesharecdn.com/actormodel-180202124812/85/-10-320.jpg)
![拡張ラムダ計算の簡約規則
13
x.e(v) e{x/v}
f(v1, . . . , vn) v f F, v = [[f]](v1, . . . , v2)
br(true, e, ) e
br(false, , e) e
1st
(pr(v, )) v
2nd
(pr( , v)) v
letrec x = v in e e{x/v{x/(letrec x = v in v)}}](https://image.slidesharecdn.com/actormodel-180202124812/85/-13-320.jpg)
![操作的意味論
14
e e
, [R e ]a || ?
[fun:a]
, [R e ]a || ?
, [R new(b) ]a || ?
[new:a,a ]
, [R a ]a, [ready(b)]a || ? a
, [R send(a , v) ] || ?
[snd:a]
, [R nil ]a || ? { a v }
, [R ready(b) ]a || { a v } ?
[rcv:a,v]
, [b(v)]a || ?](https://image.slidesharecdn.com/actormodel-180202124812/85/-14-320.jpg)
![簡約の例
15
a b
10
[ ready(e1) ]a, [seq( , ready(e2)) send(a, 10)) ]b ||
[snd:a]
[ ready(e1) ]a, [seq( , ready(e2)) nil) ]b || a 10
[ ready(e1) ]a, [ ready(e2) ]b || a 10
[rcv:a,10]
[ e1(10) ]a, [ ready(e2) ]b ||
（seqの箇所は?部省略）](https://image.slidesharecdn.com/actormodel-180202124812/85/-15-320.jpg)
![計算?
（computation tree）
16
κ0
κ1 κ1?
κ2 κ2? κ2??
κ3
計算?の例
l1
( ) n N
[ i
li+1
i+1|i < n] = 0 N
l1?
l2 l2? l2??
l3
N = {0, 1, 1 , 2, 2 , 2 , 3}
0 < 1, 0 < 1 , 1 < 2, 1 < 2 , 1 < 2 , 2 < 3
(computation sequence )
(computation path)
計算列
計算路
( )](https://image.slidesharecdn.com/actormodel-180202124812/85/-16-320.jpg)
![公平性
17
l
l
[rcv : a, v]
a
( ) = [ i
li+1
i+1|i < ]
( ) F( )](https://image.slidesharecdn.com/actormodel-180202124812/85/-17-320.jpg)
アクターモデル
- 2. アクターモデルとは ? 並?計算モデルの?つ ? 1973年にCarl Hewittが発明 ? アクターと呼ばれるプロセス同?が通信をしあって計算を?う ? 計算能?はラムダ計算と等価（チューリング完全） ? プログラミング?語 ? Erlang, Scala/Akka 2 アクターA アクターB メッセージ
- 3. π計算との違い 3 通信の同期?法 通信?法 メモリモデル π計算 同期通信 チャネルベース通信 共有メモリ アクターモデル ?同期通信 直接通信 分散メモリ
- 5. 構? 5 ? 注釈 ? アトムとはde?ne定数のようなもの ? ペアのpr(1, 2)は、タプルの(1, 2)のようなもの ? ispr?はペアかどうかを検査する関数 ? 1st, 2ndは、ペアの1番目、2番目の要素を取得す る関数 A = {true, false, nil, . . . } N = {0, 1, 2, . . . } X = {x, y, z, . . . } F = {+, , =, ispr?, 1st , 2nd , . . . } V ::= A | N | X | X.E | pr(V, V) E ::= V | pr(E, E) | E(E) | F(E, . . . , E) | br(E, E, E) | letrec X = E in E | send(E, E) | new(E) | ready(E)
- 6. 糖?構? 6 let x = e1 in e2 x.e2(e1) seq(e1, e2) let z = e1 in e2 z seq(e1, . . . , en) seq(e1, seq(e2, . . . , seq(en 1, en)) . . . ) n 3 if(e1, e2, e3) br(e1, z.e2, z.e3)(nil) z rec(f) x.f( y.x(x)(y))( x.f( y.x(x)(y))) ? 注釈 ? let x = 1, y = 2 in e というように、複数定義も可能 ? この場合は、λy.λx.e(2)(1) と等価 ? rec(f)はZコンビネータ（不動点コンビネータ）
- 7. 束縛変数と?由変数 ? ラムダ抽象と、letrec式のみが束縛 ? その他の変数は?由変数 7 x.E E E x letrec x = E1 in E2 E1, E2
- 8. 操作的意味論 ? アクターコンフィグレーション ? 各アクターの状態と、メッセージの集合 ? アクターモデルの操作的意味論 ? アクターコンフィグレーションからアクターコンフィグレーションへの 遷移について規定したもの ? ラベル付き状態遷移 8
- 9. アクターコンフィグレーション 9 || ? ? a a v v
- 10. アクターコンフィグレーションの例 10 a b 1 (メッセージ) 2つのアクターaとbが存在しており、 アクターaへ1というメッセージが配送中 [ 1]a , [ 2]b || a 1
- 11. 簡約コンテキスト 11 e e = R e R e send(new(e), 10) = send( , 10) new(e)
- 12. 簡約可能な式と簡約コンテキストの構? 12 Er ::= V(V) | F(V, . . . , V) | br(V, E, E) | letrec X = V in E | send(V, V) | new(V) | ready(V) R ::= Hole | pr(V, R) | pr(R, E) | V(R) | R(E) | F(V, . . . , V, R, E, . . . , E) | br(R, E, E) | letrec X = R in E | send(V, R) | send(R, E) | new(R) | ready(R)
- 13. 拡張ラムダ計算の簡約規則 13 x.e(v) e{x/v} f(v1, . . . , vn) v f F, v = [[f]](v1, . . . , v2) br(true, e, ) e br(false, , e) e 1st (pr(v, )) v 2nd (pr( , v)) v letrec x = v in e e{x/v{x/(letrec x = v in v)}}
- 14. 操作的意味論 14 e e , [R e ]a || ? [fun:a] , [R e ]a || ? , [R new(b) ]a || ? [new:a,a ] , [R a ]a, [ready(b)]a || ? a , [R send(a , v) ] || ? [snd:a] , [R nil ]a || ? { a v } , [R ready(b) ]a || { a v } ? [rcv:a,v] , [b(v)]a || ?
- 15. 簡約の例 15 a b 10 [ ready(e1) ]a, [seq( , ready(e2)) send(a, 10)) ]b || [snd:a] [ ready(e1) ]a, [seq( , ready(e2)) nil) ]b || a 10 [ ready(e1) ]a, [ ready(e2) ]b || a 10 [rcv:a,10] [ e1(10) ]a, [ ready(e2) ]b || （seqの箇所は?部省略）
- 16. 計算? （computation tree） 16 κ0 κ1 κ1? κ2 κ2? κ2?? κ3 計算?の例 l1 ( ) n N [ i li+1 i+1|i < n] = 0 N l1? l2 l2? l2?? l3 N = {0, 1, 1 , 2, 2 , 2 , 3} 0 < 1, 0 < 1 , 1 < 2, 1 < 2 , 1 < 2 , 2 < 3 (computation sequence ) (computation path) 計算列 計算路 ( )
- 17. 公平性 17 l l [rcv : a, v] a ( ) = [ i li+1 i+1|i < ] ( ) F( )
- 19. 例：排他実? 19 sem = rec(λb.λh.λm. if(get?(m), if(h = nil, seq(send(cust(m), true), ready(b(cust(m)))), seq(send(cust(m), false), ready(b(h))), if(release?(m), ready(b(nil)), ready(b(h))))) customer = rec(λb.λself.λs.λm. seq(if(m, seq(/* critical section */, send(s, mkrelease(self))), send(s, mkget(self))), ready(b(self)(s)))) // 補助関数 mkget = λh.pr(true, h) mkrelease = pr(false, nil) get? = λm.if(ispr?(m), 1st(m), false) release? = λm.if(ispr?(m), not(1st(m)), false) cust = λm.2nd(m) // 消費者が2?で実?する例 letrec s = new(sem(nil)), a = new(customer(a)(s)), b = new(customer(b)(s)) in seq(send(a, false), send(b, false))
- 20. EOF 20