---

feedback-df-prog(B;G;halt;dfps) ==
  <B
  , tuple-type(map(dfp.(df-program-statetype(dfp)?);dfps))  bag(B)
  , <tuple(||dfps||;i.inl df-program-state(dfps[i]) ), {}>
  , let n := ||dfps|| in
    let nxt 
     tuple(n;i.let T,S,init,nxt = dfps[i]
               in a,x.case x of inl(z) => nxt z a | inr(z) => <x, {}>  )
    in sb,a.
        let s,buf = sb 
        in if halt s
           then <inr  , {}>
           else let ps 
                 ap2-tuple(n;nxt;a;s)
                in let x 
                    G map-tuple(n;p.(snd(p));ps) buf
                   in <inl <evalall(map-tuple(n;p.(fst(p));ps))
                       , if null(x) then buf else x fi 
                       > 
                   , x
                   >
           fi >

---

Definitions occuring in Statement :  df-program-state: df-program-state(dfp),  df-program-statetype: df-program-statetype(dfp),  select: l[i],  map: map(f;as),  length: ||as||,  null: null(as),  ifthenelse: if b then t else f fi ,  it: ,  spreadn: spread4,  pi1: fst(t),  pi2: snd(t),  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: {},  bag: bag(T),  map-tuple: map-tuple(len;f;t),  ap2-tuple: ap2-tuple(len;f;x;t),  tuple: tuple(n;i.F[i]),  tuple-type: tuple-type(L),  evalall: evalall(t),  callbyvalueall: callbyvalueall,  callbyvalue: callbyvalue
Definitions :  product: x:A  B[x],  tuple-type: tuple-type(L),  map: map(f;as),  union: left + right,  df-program-statetype: df-program-statetype(dfp),  unit: Unit,  bag: bag(T),  df-program-state: df-program-state(dfp),  callbyvalue: callbyvalue,  length: ||as||,  tuple: tuple(n;i.F[i]),  spreadn: spread4,  select: l[i],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  spread: spread def,  inr: inr x ,  it: ,  empty-bag: {},  ap2-tuple: ap2-tuple(len;f;x;t),  callbyvalueall: callbyvalueall,  apply: f a,  pi2: snd(t),  inl: inl x ,  pair: <a, b>,  evalall: evalall(t),  map-tuple: map-tuple(len;f;t),  lambda: x.A[x],  pi1: fst(t),  ifthenelse: if b then t else f fi ,  null: null(as)
FDL editor aliases :  feedback-df-prog

---

feedback-df-prog(B;G;halt;dfps)  ==
    <B
    ,  tuple-type(map(\mlambda{}dfp.(df-program-statetype(dfp)?);dfps))  \mtimes{}  bag(B)
    ,  <tuple(||dfps||;i.inl  df-program-state(dfps[i])  ),  \{\}>
    ,  let  n  :=  ||dfps||  in
        let  nxt  \mleftarrow{}{}
          tuple(n;i.let  T,S,init,nxt  =  dfps[i]
                              in  \mlambda{}a,x.case  x  of  inl(z)  =>  nxt  z  a  |  inr(z)  =>  <x,  \{\}>    )
        in  \mlambda{}sb,a.
                let  s,buf  =  sb 
                in  if  halt  s
                      then  <inr  \mcdot{}  ,  \{\}>
                      else  let  ps  \mleftarrow{}{}
                                  ap2-tuple(n;nxt;a;s)
                                in  let  x  \mleftarrow{}{}
                                        G  map-tuple(n;\mlambda{}p.(snd(p));ps)  buf
                                      in  <inl  <evalall(map-tuple(n;\mlambda{}p.(fst(p));ps)),  if  null(x)  then  buf  else  x  fi  > 
                                      ,  x
                                      >
                      fi  >


Date html generated: 2011_08_16-AM-09_40_25
Last ObjectModification: 2011_06_09-PM-05_13_46

Home Index