Information Technology Reference
In-Depth Information
SndM
−−→
j
[
C
[
v
]
q
]
◦
h
[
d
r
:
{sd,
i
,
v
}
]
∗
i
!
v
j
[
C
[
i
!
v
]
q
]
◦
h
[
d
r
]
∗
fv(
v
)
=∅
RcvM
−−→
i
[
e
q
:
v
]
◦
h
[
d
r
:
{rv,
i
,
v
}
]
∗
i
?
v
i
[
e
q
]
◦
h
[
d
r
]
∗
m
∈{•,∗}
m
∈{•,∗}
fv(
v
)
=∅
SndU
RcvU
i
!
v
−−→
j
[
C
[
v
]
q
]
m
i
?
v
−−→
i
[
e
q
:
v
]
m
j
[
C
[
i
!
v
]
q
]
m
i
[
e
q
]
m
(
h
)
i
!
v
−−−−→
B
A
γ
j
obj(
γ
)
∪
sbj(
γ
)
i
j
,
j
∈
sbj
(
h
)
i
!
v
−→
B
(
ν
j
)
A
γ
A
Scp
Opn
h
)
i
!
v
−−−−−→
B
(
j
,
−→
(
ν
j
)
B
(
ν
j
)
A
Com
τ
−→
j
[
C
[
v
]
q
]
m
j
[
C
[
i
!
v
]
q
]
m
i
[
e
q
]
n
i
[
e
q
:
v
]
n
A
γ
−→
A
A
B
γ
Par
obj(
γ
)
∩
fId(
B
)
= ∅
−→
A
B
mtch(
g
,
v
)
=
e
Rd1
τ
−→
i
[
C
(
v
:
q
)]
m
C
q
]
m
i
[
[
rcv
g
end
]
[
e
]
τ
−→
i
[
C
[
e
]
r
]
m
i
[
C
[
rcv
g
end
]
q
]
m
mtch(
g
,
v
)
=⊥
Rd2
τ
−→
(
v
:
q
)]
m
(
v
:
r
)]
m
i
[
C
[
rcv
g
end
]
i
[
C
[
e
]
mtch(
g
,
v
)
=
e
mtch(
g
,
v
)
=⊥
Cs1
Cs2
τ
−→
τ
−→
[
case
v
of
g
end
]]
m
[
e
]]
m
[
case
v
of
g
end
]]
m
[
exit
]]
m
i
[
C
i
[
C
i
[
C
i
[
C
v
exit
i
[
C
[
x
=
v
,
e
]]
m
Ass
Ext
τ
−→
i
[
C
[
e
{
τ
−→
i
[
C
[
exit
]]
m
v
/
x
}
]]
m
i
[
C
[
x
=exit,
e
]]
m
App
Slf
τ
−→
i
[
C
[
e
{
μ
y
.λ
x
.
e
τ
−→
i
[
C
[
i
]]
m
i
[
C
[
μ
y
.λ
x
.
e
(
v
)]]
m
v
/
x
}
]]
m
i
[
C
[
self
]]
m
/
y
}{
A
≡
A
γ
(
m
=◦ =
n
)or(
n
=•
)
i
[
C
[
spw
e
]
q
]
m
−→
B
≡
B
A
γ
Spw
Str
−→
(
ν
j
)
i
[
C
[
j
]
q
]
m
j
[
e
]
n
τ
−→
B
A
≡
B
A
C
≡
B
C
sCom
sAss
sCtxP
A
B
≡
B
A
(
A
B
)
C
≡
A
(
B
C
)
i
fId(
A
)
A
(
ν
i
)
B
≡
(
ν
i
)
B
A
A
≡
B
sExt
sSwp
sCtxS
(
ν
i
)(
ν
j
)
A
≡
(
ν
j
)(
ν
i
)
A
(
ν
i
)
A
≡
(
ν
i
)
B
Fig. 2.
Erlang Semantics for Actor Systems
