Nuprl Definition : rec-bind-nxt

rec-bind-nxt(X;Y;p;a) ==
  let sx,sy = p 
  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: f 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
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: 2015_07_17-AM-08_07_59
Last ObjectModification: 2012_11_23-PM-02_10_09

Home Index