Nuprl Lemma : hdf-parallel-transformation2

∀[L,G,H,S,init,out:Base]. ∀[m:ℕ].
  (inl (λa.<inr Ax , out>) || fix((λmk-hdf,s. (inl (λa.cbva_seq(L[s;a]; λg.<case H[g;s]
                                                                             of inl() =>
                                                                             mk-hdf S[g;s]
                                                                             | inr() =>
                                                                             inr Ax 
                                                                           , G[g]
                                                                           >; m))))) 
                              init ~ fix((λmk-hdf,s. (inl (λa.cbva_seq(λn.if (n =z m)
                                                                          then case fst(s)
                                                                                of inl(x) =>
                                                                                mk_lambdas_fun(λg.(out + G[g]);m)
                                                                                | inr(x) =>
                                                                                mk_lambdas_fun(λg.G[g];m)
                                                                          else L[snd(s);a] n
                                                                          fi ; λg.<case H[partial_ap(g;m + 1;m);snd(s)]
                                                                                    of inl() =>
                                                                                    mk-hdf 
                                                                                    <inr Ax 
                                                                                    , S[partial_ap(g;m + 1;m);snd(s)]
                                                                                    >
                                                                                    | inr() =>
                                                                                    inr Ax 
                                                                                  , select_fun_last(g;m)
                                                                                  >; m + 1))))) 
                                     <inl Ax, init>)


Proof



Definitions occuring in Statement :  hdf-parallel: X || Y,  nat: ℕ,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  uall: ∀[x:A]. B[x],  so_apply: x[s1;s2],  so_apply: x[s],  pi1: fst(t),  pi2: snd(t),  apply: f a,  fix: fix(F),  lambda: λx.A[x],  pair: <a, b>,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  inl: inl x,  add: n + m,  natural_number: $n,  base: Base,  sqequal: s ~ t,  axiom: Ax,  bag-append: as + bs,  select_fun_last: select_fun_last(g;m),  partial_ap: partial_ap(g;n;m),  mk_lambdas_fun: mk_lambdas_fun(F;m),  cbva_seq: cbva_seq(L; F; m)
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  eq_int: (i =z j),  ifthenelse: if b then t else f fi ,  hdf-parallel: X || Y,  bfalse: ff,  btrue: tt,  hdf-halted: hdf-halted(P),  band: p ∧b q,  hdf-ap: X(a),  mk-hdf: mk-hdf(s,m.G[s; m];st.H[st];s0),  hdf-run: hdf-run(P),  hdf-halt: hdf-halt(),  isr: isr(x),  so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),  so_apply: x[s1;s2;s3;s4],  so_lambda: λ2x.t[x],  top: Top,  so_apply: x[s],  uimplies: b supposing a,  strict4: strict4(F),  and: P ∧ Q,  all: ∀x:A. B[x],  implies: P ⇒ Q,  has-value: (a)↓,  prop: ℙ,  guard: {T},  or: P ∨ Q,  squash: ↓T,  so_lambda: λ2x y.t[x; y],  so_apply: x[s1;s2],  empty-bag: {},  nil: [],  it: ⋅,  pi1: fst(t),  pi2: snd(t),  select_fun_last: select_fun_last(g;m),  int_seg: {i..j-},  lelt: i ≤ j < k,  satisfiable_int_formula: satisfiable_int_formula(fmla),  exists: ∃x:A. B[x],  false: False,  not: ¬A,  decidable: Dec(P),  subtype_rel: A ⊆r B,  le: A ≤ B,  less_than': less_than'(a;b),  nat: ℕ,  ge: i ≥ j ,  sq_type: SQType(T)
Latex:
\mforall{}[L,G,H,S,init,out:Base].  \mforall{}[m:\mBbbN{}].
    (inl  (\mlambda{}a.<inr  Ax  ,  out>)  ||  fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(L[s;a];  \mlambda{}g.<case  H[g;s]
                                                                                                                                                          of  inl()  =>
                                                                                                                                                          mk-hdf  S[g;s]
                                                                                                                                                          |  inr()  =>
                                                                                                                                                          inr  Ax 
                                                                                                                                                      ,  G[g]
                                                                                                                                                      >  m))))) 
                                                            init 
    \msim{}  fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(\mlambda{}n.if  (n  =\msubz{}  m)
                                                                                  then  case  fst(s)
                                                                                              of  inl(x)  =>
                                                                                              mk\_lambdas\_fun(\mlambda{}g.(out  +  G[g]);m)
                                                                                              |  inr(x)  =>
                                                                                              mk\_lambdas\_fun(\mlambda{}g.G[g];m)
                                                                                  else  L[snd(s);a]  n
                                                                                  fi  ;  \mlambda{}g.<case  H[partial\_ap(g;m  +  1;m);snd(s)]
                                                                                                      of  inl()  =>
                                                                                                      mk-hdf  <inr  Ax  ,  S[partial\_ap(g;m  +  1;m);snd(s)]>
                                                                                                      |  inr()  =>
                                                                                                      inr  Ax 
                                                                                                  ,  select\_fun\_last(g;m)
                                                                                                  >  m  +  1))))) 
        <inl  Ax,  init>)


Date html generated: 2016_05_16-AM-10_47_01
Last ObjectModification: 2016_01_17-AM-11_11_10

Theory : halting!dataflow


Home Index