Nuprl Definition : processComm
processComm(l_comm;l_choose) ==
RecProcess(<⊗, [], l_comm, ff, 0>;cSt,piD.if pDVguards?(piD) then Comm-next-guards(l_comm;piD;cSt)
if pDVselex?(piD) then Comm-next-selex(l_comm;piD;cSt)
if pDVcontinue?(piD) then Comm-next-continue(l_comm;l_choose;piD;cSt)
else <cSt, make-lg([])>
fi )
Definitions occuring in Statement :
Comm-next-continue: Comm-next-continue(l_comm;l_choose;piD;cSt),
Comm-next-selex: Comm-next-selex(l_comm;piD;cSt),
Comm-next-guards: Comm-next-guards(l_comm;piD;cSt),
pDVselex?: pDVselex?(x),
pDVcontinue?: pDVcontinue?(x),
pDVguards?: pDVguards?(x),
make-lg: make-lg(L),
rec-process: RecProcess(s0;s,m.next[s; m]),
fpf-empty: ⊗,
nil: [],
ifthenelse: if b then t else f fi ,
bfalse: ff,
pair: <a, b>,
natural_number: $n
FDL editor aliases :
processComm
Latex:
processComm(l$_{comm}$;l$_{choose}$) ==
RecProcess(<\motimes{}, [], l$_{comm}$, ff, 0>cSt,piD.if pDVguards?(piD) then Comm-nex\000Ct-guards(l$_{comm}$;piD;cSt)
if pDVselex?(piD) then Comm-next-selex(l$_{comm}$;piD;cSt)
if pDVcontinue?(piD) then Comm-next-continue(l$_{comm}$;l$_{choose\000C}$;piD;cSt)
else <cSt, make-lg([])>
fi )
Date html generated:
2015_07_23-AM-11_58_56
Last ObjectModification:
2012_08_30-PM-01_49_41
Home
Index