---

until-prog(A;S;T;sx;sy;nxtx;nxty) ==
  <A
  , S  (T?)
  , <sx, inl sy >
  , s,m.
     evalall(let sx,sy = s 
             in let sx',xout = nxtx sx m 
                in let sy',yout = case sy
                   of inl(s) =>
                    nxty s m
                    | inr(z) =>
                    <sy, {}> 
                   in <case sx'
                       of inl(s) =>
                        if bag-null(yout) then inl <s, sy'>  else inr   fi 
                        | inr(z) =>
                        inr  
                      , xout
                      >)>

---

Definitions occuring in Statement :  ifthenelse: if b then t else f fi ,  it: ,  unit: Unit,  apply: f a,  lambda: x.A[x],  spread: spread def,  pair: <a, b>,  product: x:A  B[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  inl: inl x ,  union: left + right,  bag-null: bag-null(bs),  empty-bag: {},  evalall: evalall(t)
Definitions :  product: x:A  B[x],  union: left + right,  unit: Unit,  lambda: x.A[x],  evalall: evalall(t),  spread: spread def,  apply: f a,  empty-bag: {},  decide: case b of inl(x) => s[x] | inr(y) => t[y],  ifthenelse: if b then t else f fi ,  bag-null: bag-null(bs),  inl: inl x ,  pair: <a, b>,  inr: inr x ,  it:
FDL editor aliases :  until-prog

---

until-prog(A;S;T;sx;sy;nxtx;nxty)  ==
    <A
    ,  S  \mtimes{}  (T?)
    ,  <sx,  inl  sy  >
    ,  \mlambda{}s,m.
          evalall(let  sx,sy  =  s 
                          in  let  sx',xout  =  nxtx  sx  m 
                                in  let  sy',yout  =  case  sy  of  inl(s)  =>  nxty  s  m  |  inr(z)  =>  <sy,  \{\}> 
                                      in  <case  sx'
                                              of  inl(s)  =>
                                                if  bag-null(yout)  then  inl  <s,  sy'>    else  inr  \mcdot{}    fi 
                                                |  inr(z)  =>
                                                inr  \mcdot{} 
                                            ,  xout
                                            >)>


Date html generated: 2011_08_16-PM-06_16_47
Last ObjectModification: 2011_06_16-PM-03_37_34

Home Index