Nuprl Definition : omega_step

The "omega step" first searches for an "exact" equality constraint (one where
the coefficient of variable is 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

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 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 chosen variable -- which eliminates that variable. 

omega_step(p) ==
  if (dim(p)) < (1)
     then p
     else case p
           of inl(q) =>
           let eqs,ineqs 
           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(_) =>
               if null(eqs)
               then case gcd-reduce-ineq-constraints([];shadow_inequalities(ineqs))
                     of inl(ineqs') =>
                     inl <[], ineqs'>
                     inr(x) =>
               else inl <[], (eager-map(λeq.eager-map(λx.(-x);eq);eqs) eqs) ineqs>
           inr(_) =>

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 then else fi  less: if (a) < (b)  then c  else d lambda: λx.A[x] spread: spread def pair: <a, b> decide: case of inl(x) => s[x] inr(y) => t[y] inr: inr  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 then else fi  null: null(as) decide: case 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  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

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>
                      |  inr($_{}$)  =>

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

Theory : omega

Home Index