3

我想在自然数向量中找到最大值。然而，Vector（即'vec'）是与Set 或List 不同的类型。我想了几个不起作用的想法，比如调平或提升 vec 的类型或递归函数的定义。

你建议什么解决方案来获得向量中的最大值？

(*
IMPORTS:
  "~~/src/HOL/Algebra/Ring"
  "~~/src/HOL/Library/Numeral_Type"
  "~~/src/HOL/Library/Permutations"
  "~~/src/HOL/Library/Polynomial"
  "~~/src/HOL/Big_Operators"

 vec (VECTOR) is from Finite_Cartesian_Product
 degree is from Polynomial
 Max is from Big_Operators
*)

(* The problem is that "Max" from Big_Operators is not working on vectors! *)
definition maxdeg:: "('a::zero poly)^'n ⇒ nat" where "maxdeg v = Max(χ i . degree(v$i))"
4

1 回答 1

4

最大值运算符Max具有类型'a set => 'a，即从（有限）集合中检索最大元素。向量（类型(a, b) vec）本质上是从索引到条目的函数，抽象写成χ i. _，应用写成v $ _。

您现在想要获得向量范围内的最大值。考虑到上述情况，您可以使用range函数并在向量上拼出函数应用程序：

 maxdeg v = Max (range (%j. (χ i. degree (v $ i)) $ j))

这可以简化为

 maxdeg v = Max (range (%i. degree (v $ i)))

如果您只想要向量的最大条目而不首先在向量上映射度，则以下工作（其中op $ v的 eta 收缩%j. v $ j）：

 maxvec v = Max (range (op $ v))
于 2013-08-12T06:31:55.343 回答