df-program-halt-meaning(dfp) ==
  let B,S,s0,F = dfp
  in rec-dataflow(inr  ;s,a.case s of inl(s1) =F s1 a | inr(x) => <s, {}>)  



Definitions occuring in Statement :  rec-dataflow: rec-dataflow(s0;s,m.next[s; m]) it: spreadn: spread4 apply: f a pair: <a, b> decide: case b of inl(x) =s[x] | inr(y) =t[y] inr: inr x  empty-bag: {}
Definitions :  spreadn: spread4 rec-dataflow: rec-dataflow(s0;s,m.next[s; m]) inr: inr x  it: decide: case b of inl(x) =s[x] | inr(y) =t[y] apply: f a pair: <a, b> empty-bag: {}
FDL editor aliases :  df-program-halt-meaning

df-program-halt-meaning(dfp)  ==
    let  B,S,s0,F  =  dfp
    in  rec-dataflow(inr  \mcdot{}  ;s,a.case  s  of  inl(s1)  =>  F  s1  a  |  inr(x)  =>  <s,  \{\}>)   


Date html generated: 2011_08_16-AM-09_35_22
Last ObjectModification: 2011_05_05-PM-10_29_20

Home Index