Nuprl Definition : hdf-sequence

hdf-sequence(X;Y;Z) ==
  mk-hdf(S,a.case S
   of inl(XY) =>
   let X,Y XY 
   in let X',bx X(a) 
      in let Y',by Y(a) 
         in if bag-null(bx) ∧b bbag-null(by)) then let Z',bz Z(a) in <inr Z' bz> else <inl <X', Y'>bx> fi 
   inr(Z) =>
   let Z',b Z(a) 
   in <inr Z' b>;S.case of inl(XY) => ff inr(Z) => hdf-halted(Z);inl <X, Y>)



Definitions occuring in Statement :  mk-hdf: mk-hdf(s,m.G[s; m];st.H[st];s0) hdf-halted: hdf-halted(P) hdf-ap: X(a) band: p ∧b q bnot: ¬bb ifthenelse: if then else fi  bfalse: ff spread: spread def pair: <a, b> decide: case of inl(x) => s[x] inr(y) => t[y] inr: inr  inl: inl x bag-null: bag-null(bs)
FDL editor aliases :  hdf-sequence

Latex:
hdf-sequence(X;Y;Z)  ==
    mk-hdf(S,a.case  S
      of  inl(XY)  =>
      let  X,Y  =  XY 
      in  let  X',bx  =  X(a) 
            in  let  Y',by  =  Y(a) 
                  in  if  bag-null(bx)  \mwedge{}\msubb{}  (\mneg{}\msubb{}bag-null(by))
                        then  let  Z',bz  =  Z(a) 
                                  in  <inr  Z'  ,  bz>
                        else  <inl  <X',  Y'>,  bx>
                        fi 
      |  inr(Z)  =>
      let  Z',b  =  Z(a) 
      in  <inr  Z'  ,  b>S.case  S  of  inl(XY)  =>  ff  |  inr(Z)  =>  hdf-halted(Z);inl  <X,  Y>)



Date html generated: 2016_05_16-AM-10_42_30
Last ObjectModification: 2012_12_10-AM-11_55_05

Theory : halting!dataflow


Home Index