Nuprl Definition : shadow-inequalities
For the given index, i, divide the inequality constraints into ,
those where the i-th coefficient is >0, and those where it is <0
(and ignore -- hence delete -- those where the i-th coefficient is =0)
For each as in the first part and each bs in the second part, form the
"shadow-vec". The list of all of these is the new set of constraints
in which the i-th variable has been eliminated.
In the worst case, N constraints in k+1 variables can result in
(N/2)*(N/2) = N^2/4 constraints in k variables. But this does not seem
to happen in practice for typical theorem proving applications.⋅
shadow-inequalities(i;ineqs) ==
eval Z = evalall(map(λL.L\i;filter(λL.(L[i] =z 0);ineqs))) in
eager-append(eager-product-map(λas,bs. shadow-vec(i;as;bs);filter(λL.0 <z L[i];ineqs);filter(λL.L[i] <z 0;ineqs));Z)
Definitions occuring in Statement :
shadow-vec: shadow-vec(i;as;bs),
list-delete: as\i,
select: L[n],
eager-product-map: eager-product-map(f;as;bs),
filter: filter(P;l),
map: map(f;as),
eager-append: eager-append(as;bs),
evalall: evalall(t),
callbyvalue: callbyvalue,
lt_int: i <z j,
eq_int: (i =z j),
lambda: λx.A[x],
natural_number: $n
Definitions occuring in definition :
callbyvalue: callbyvalue,
evalall: evalall(t),
map: map(f;as),
list-delete: as\i,
eq_int: (i =z j),
eager-append: eager-append(as;bs),
eager-product-map: eager-product-map(f;as;bs),
shadow-vec: shadow-vec(i;as;bs),
filter: filter(P;l),
lambda: λx.A[x],
lt_int: i <z j,
select: L[n],
natural_number: $n
FDL editor aliases :
shadow-inequalities
Latex:
shadow-inequalities(i;ineqs) ==
eval Z = evalall(map(\mlambda{}L.L\mbackslash{}i;filter(\mlambda{}L.(L[i] =\msubz{} 0);ineqs))) in
eager-append(eager-product-map(\mlambda{}as,bs. shadow-vec(i;as;bs);filter(\mlambda{}L.0 <z L[i];
ineqs);filter(\mlambda{}L.L[i] <z 0;ineqs));Z)
Date html generated:
2016_07_08-PM-04_48_19
Last ObjectModification:
2015_12_14-PM-07_03_51
Theory : omega
Home
Index