Nuprl Definition : hdf-compose3
X o Y ==
mk-hdf(XY,a.let X,Y = XY
in let X',fs = X(a)
in let Y',bs = Y(a)
in let out ⟵ ⋃f∈fs.bag-map(f;bs)
in <<X', Y'>, out>;XY.let X,Y = XY
in hdf-halted(X) ∨bhdf-halted(Y);<X, Y>)
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),
bor: p ∨bq,
callbyvalueall: callbyvalueall,
spread: spread def,
pair: <a, b>,
bag-combine: ⋃x∈bs.f[x],
bag-map: bag-map(f;bs)
FDL editor aliases :
hdf-compose3
Latex:
X o Y ==
mk-hdf(XY,a.let X,Y = XY
in let X',fs = X(a)
in let Y',bs = Y(a)
in let out \mleftarrow{}{} \mcup{}f\mmember{}fs.bag-map(f;bs)
in <<X', Y'>, out>XY.let X,Y = XY
in hdf-halted(X) \mvee{}\msubb{}hdf-halted(Y);<X, Y>)
Date html generated:
2016_05_16-AM-10_39_36
Last ObjectModification:
2012_11_23-PM-02_09_31
Theory : halting!dataflow
Home
Index