Nuprl Definition : rec-bind-df-trans2

rec-bind-df-trans2(Xinit;Yinit;Xnxt;Ynxt) ==
Y
(

rec-bind-df-trans2,s,m.
let a,sx,sy = s in
if (

isl(sx))

(

isl(sy))
then <inr

, {}>
else let ps

          <if isl(sx) then Xnxt a outl(sx) m else <sx, {}> fi
         , if isl(sy)
           then evalall(let s1,L = outl(sy)
                        in let s',b = if isl(s1) then Ynxt a outl(s1) m else <s1, {}> fi
                           in let b' = bag-map(

a.<a, rec-bind-df-init(Xinit;Yinit) a>;b) in
let nxtoutsL = bag-map(

s.(rec-bind-df-trans2 s m);L) in
let nxtoutsB = bag-map(

s.(rec-bind-df-trans2 s m);b') in
let nxtouts = nxtoutsL + nxtoutsB in
let spawned = bag-mapfilter(

p.outl(fst(p));

p.isl(fst(p));nxtouts) in
let out =

p

nxtouts.snd(p) in
let nxtstate = if null(spawned)

(

isl(s')) then inr

  else inl <s', spawned>  fi  in
                               <nxtstate, out>)
           else <sy, {}>
           fi
         >
         in <inl evalall(<a, fst(fst(ps)), fst(snd(ps))>) , (snd(fst(ps))) + (snd(snd(ps)))>
    fi )

Definitions occuring in Statement : rec-bind-df-init: rec-bind-df-init(ix;iy), null: null(as), outl: outl(x), isl: isl(x), band: p

q, bnot:

b, ifthenelse: if b then t else f fi , let: let, it:

, spreadn: spread3, pi1: fst(t), pi2: snd(t), ycomb: Y, apply: f a, lambda:

x.A[x], spread: spread def, pair: <a, b>, inr: inr x , inl: inl x , bag-combine:

x

bs.f[x], bag-mapfilter: bag-mapfilter(f;P;bs), bag-append: as + bs, bag-map: bag-map(f;bs), empty-bag: {}, evalall: evalall(t), callbyvalueall: callbyvalueall
FDL editor aliases : rec-bind-df-trans2

rec-bind-df-trans2(Xinit;Yinit;Xnxt;Ynxt) == Y (\mlambda{}rec-bind-df-trans2,s,m. let a,sx,sy = s in if (\mneg{}\msubb{}isl(sx)) \mwedge{}\msubb{} (\mneg{}\msubb{}isl(sy)) then <inr \mcdot{} , \{\}> else let ps \mleftarrow{}{} <if isl(sx) then Xnxt a outl(sx) m else <sx, \{\}> fi , if isl(sy) then evalall(let s1,L = outl(sy) in let s',b = if isl(s1) then Ynxt a outl(s1) m else <s1, \{\}> fi in let b' = bag-map(\mlambda{}a.<a, rec-bind-df-init(Xinit;Yinit) a>b) in let nxtoutsL = bag-map(\mlambda{}s.(rec-bind-df-trans2 s m);L) in let nxtoutsB = bag-map(\mlambda{}s.(rec-bind-df-trans2 s m);b') in let nxtouts = nxtoutsL + nxtoutsB in let spawned = bag-mapfilter(\mlambda{}p.outl(fst(p));\mlambda{}p.isl(fst(p)); nxtouts) in let out = \mcup{}p\mmember{}nxtouts.snd(p) in let nxtstate = if null(spawned) \mwedge{}\msubb{} (\mneg{}\msubb{}isl(s')) then inr \mcdot{} else inl <s', spawned> fi in <nxtstate, out>) else <sy, \{\}> fi > in <inl evalall(<a, fst(fst(ps)), fst(snd(ps))>) , (snd(fst(ps))) + (snd(snd(ps)))> fi ) Date html generated: 2012_02_20-PM-02_43_40 Last ObjectModification: 2012_02_17-PM-08_04_58 Home Index