Nuprl Definition : hdf-buffer

hdf-buffer(X;bs) ==
  mk-hdf(Xbs,a.let X,bs = Xbs 
               in let X',fs = X(a) 
                  in let bs' ⟵ ⋃f∈fs.⋃b∈bs.f b
                     in <<X', if bag-null(bs') then bs else bs' fi >, bs'>;s.let X,bs = s 
                                                                          in hdf-halted(X);<X, bs>)


Definitions occuring in Statement :  mk-hdf: mk-hdf(s,m.G[s; m];st.H[st];s0),  hdf-halted: hdf-halted(P),  hdf-ap: X(a),  callbyvalueall: callbyvalueall,  ifthenelse: if b then t else f fi ,  apply: f a,  spread: spread def,  pair: <a, b>,  bag-combine: ⋃x∈bs.f[x],  bag-null: bag-null(bs)
FDL editor aliases :  hdf-buffer
Latex:
hdf-buffer(X;bs)  ==
    mk-hdf(Xbs,a.let  X,bs  =  Xbs 
                              in  let  X',fs  =  X(a) 
                                    in  let  bs'  \mleftarrow{}{}  \mcup{}f\mmember{}fs.\mcup{}b\mmember{}bs.f  b
                                          in  <<X',  if  bag-null(bs')  then  bs  else  bs'  fi  >,  bs'>s.let  X,bs  =  s 
                                                                                                                                                    in  hdf-halted(X);<X,  bs>)


Date html generated: 2016_05_16-AM-10_39_58
Last ObjectModification: 2012_11_23-PM-02_09_35

Theory : halting!dataflow


Home Index