Nuprl Definition : process-ordered-message

See this comment: ordered message buffers⋅
process-ordered-message(nL;km) ==
  let n,L = nL 
  in let k,m = km 
     in if (n) < (k)
           then eval L' = eval_list(insert-ordered-message(L;km)) in
                <[], n, L'>
           else if (k) < (n)
                   then <[], n, L>
                   else eval sn = n + 1 in
                        if null(L) ∨bsn <z fst(hd(L))
                        then <[km], sn, L>
                        else let L1,L2 = split-maximal-consecutive(λp.(fst(p));L) 
                             in eval n' = fst(last(L1)) in
                                <[km / L1], n', L2>
                        fi 


Definitions occuring in Statement :  split-maximal-consecutive: split-maximal-consecutive(g;L),  insert-ordered-message: insert-ordered-message(L;x),  last: last(L),  hd: hd(l),  null: null(as),  eval_list: eval_list(t),  cons: [a / b],  nil: [],  bor: p ∨bq,  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  pi1: fst(t),  less: if (a) < (b)  then c  else d,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  add: n + m,  natural_number: $n
FDL editor aliases :  process-ordered-message
Latex:
process-ordered-message(nL;km)  ==
    let  n,L  =  nL 
    in  let  k,m  =  km 
          in  if  (n)  <  (k)
                      then  eval  L'  =  eval\_list(insert-ordered-message(L;km))  in
                                <[],  n,  L'>
                      else  if  (k)  <  (n)
                                      then  <[],  n,  L>
                                      else  eval  sn  =  n  +  1  in
                                                if  null(L)  \mvee{}\msubb{}sn  <z  fst(hd(L))
                                                then  <[km],  sn,  L>
                                                else  let  L1,L2  =  split-maximal-consecutive(\mlambda{}p.(fst(p));L) 
                                                          in  eval  n'  =  fst(last(L1))  in
                                                                <[km  /  L1],  n',  L2>
                                                fi 


Date html generated: 2015_07_23-PM-00_28_01
Last ObjectModification: 2014_07_23-PM-01_27_11

Home Index