Nuprl Definition : omega_step

The "omega step" first searches for an "exact" equality constraint (one where
the coefficient of a variable is 1 or -1). In that case, the constraint can
be solved exactly for that variable, and the variable can be eliminated.
(If that happens, we then run the "gcd-reduce" operations on the resulting
constraints.)

If there is no exact equality constraint, but there are still equality
constraints, then we convert each remaining equality constraints into
two inequality constraints.  (Bill Pugh has a better procedure for
dealing with in-exact equality constraints, but we haven't implemented it.)

If there are no more equality constraints, then omega computes the
"shadow inequalities" for a chosen variable -- which eliminates that variable. 
⋅
omega_step(p) ==
  if (dim(p)) < (1)
     then p
     else case p
           of inl(q) =>
           let eqs,ineqs = q 
           in case first-success(λL.find-exact-eq-constraint(L);eqs)
               of inl(tr) =>
               let i,wj = tr 
               in let w,j = wj 
                  in case gcd-reduce-eq-constraints([];exact-reduce-constraints(w;j;eqs))
                      of inl(eqs') =>
                      case gcd-reduce-ineq-constraints([];exact-reduce-constraints(w;j;ineqs))
                       of inl(ineqs') =>
                       inl <eqs', ineqs'>
                       | inr(x) =>
                       inr x 
                      | inr(x) =>
                      inr x 
               | inr(_) =>
               if null(eqs)
               then case gcd-reduce-ineq-constraints([];shadow_inequalities(ineqs))
                     of inl(ineqs') =>
                     inl <[], ineqs'>
                     | inr(x) =>
                     inr x 
               else inl <[], (eager-map(λeq.eager-map(λx.(-x);eq);eqs) @ eqs) @ ineqs>
               fi 
           | inr(_) =>
           p


Definitions occuring in Statement :  int-problem-dimension: dim(p),  find-exact-eq-constraint: find-exact-eq-constraint(L),  shadow_inequalities: shadow_inequalities(ineqs),  gcd-reduce-ineq-constraints: gcd-reduce-ineq-constraints(sat;LL),  gcd-reduce-eq-constraints: gcd-reduce-eq-constraints(sat;LL),  exact-reduce-constraints: exact-reduce-constraints(w;j;L),  first-success: first-success(f;L),  null: null(as),  eager-map: eager-map(f;as),  append: as @ bs,  nil: [],  ifthenelse: if b then t else f fi ,  less: if (a) < (b)  then c  else d,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  inl: inl x,  minus: -n,  natural_number: $n
Definitions occuring in definition :  less: if (a) < (b)  then c  else d,  int-problem-dimension: dim(p),  natural_number: $n,  first-success: first-success(f;L),  find-exact-eq-constraint: find-exact-eq-constraint(L),  spread: spread def,  gcd-reduce-eq-constraints: gcd-reduce-eq-constraints(sat;LL),  exact-reduce-constraints: exact-reduce-constraints(w;j;L),  ifthenelse: if b then t else f fi ,  null: null(as),  decide: case b of inl(x) => s[x] | inr(y) => t[y],  gcd-reduce-ineq-constraints: gcd-reduce-ineq-constraints(sat;LL),  shadow_inequalities: shadow_inequalities(ineqs),  inr: inr x ,  inl: inl x,  pair: <a, b>,  nil: [],  append: as @ bs,  eager-map: eager-map(f;as),  lambda: λx.A[x],  minus: -n
FDL editor aliases :  omega_step
Latex:
omega\_step(p)  ==
    if  (dim(p))  <  (1)
          then  p
          else  case  p
                      of  inl(q)  =>
                      let  eqs,ineqs  =  q 
                      in  case  first-success(\mlambda{}L.find-exact-eq-constraint(L);eqs)
                              of  inl(tr)  =>
                              let  i,wj  =  tr 
                              in  let  w,j  =  wj 
                                    in  case  gcd-reduce-eq-constraints([];exact-reduce-constraints(w;j;eqs))
                                            of  inl(eqs')  =>
                                            case  gcd-reduce-ineq-constraints([];exact-reduce-constraints(w;j;ineqs))
                                              of  inl(ineqs')  =>
                                              inl  <eqs',  ineqs'>
                                              |  inr(x)  =>
                                              inr  x 
                                            |  inr(x)  =>
                                            inr  x 
                              |  inr($_{}$)  =>
                              if  null(eqs)
                              then  case  gcd-reduce-ineq-constraints([];shadow\_inequalities(ineqs))
                                          of  inl(ineqs')  =>
                                          inl  <[],  ineqs'>
                                          |  inr(x)  =>
                                          inr  x 
                              else  inl  <[],  (eager-map(\mlambda{}eq.eager-map(\mlambda{}x.(-x);eq);eqs)  @  eqs)  @  ineqs>
                              fi 
                      |  inr($_{}$)  =>
                      p


Date html generated: 2017_09_29-PM-05_56_05
Last ObjectModification: 2017_05_24-PM-02_33_46

Theory : omega


Home Index