Nuprl Definition : mk-hdf

mk-hdf(s,m.G[s; m];st.H[st];s0) ==
  fix((λmk-hdf,s0. if H[s0] then hdf-halt() else hdf-run(λm.let s1,b = G[s0; m] in <mk-hdf s1, b>) fi )) s0


Definitions occuring in Statement :  hdf-run: hdf-run(P),  hdf-halt: hdf-halt(),  ifthenelse: if b then t else f fi ,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  pair: <a, b>
FDL editor aliases :  mk-hdf
Latex:
mk-hdf(s,m.G[s;  m];st.H[st];s0)  ==
    fix((\mlambda{}mk-hdf,s0.  if  H[s0]
                                    then  hdf-halt()
                                    else  hdf-run(\mlambda{}m.let  s1,b  =  G[s0;  m] 
                                                                    in  <mk-hdf  s1,  b>)
                                    fi  )) 
    s0


Date html generated: 2016_05_16-AM-10_38_52
Last ObjectModification: 2012_11_23-PM-02_09_23

Theory : halting!dataflow


Home Index