Nuprl Definition : bind-nxt

bind-nxt(Y;p;a) ==
  let X,ys 
  in let X',b X(a) 
     in let ybs ⟵ bag-map(λP.P(a);ys bag-map(Y;b))
        in let ys' ⟵ [y∈bag-map(λyb.(fst(yb));ybs)|¬bhdf-halted(y)]
           in let out ⟵ ⋃yb∈ybs.snd(yb)
              in <<X', ys'>out>



Definitions occuring in Statement :  hdf-halted: hdf-halted(P) hdf-ap: X(a) callbyvalueall: callbyvalueall bnot: ¬bb pi1: fst(t) pi2: snd(t) lambda: λx.A[x] spread: spread def pair: <a, b> bag-combine: x∈bs.f[x] bag-filter: [x∈b|p[x]] bag-append: as bs bag-map: bag-map(f;bs)
FDL editor aliases :  bind-nxt

Latex:
bind-nxt(Y;p;a)  ==
    let  X,ys  =  p 
    in  let  X',b  =  X(a) 
          in  let  ybs  \mleftarrow{}{}  bag-map(\mlambda{}P.P(a);ys  +  bag-map(Y;b))
                in  let  ys'  \mleftarrow{}{}  [y\mmember{}bag-map(\mlambda{}yb.(fst(yb));ybs)|\mneg{}\msubb{}hdf-halted(y)]
                      in  let  out  \mleftarrow{}{}  \mcup{}yb\mmember{}ybs.snd(yb)
                            in  <<X',  ys'>,  out>



Date html generated: 2016_05_16-AM-10_42_36
Last ObjectModification: 2012_11_23-PM-02_09_59

Theory : halting!dataflow


Home Index