Nuprl Definition : consensus-rcvs-to-consensus-events

consensus-rcvs-to-consensus-events(f;t;v0;L) ==
  accumulate (with value p and list item r):
   let X,Y = p 
   in let b,i,as,vs,v = accumulate (with value s and list item r):
                         consensus-accum-num((2 * t) + 1;f;s;r)
                        over list:
                          Y @ [r]
                        with starting value:
                         <ff, 0, [], [], v0>) in <X
                                                  @ if rcv-vote?(r)
                                                    then let a,i,v = rcvd-vote(r) in 
                                                         [consensus-message(a;i + 1;inl <i, v>)]
                                                    else []
                                                    fi 
                                                  @ if b
                                                    then if null(as)
                                                         then [Archive(v); NextInning]
                                                         else map(λn.NextInning;upto(i - 1 
                                                                  - ||filter(λx.is-inning-event(x);X)||))
                                                              @ [Archive(v); NextInning]
                                                         fi 
                                                    else []
                                                    fi 
                                                 , Y @ [r]
                                                 >
  over list:
    L
  with starting value:
   <[], []>)


Definitions occuring in Statement :  consensus-accum-num: consensus-accum-num(num;f;s;r),  rcvd-vote: rcvd-vote(x),  rcv-vote?: rcv-vote?(x),  consensus-message: consensus-message(b;i;z),  archive-event: Archive(v),  is-inning-event: is-inning-event(x),  inning-event: NextInning,  upto: upto(n),  filter: filter(P;l),  map: map(f;as),  length: ||as||,  append: as @ bs,  null: null(as),  list_accum: list_accum,  cons: [a / b],  nil: [],  ifthenelse: if b then t else f fi ,  bfalse: ff,  spreadn: let a,b,c,d,e = u in v[a; b; c; d; e],  spreadn: spread3,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  inl: inl x,  multiply: n * m,  subtract: n - m,  add: n + m,  natural_number: $n
FDL editor aliases :  consensus-rcvs-to-consensus-events
consensus-rcvs-to-consensus-events(f;t;v0;L)  ==
    accumulate  (with  value  p  and  list  item  r):
      let  X,Y  =  p 
      in  let  b,i,as,vs,v  =  accumulate  (with  value  s  and  list  item  r):
                                                  consensus-accum-num((2  *  t)  +  1;f;s;r)
                                                over  list:
                                                    Y  @  [r]
                                                with  starting  value:
                                                  <ff,  0,  [],  [],  v0>)  in  <X
                                                                                                    @  if  rcv-vote?(r)
                                                                                                        then  let  a,i,v  =  rcvd-vote(r)  in 
                                                                                                                  [consensus-message(a;i  +  1;inl  <i,  v>)]
                                                                                                        else  []
                                                                                                        fi 
                                                                                                    @  if  b
                                                                                                        then  if  null(as)
                                                                                                                  then  [Archive(v);  NextInning]
                                                                                                                  else  map(\mlambda{}n.NextInning;upto(i  -  1 
                                                                                                                                    -  ||filter(\mlambda{}x.is-inning-event(x);
                                                                                                                                                          X)||))
                                                                                                                            @  [Archive(v);  NextInning]
                                                                                                                  fi 
                                                                                                        else  []
                                                                                                        fi 
                                                                                                  ,  Y  @  [r]
                                                                                                  >
    over  list:
        L
    with  starting  value:
      <[],  []>)


Date html generated: 2015_07_17-AM-11_54_29
Last ObjectModification: 2012_02_25-AM-11_54_53

Home Index