Theory Benchmarks
section ‹Benchmark Problems for Computing Gr\"obner Bases›
theory Benchmarks
imports Polynomials.MPoly_Type_Class_OAlist
begin
text ‹This theory defines various well-known benchmark problems for computing Gr\"obner bases. The
actual tests of the different algorithms on these problems are contained in the theories whose
names end with ‹_Examples›.›
subsection ‹Cyclic›
definition cycl_pp :: "nat ⇒ nat ⇒ nat ⇒ (nat, nat) pp"
where "cycl_pp n d i = sparse⇩0 (map (λk. (modulo (k + i) n, 1)) [0..<d])"
definition cyclic :: "(nat, nat) pp nat_term_order ⇒ nat ⇒ ((nat, nat) pp ⇒⇩0 'a::{zero,one,uminus}) list"
where "cyclic to n =
(let xs = [0..<n] in
(map (λd. distr⇩0 to (map (λi. (cycl_pp n d i, 1)) xs)) [1..<n]) @
[distr⇩0 to [(cycl_pp n n 0, 1), (0, -1)]]
)"
text ‹@{term "cyclic n"} is a system of ‹n› polynomials in ‹n› indeterminates, with maximum degree ‹n›.›
subsection ‹Katsura›
definition katsura_poly :: "(nat, nat) pp nat_term_order ⇒ nat ⇒ nat ⇒ ((nat, nat) pp ⇒⇩0 'a::comm_ring_1)"
where "katsura_poly to n i =
change_ord to ((∑j::int=-int n..<n + 1. if abs (i - j) ≤ n then V⇩0 (nat (abs j)) * V⇩0 (nat (abs (i - j))) else 0) - V⇩0 i)"
definition katsura :: "(nat, nat) pp nat_term_order ⇒ nat ⇒ ((nat, nat) pp ⇒⇩0 'a::comm_ring_1) list"
where "katsura to n =
(let xs = [0..<n] in
(distr⇩0 to ((sparse⇩0 [(0, 1)], 1) # (map (λi. (sparse⇩0 [(Suc i, 1)], 2)) xs) @ [(0, -1)])) #
(map (katsura_poly to n) xs)
)"
text ‹For @{prop "1 ≤ n"}, @{term "katsura n"} is a system of ‹n + 1› polynomials in ‹n + 1›
indeterminates, with maximum degree ‹2›.›
subsection ‹Eco›
definition eco_poly :: "(nat, nat) pp nat_term_order ⇒ nat ⇒ nat ⇒ ((nat, nat) pp ⇒⇩0 'a::comm_ring_1)"
where "eco_poly to m i =
distr⇩0 to ((sparse⇩0 [(i, 1), (m, 1)], 1) # map (λj. (sparse⇩0 [(j, 1), (j + i + 1, 1), (m, 1)], 1)) [0..<m - i - 1])"
definition eco :: "(nat, nat) pp nat_term_order ⇒ nat ⇒ ((nat, nat) pp ⇒⇩0 'a::comm_ring_1) list"
where "eco to n =
(let m = n - 1 in
(distr⇩0 to ((map (λj. (sparse⇩0 [(j, 1)], 1)) [0..<m]) @ [(0, 1)])) #
(distr⇩0 to [(sparse⇩0 [(m-1, 1), (m,1)], 1), (0, - of_nat m)]) #
(rev (map (eco_poly to m) [0..<m-1]))
)"
text ‹For @{prop "2 ≤ n"}, @{term "eco n"} is a system of ‹n› polynomials in ‹n› indeterminates,
with maximum degree ‹3›.›
subsection ‹Noon›
definition noon_poly :: "(nat, nat) pp nat_term_order ⇒ nat ⇒ nat ⇒ ((nat, nat) pp ⇒⇩0 'a::comm_ring_1)"
where "noon_poly to n i =
(let ten = of_nat 10; eleven = - of_nat 11 in
distr⇩0 to ((map (λj. if j = i then (sparse⇩0 [(i, 1)], eleven) else (sparse⇩0 [(j, 2), (i, 1)], ten)) [0..<n]) @
[(0, ten)]))"
definition noon :: "(nat, nat) pp nat_term_order ⇒ nat ⇒ ((nat, nat) pp ⇒⇩0 'a::comm_ring_1) list"
where "noon to n = (noon_poly to n 1) # (noon_poly to n 0) # (map (noon_poly to n) [2..<n])"
text ‹For @{prop "2 ≤ n"}, @{term "noon n"} is a system of ‹n› polynomials in ‹n› indeterminates,
with maximum degree ‹3›.›
end