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 then else fi  apply: 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