Nuprl Definition : bind-nxt
bind-nxt(Y;p;a) ==
let X,ys = p
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