Nuprl Definition : rec-bind-nxt

rec-bind-nxt(X;Y;p;a) ==
  let sx,sy 
  in let Ys ⟵ bag-map(λp.p(a);sy)
     in let sy' bag-mapfilter(λx.(fst(x));λx.isl(fst(x));Ys) in
         let Youts = ⋃x∈Ys.snd(x) in
         let newXs bag-map(X;Youts) in
         let Xs ⟵ bag-map(λp.p(a);sx newXs)
         in let sx' bag-mapfilter(λx.(fst(x));λx.isl(fst(x));Xs) in
             let Xouts = ⋃x∈Xs.snd(x) in
             let Ys' ⟵ bag-map(λx.(fst(Y x(a)));Youts)
             in let sy'' [p∈Ys'|isl(p)] in
                    <<sx', sy' sy''>Xouts>



Definitions occuring in Statement :  hdf-ap: X(a) callbyvalueall: callbyvalueall isl: isl(x) let: let pi1: fst(t) pi2: snd(t) apply: a lambda: λx.A[x] spread: spread def pair: <a, b> bag-combine: x∈bs.f[x] bag-mapfilter: bag-mapfilter(f;P;bs) bag-filter: [x∈b|p[x]] bag-append: as bs bag-map: bag-map(f;bs)
FDL editor aliases :  rec-bind-nxt

Latex:
rec-bind-nxt(X;Y;p;a)  ==
    let  sx,sy  =  p 
    in  let  Ys  \mleftarrow{}{}  bag-map(\mlambda{}p.p(a);sy)
          in  let  sy'  =  bag-mapfilter(\mlambda{}x.(fst(x));\mlambda{}x.isl(fst(x));Ys)  in
                  let  Youts  =  \mcup{}x\mmember{}Ys.snd(x)  in
                  let  newXs  =  bag-map(X;Youts)  in
                  let  Xs  \mleftarrow{}{}  bag-map(\mlambda{}p.p(a);sx  +  newXs)
                  in  let  sx'  =  bag-mapfilter(\mlambda{}x.(fst(x));\mlambda{}x.isl(fst(x));Xs)  in
                          let  Xouts  =  \mcup{}x\mmember{}Xs.snd(x)  in
                          let  Ys'  \mleftarrow{}{}  bag-map(\mlambda{}x.(fst(Y  x(a)));Youts)
                          in  let  sy''  =  [p\mmember{}Ys'|isl(p)]  in
                                        <<sx',  sy'  +  sy''>,  Xouts>



Date html generated: 2016_05_16-AM-10_44_29
Last ObjectModification: 2012_11_23-PM-02_10_09

Theory : halting!dataflow


Home Index