Nuprl Definition : gcd-reduce-ineq-constraints
Each inequality constraint is a list [c,a1,a2,...] and represents the
constraint c + a1*v1 + a2*v2 + .... >= 0 (on variables v1, v2, ...).
If g = gcd(a1,a2,...) is greater than 1 then we
divide all the a1,a2,... by g and replace c by the "floor" of ⌜c ÷ g⌝.
This preserves the satisfiability of the inequality.⋅
gcd-reduce-ineq-constraints(sat;LL) ==
accumulate_abort(L,Ls.let h,t = L
in if t = Ax then if (h) < (0) then inr ⋅ else (inl [L / Ls])
otherwise eval g = |gcd-list(t)| in
if (1) < (g)
then eval h' = h ÷↓ g in
eval t' = eager-map(λx.(x ÷ g);t) in
inl [[h' / t'] / Ls]
else (inl [L / Ls]);inl sat;LL)
Definitions occuring in Statement :
gcd-list: gcd-list(L),
accumulate_abort: accumulate_abort(x,sofar.F[x; sofar];s;L),
eager-map: eager-map(f;as),
cons: [a / b],
div_floor: a ÷↓ n,
absval: |i|,
callbyvalue: callbyvalue,
it: ⋅,
isaxiom: if z = Ax then a otherwise b,
less: if (a) < (b) then c else d,
lambda: λx.A[x],
spread: spread def,
inr: inr x ,
inl: inl x,
divide: n ÷ m,
natural_number: $n
Definitions occuring in definition :
accumulate_abort: accumulate_abort(x,sofar.F[x; sofar];s;L),
spread: spread def,
isaxiom: if z = Ax then a otherwise b,
inr: inr x ,
it: ⋅,
absval: |i|,
gcd-list: gcd-list(L),
less: if (a) < (b) then c else d,
natural_number: $n,
div_floor: a ÷↓ n,
callbyvalue: callbyvalue,
eager-map: eager-map(f;as),
lambda: λx.A[x],
divide: n ÷ m,
cons: [a / b],
inl: inl x
FDL editor aliases :
gcd-reduce-ineq-constraints
Latex:
gcd-reduce-ineq-constraints(sat;LL) ==
accumulate\_abort(L,Ls.let h,t = L
in if t = Ax then if (h) < (0) then inr \mcdot{} else (inl [L / Ls])
otherwise eval g = |gcd-list(t)| in
if (1) < (g)
then eval h' = h \mdiv{}\mdownarrow{} g in
eval t' = eager-map(\mlambda{}x.(x \mdiv{} g);t) in
inl [[h' / t'] / Ls]
else (inl [L / Ls]);inl sat;LL)
Date html generated:
2016_07_08-PM-04_48_15
Last ObjectModification:
2015_12_14-PM-06_36_35
Theory : omega
Home
Index