Nuprl Definition : hdataflow
A "halting dataflow", P, is either halted (inr ⋅ ) or it is a function
that given an input a ∈ A computes a pair <Q, out>, where Q is a new
"halting dataflow" and out is a bag of type B.⋅
hdataflow(A;B) == corec(P.A ⟶ (P × bag(B))?)
Definitions occuring in Statement :
corec: corec(T.F[T]),
unit: Unit,
function: x:A ⟶ B[x],
product: x:A × B[x],
union: left + right,
bag: bag(T)
FDL editor aliases :
hdf
Latex:
hdataflow(A;B) == corec(P.A {}\mrightarrow{} (P \mtimes{} bag(B))?)
Date html generated:
2016_05_17-PM-03_26_14
Last ObjectModification:
2014_07_15-PM-05_03_48
Theory : halting!dataflow
Home
Index