Nuprl Definition : nysiad-inst-msg-fun
nysiad-inst-msg-fun(oarcasthdr;orderhdr;orderedhdr;deliverhdr;readyhdr;add2baghdr;addwaitinghdr;...;...;...;...;M;mf) ==
λhdr.if name_eq(hdr;oarcasthdr) then M
if name_eq(hdr;orderhdr) then Id × ℤ × M
if name_eq(hdr;orderedhdr) then Id × Id × ℤ × M
if name_eq(hdr;deliverhdr) then Id × ℤ × M
if name_eq(hdr;readyhdr) then Id
if name_eq(hdr;add2baghdr) then Message(mf) × Id? × Id
if name_eq(hdr;addwaitinghdr) then Message(mf) × Id? × Id
if name_eq(hdr;adeliverhdr) then Id × Message(mf)
if name_eq(hdr;inputmsghdr) then Message(mf) × Id? × Id
if name_eq(hdr;tooarcasthdr) then Message(mf) × Id? × Id
if name_eq(hdr;kdeliverhdr) then Message(mf) × Id? × Id
else Void
fi
Definitions occuring in Statement :
Message: Message(f),
Id: Id,
name_eq: name_eq(x;y),
ifthenelse: if b then t else f fi ,
unit: Unit,
lambda: λx.A[x],
product: x:A × B[x],
union: left + right,
int: ℤ,
void: Void
FDL editor aliases :
nysiad-inst-msg-fun
Latex:
nysiad-inst-msg-fun(oarcasthdr;orderhdr;orderedhdr;deliverhdr;...;...;...;...;...;...;...;M;mf) ==
\mlambda{}hdr.if name\_eq(hdr;oarcasthdr) then M
if name\_eq(hdr;orderhdr) then Id \mtimes{} \mBbbZ{} \mtimes{} M
if name\_eq(hdr;orderedhdr) then Id \mtimes{} Id \mtimes{} \mBbbZ{} \mtimes{} M
if name\_eq(hdr;deliverhdr) then Id \mtimes{} \mBbbZ{} \mtimes{} M
if name\_eq(hdr;readyhdr) then Id
if name\_eq(hdr;add2baghdr) then Message(mf) \mtimes{} Id? \mtimes{} Id
if name\_eq(hdr;addwaitinghdr) then Message(mf) \mtimes{} Id? \mtimes{} Id
if name\_eq(hdr;adeliverhdr) then Id \mtimes{} Message(mf)
if name\_eq(hdr;inputmsghdr) then Message(mf) \mtimes{} Id? \mtimes{} Id
if name\_eq(hdr;tooarcasthdr) then Message(mf) \mtimes{} Id? \mtimes{} Id
if name\_eq(hdr;kdeliverhdr) then Message(mf) \mtimes{} Id? \mtimes{} Id
else Void
fi
Date html generated:
2015_07_23-PM-03_49_14
Last ObjectModification:
2014_08_08-PM-06_08_48
Home
Index