Nuprl Definition : omega

omega works on an "integer problem" that is a set of equality constraints
and a set of inequality constraints. It start by normalizing the constraints.
Then it repeats the "omega_step". On each step, either the number of
equality constraints decreases, or the dimension of the problem (the number
of variables) decreases. Thus the algorithm terminates.

Each step preserves satisfiablity of the constraints, meaning that if
the resulting problem is unsatisfiable then the original problem is
unsatisfiable. Because we have not implemented Bill Pugh's "dark shadow"
test, the reverse is not true in general (the reduced problem could be
satisfiable even though the original problem was unsatisfiable).⋅

omega(eqs;ineqs) == let s ⟵ omega_start(eqs;ineqs) in rep_int_constraint_step(λp.omega_step(p);s)

Definitions occuring in Statement : omega_start: omega_start(eqs;ineqs), omega_step: omega_step(p), rep_int_constraint_step: rep_int_constraint_step(f;p), callbyvalueall: callbyvalueall, lambda: λx.A[x]
Definitions occuring in definition : callbyvalueall: callbyvalueall, omega_start: omega_start(eqs;ineqs), rep_int_constraint_step: rep_int_constraint_step(f;p), lambda: λx.A[x], omega_step: omega_step(p)
FDL editor aliases : omega

Latex:
omega(eqs;ineqs) == let s \mleftarrow{}{} omega\_start(eqs;ineqs) in rep\_int\_constraint\_step(\mlambda{}p.omega\_step(p);s) Date html generated: 2016_07_08-PM-04_48_47 Last ObjectModification: 2016_02_29-PM-06_24_56 Theory : omega Home Index