Изабель: максимальное значение в векторе

Я хотел бы найти максимум в векторе натуральных чисел. Однако вектор (т. е. «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 vector isabelle
person mrsteve    schedule 12.08.2013    source источник

Ответы (1)


arrow_upward
4
arrow_downward

Максимальный оператор 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 — это эта-сокращение %j. v $ j):

 maxvec v = Max (range (op $ v))
person Andreas Lochbihler    schedule 12.08.2013