Nuprl Definition : pv8_p2_perform

pv8_p2_perform(Cid;Op;RepState;Result;apply_op;eq_Cid) ==
  cmd,state.
   let rstate,slt,proposals,decisions = state
   in let client,cid,ope = cmd in 
      if (zkdecisions.pv8_p2_greater_proposal(Cid;Op;eq_Cid) <slt, cmd> zk)_b
      then <<rstate, slt + 1, proposals, decisions>, {}>
      else let next,result = apply_op ope rstate 
           in let new_state = <next, slt + 1, proposals, decisions> in
                  <new_state, {pv8_p2_response'send(Cid;Result) client <cid, result>}>
      fi   


Definitions occuring in Statement :  pv8_p2_response'send: pv8_p2_response'send(Cid;Result),  pv8_p2_greater_proposal: pv8_p2_greater_proposal(Cid;Op;eq_Cid),  ifthenelse: if b then t else f fi ,  let: let,  spreadn: spread4,  spreadn: spread3,  apply: f a,  lambda: x.A[x],  spread: spread def,  pair: <a, b>,  add: n + m,  natural_number: $n,  single-bag: {x},  empty-bag: {},  bl-exists: (xL.P[x])_b
FDL editor aliases :  pv8_p2_perform pv8_p2_perform
pv8\_p2\_perform(Cid;Op;RepState;Result;apply$_{op}$;eq$_{Cid}\mbackslash{}ff2\000C4)  ==
    \mlambda{}cmd,state.
      let  rstate,slt,proposals,decisions  =  state
      in  let  client,cid,ope  =  cmd  in 
            if  (\mexists{}zk\mmember{}decisions.pv8\_p2\_greater\_proposal(Cid;Op;eq$_{Cid}$)  <slt,  cmd>  zk\000C)\_b
            then  <<rstate,  slt  +  1,  proposals,  decisions>,  \{\}>
            else  let  next,result  =  apply$_{op}$  ope  rstate 
                      in  let  new$_{state}$  =  <next,  slt  +  1,  proposals,  decisions>  in
                                    <new$_{state}$,  \{pv8\_p2\_response'send(Cid;Result)  client  <cid,\000C  result>\}>
            fi     


Date html generated: 2012_02_20-PM-07_40_08
Last ObjectModification: 2012_02_06-PM-03_07_22

Home Index