---

parallel-df-prog2(B;G;dfp1;dfp2) ==
  let C1,S1,s1,F1 = dfp1
  in let C2,S2,s2,F2 = dfp2
     in <B
        , S1?  (S2?)
        , <inl s1 , inl s2 >
        , s,a.
           evalall(let s1,s2 = s 
                   in case s1
                      of inl(s1) =>
                       let s1',out1 = F1 s1 a 
                       in case s2
                          of inl(s2) =>
                           let s2',out2 = F2 s2 a 
                           in <inl <s1', s2'> , G out1 out2>
                           | inr(x) =>
                           <inl <s1', s2> , G out1 {}>
                       | inr(x) =>
                       case s2
                       of inl(s2) =>
                        let s2',out2 = F2 s2 a 
                        in <inl <s1, s2'> , G {} out2>
                        | inr(x) =>
                        <inr  , {}>)>    

---

Definitions occuring in Statement :  it: ,  spreadn: spread4,  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,  empty-bag: {},  evalall: evalall(t)
Definitions :  spreadn: spread4,  product: x:A  B[x],  union: left + right,  unit: Unit,  lambda: x.A[x],  evalall: evalall(t),  decide: case b of inl(x) => s[x] | inr(y) => t[y],  spread: spread def,  inl: inl x ,  apply: f a,  pair: <a, b>,  inr: inr x ,  it: ,  empty-bag: {}
FDL editor aliases :  parallel-df-prog2

---

parallel-df-prog2(B;G;dfp1;dfp2)  ==
    let  C1,S1,s1,F1  =  dfp1
    in  let  C2,S2,s2,F2  =  dfp2
          in  <B
                ,  S1?  \mtimes{}  (S2?)
                ,  <inl  s1  ,  inl  s2  >
                ,  \mlambda{}s,a.
                      evalall(let  s1,s2  =  s 
                                      in  case  s1
                                            of  inl(s1)  =>
                                              let  s1',out1  =  F1  s1  a 
                                              in  case  s2
                                                    of  inl(s2)  =>
                                                      let  s2',out2  =  F2  s2  a 
                                                      in  <inl  <s1',  s2'>  ,  G  out1  out2>
                                                      |  inr(x)  =>
                                                      <inl  <s1',  s2>  ,  G  out1  \{\}>
                                              |  inr(x)  =>
                                              case  s2
                                              of  inl(s2)  =>
                                                let  s2',out2  =  F2  s2  a 
                                                in  <inl  <s1,  s2'>  ,  G  \{\}  out2>
                                                |  inr(x)  =>
                                                <inr  \mcdot{}  ,  \{\}>)>       


Date html generated: 2011_08_16-AM-09_42_23
Last ObjectModification: 2011_06_02-PM-04_07_44

Home Index