---

programmable-dataflow{i:l}(A;B;X) ==
  S:Type
   s0:S
    (F:{S  A  (S?  bag(B))| (valueall-type(S)
     (X
      = rec-dataflow(inl s0 ;s,a.case s
        of inl(s1) =>
         F s1 a
         | inr(x) =>
         <s, {}>)))})

---

Definitions occuring in Statement :  rec-dataflow: rec-dataflow(s0;s,m.next[s; m]),  dataflow: dataflow(A;B),  sq_exists: x:{A| B[x]},  exists: x:A. B[x],  and: P  Q,  unit: Unit,  apply: f a,  function: x:A  B[x],  pair: <a, b>,  product: x:A  B[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inl: inl x ,  union: left + right,  universe: Type,  equal: s = t,  valueall-type: valueall-type(T)
Definitions :  universe: Type,  exists: x:A. B[x],  sq_exists: x:{A| B[x]},  function: x:A  B[x],  product: x:A  B[x],  union: left + right,  unit: Unit,  and: P  Q,  valueall-type: valueall-type(T),  equal: s = t,  dataflow: dataflow(A;B),  bag: Error :bag,  rec-dataflow: rec-dataflow(s0;s,m.next[s; m]),  inl: inl x ,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  apply: f a,  pair: <a, b>,  empty-bag: Error :empty-bag
FDL editor aliases :  programmable-dataflow

---

programmable-dataflow\{i:l\}(A;B;X)  ==
    \mexists{}S:Type
      \mexists{}s0:S
        (\mexists{}F:\{S  {}\mrightarrow{}  A  {}\mrightarrow{}  (S?  \mtimes{}  bag(B))|  (valueall-type(S)
        \mwedge{}  (X  =  rec-dataflow(inl  s0  ;s,a.case  s  of  inl(s1)  =>  F  s1  a  |  inr(x)  =>  <s,  \{\}>)))\})


Date html generated: 2011_08_10-AM-08_24_16
Last ObjectModification: 2011_06_02-PM-03_12_39

Home Index