Nuprl Definition : hdf-parallel-bag
hdf-parallel-bag(Xs) ==
mk-hdf(Xs,a.eval x = bag-map(λX.X(a);Xs) in
let out ⟵ ⋃p∈x.snd(p)
in <bag-map(λp.(fst(p));x), out>;Xs.bag_all(Xs;λx.hdf-halted(x));Xs)
Definitions occuring in Statement :
mk-hdf: mk-hdf(s,m.G[s; m];st.H[st];s0)
,
hdf-halted: hdf-halted(P)
,
hdf-ap: X(a)
,
callbyvalueall: callbyvalueall,
callbyvalue: callbyvalue,
pi1: fst(t)
,
pi2: snd(t)
,
lambda: λx.A[x]
,
pair: <a, b>
,
bag_all: bag_all(b;f)
,
bag-combine: ⋃x∈bs.f[x]
,
bag-map: bag-map(f;bs)
FDL editor aliases :
hdf-parallel-bag
Latex:
hdf-parallel-bag(Xs) ==
mk-hdf(Xs,a.eval x = bag-map(\mlambda{}X.X(a);Xs) in
let out \mleftarrow{}{} \mcup{}p\mmember{}x.snd(p)
in <bag-map(\mlambda{}p.(fst(p));x), out>Xs.bag\_all(Xs;\mlambda{}x.hdf-halted(x));Xs)
Date html generated:
2016_05_16-AM-10_41_52
Last ObjectModification:
2012_12_14-PM-03_43_11
Theory : halting!dataflow
Home
Index