我想找到自然数向量中的最大值。然而,向量(即‘vec’)是与集合或列表不同的类型。我考虑了几个行不通的想法,比如调平或提升 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))"
最大算子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))
本文内容由网友自发贡献,版权归原作者所有,本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容,请联系:hwhale#tublm.com(使用前将#替换为@)