list - 在有限集上定义一个类似于 "arg max"的函数，并证明它的一些属性，并避免通过列表绕道而行

Question

我正在使用向量作为函数的自定义实现，其域是自然数的有限“索引集”，并且其图像是某种可以定义最大值的类型，通常是 real。例如。我可以得到一个二维向量 v，其中 v 1 = 2.7 和 v 3 = 4.2。

在这样的向量上，我想定义一个类似“arg max”的运算符，它告诉我最大分量的索引，3 在 v 的示例中多于。我说“the”索引是因为“arg max”之类的运算符还会接受一个打破平局的函数，该函数将应用于具有值的组件。 (背景是bids in auctions。)

我知道有限集上的 Max 是使用 fold1 定义的(我还不明白它是如何工作的)。我尝试了这个，它本身被接受了，但后来没有为我想做的其他事情工作:

fun arg_max_tb :: "index_set ⇒ tie_breaker ⇒ (real vector) ⇒ nat"
where "arg_max_tb N t v = fold1
  (λ x y . if (v x > v y) then x      (* component values differ *)
   else if (v x = v y ∧ t x y) then x (* tie-breaking needed *)
   else y) N"

请注意，此外我想证明我的“arg max”运算符的某些属性，这可能需要归纳。我知道有规则 finite_ne_induct 用于对有限集进行归纳。好的，但我也希望能够以可以对其进行评估的方式定义我的运算符(例如，当尝试使用具体的有限集时)，但评估

value "arg_max_tb {1::nat} (op >) (nth [27::real, 42])"

预期返回值 1 给我以下错误:

Wellsortedness error
(in code equation arg_max_tb ?n ?t ?v \equiv
                  fold1 (\lambda x y. if ord_real_inst.less_real (?v y) (?v x) then ...) ?n):
Type nat not of sort enum
 No type arity nat :: enum

因此我求助于将我的有限集转换为列表。在列表上，我已经能够通过使用 list_nonempty_induct 进行归纳来定义运算符并证明其某些属性(如果有兴趣可以共享代码)。

基于工作列表的定义如下所示:

fun arg_max_l_tb :: "(nat list) ⇒ tie_breaker ⇒ (real vector) ⇒ nat"
where "arg_max_l_tb [] t v = 0"
      (* in practice we will only call the function
         with lists of at least one element *)
    | "arg_max_l_tb [x] t v = x"
    | "arg_max_l_tb (x # xs) t v =
      (let y = arg_max_l_tb xs t v in
        if (v x > v y) then x              (* component values differ *)
        else if (v x = v y ∧ t x y) then x (* tie-breaking needed *)
        else y)"

fun arg_max_tb :: "index_set ⇒ tie_breaker ⇒ (real vector) ⇒ nat"
where "arg_max_tb N t v = arg_max_l_tb (sorted_list_of_set N) t v"

我没有成功直接在有限集的构造函数上定义函数。以下不起作用:

fun arg_max_tb :: "index_set ⇒ tie_breaker ⇒ (real vector) ⇒ participant"
where "arg_max_tb {} t b = 0"
    | "arg_max_tb {x} t b = x"
    | "arg_max_tb (insert x S) t b =
      (let y = arg_max_tb S t b in
        if (b x > b y) then x
        else if (b x = b y ∧ t x y) then x
        else y)"

它给了我错误信息

Malformed definition:
Non-constructor pattern not allowed in sequential mode.
⋀t b. arg_max_tb {} t b = 0

这会不会是因为列表构造函数被定义为数据类型，而有限集仅被定义为归纳方案？

随便——你知道在有限集上定义这个函数的方法吗？是直接写下来，还是通过一些类似折叠的实用函数？

Answer 1

折叠有限集要求结果与访问集合元素的顺序无关，因为集合是无序的。关于 fold1 f 的大多数引理因此假设折叠操作f是左交换的，即 f a (f b x) = f b (f a x)对于所有 a , b , x .

您提供给 fold1 的函数在您的第一个定义中不满足这一点，因为打破平局的功能是任意谓词。例如，采用平局函数 %v v'. True .因此，如果你想坚持这个定义，你必须首先找到打破平局的充分条件，并将这个假设贯穿你所有的引理。

您基于元素排序列表的工作解决方案避免了这种交换性问题。您关于 {} 的模式匹配的最后建议, {x}和 insert x S不工作有两个原因。一、fun只能在数据类型构造函数上进行模式匹配，因此您必须使用 function反而;这解释了错误消息。但是随后，您还必须证明方程不重叠，因此您将再次遇到与交换性相同的问题。此外，您将无法证明终止，因为 S可能是无限的。

代码生成的排序错误来自 fold1 的设置. fold1 f A定义为 THE x. fold1Set f A x其中 fold1Set f A x持有 iff x是折叠的结果 f在 A按照元素的某种顺序。为了检查所有结果是否相同，生成的代码天真地测试了 x 的所有可能值。是否fold1Set f A x持有。如果它确实只找到一个这样的值，则返回该值。否则，它会引发异常。在你的情况下，x是一个索引，即 nat 类型其中蕴含着无限多的值(value)。因此，不可能进行详尽的测试。从技术上讲，这翻译为 nat不是类型类的实例 enum .

通常，您会为根据 fold1 定义的所有内容推导出专门的代码方程式.请参阅有关程序优化的代码生成器教程。