### 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)
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