Theory Benchmarks

(* Author: Alexander Maletzky *)

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 = sparse0 (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. distr0 to (map (λi. (cycl_pp n d i, 1)) xs)) [1..<n]) @
              [distr0 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›.›

(*
Input: n
Define: m ≡ n - 1
Variables: x(0), ..., x(m)
Polynomials: p(0), ..., p(m)

p(0)  = x(0) + ... + x(m)
p(1)  = x(0)*x(1) + x(1)*x(2) + ... + x(m-1)*x(m) + x(m)*x(0)
p(1)  = x(0)*x(1)*x(2) + x(1)*x(2)*x(3) + ... + x(m-1)*x(m)*x(0) + x(m)*x(0)*x(1)
...
p(m)  = x(0)*x(1)*...*x(m) - 1
*)

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 V0 (nat (abs j)) * V0 (nat (abs (i - j))) else 0) - V0 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
            (distr0 to ((sparse0 [(0, 1)], 1) # (map (λi. (sparse0 [(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›.›

(*
Input: n
Variables: x(0), ..., x(n)
Polynomials: p(0), ..., p(n)

p(0)    = x(0) + 2 * (x(1) + ... + x(n)) - 1
p(i+1)  = (∑j=-n..n. if |i - j| ≤ n then x(|j|) * x(|i - j|) else 0) - x(i)    for 0 ≤ i < n
*)

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 =
            distr0 to ((sparse0 [(i, 1), (m, 1)], 1) # map (λj. (sparse0 [(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
            (distr0 to ((map (λj. (sparse0 [(j, 1)], 1)) [0..<m]) @ [(0, 1)])) #
            (distr0 to [(sparse0 [(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›.›

(*
Input: n
Define: m ≡ n - 1
Variables: x(0), ..., x(m)
Polynomials: p(m), ..., p(0)

p(i)    = x(i)*x(m) + x(0)*x(i+1)*x(m) + ... + x(m-i-2)*x(m-1)*x(m)    for 0 ≤ i < m-1
p(m-1)  = x(m-1)*x(m) - m
p(m)    = x(0) + ... + x(m-1) + 1
*)

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
              distr0 to ((map (λj. if j = i then (sparse0 [(i, 1)], eleven) else (sparse0 [(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›.›

(*
Input: n
Define: m ≡ n - 1
Variables: x(0), ..., x(m)
Polynomials: p(1), p(0), p(2), ..., p(m)

p(i)  = 10 * (x(0)2*x(i) + x(1)2*x(i) + ... + x(i-1)2*x(i) + x(i+1)2*x(i) + ... + x(m)2*x(i)) - 11*x(i) + 10
    for 0 ≤ i ≤ m
*)

(* https://raw.githubusercontent.com/ederc/singular-benchmarks/master/benchs.lib *)

end (* theory *)