Nuprl Definition : hdf-until

hdf-until(X;Y) ==
  mk-hdf(p,a.let X,Y 
             in let X',b X(a) 
                in let Y',c Y(a) 
                   in <<if bag-null(c) then X' else hdf-halt() fi Y'>b>;p.hdf-halted(fst(p));<X, Y>)



Definitions occuring in Statement :  mk-hdf: mk-hdf(s,m.G[s; m];st.H[st];s0) hdf-halt: hdf-halt() hdf-halted: hdf-halted(P) hdf-ap: X(a) ifthenelse: if then else fi  pi1: fst(t) spread: spread def pair: <a, b> bag-null: bag-null(bs)
FDL editor aliases :  hdf-until

Latex:
hdf-until(X;Y)  ==
    mk-hdf(p,a.let  X,Y  =  p 
                          in  let  X',b  =  X(a) 
                                in  let  Y',c  =  Y(a) 
                                      in  <<if  bag-null(c)  then  X'  else  hdf-halt()  fi  ,  Y'>,  b>p.hdf-halted(fst(p));<X
                                                                                                                                                                                                  ,  Y
                                                                                                                                                                                                  >)



Date html generated: 2016_05_16-AM-10_40_59
Last ObjectModification: 2012_11_23-PM-02_09_51

Theory : halting!dataflow


Home Index