2

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

在这样的向量上，我想定义一个类似“arg max”的运算符，它告诉我最大分量的索引，3在上面的例子中v。我说的是“the”索引，因为“arg max”like 运算符将另外接受一个打破平局的函数，以应用于具有值的组件。（背景是拍卖中的出价。）

我知道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

这可能是因为列表构造函数被定义为 a datatype，而有限集仅被定义为一个inductive方案？

不管怎样——你知道在有限集上定义这个函数的方法吗？要么直接写下来，要么通过一些类似折叠的效用函数？

4

2 回答 2

4

对有限集合进行折叠要求结果与访问集合元素的顺序无关，因为集合是无序的。因此，大多数关于的引理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且仅当是以元素的某种顺序x折叠的结果f。A为了检查所有结果是否相同，生成的代码天真地测试x是否fold1Set f A x成立的所有可能值。如果它确实只找到一个这样的值，那么它会返回该值。否则，它会引发异常。在您的情况下，x是一个索引，即nat具有无限多个值的类型。因此，不可能进行详尽的测试。从技术上讲，这nat不是类型 class 的实例enum。

通常，您会为根据fold1. 请参阅有关程序细化的代码生成器教程。

于 2013-05-23T05:52:06.067 回答
3

这个问题实际上由多个问题组成。

在有限集上定义函数

折叠/折叠l1

通常的递归组合器是Finite_Set.fold（或fold1）。然而，为了能够证明任何事情fold f z S，结果必须独立于f应用于元素的顺序S。

如果f是关联的和可交换的，您可以使用 Finite_Set.ab_semigroup_mult.fold1_insert andFinite_Set.fold1_singleton来获得简单规则，fold1 f S并且您应该能够将其finite_ne_induct用作您的归纳规则。

请注意，您提供给 fold1 的函数（我称之为）仅在是线性顺序f时才可交换：t

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"

fold1 上的现有引理并未涵盖这一点，因此您需要证明的通用变体Finite_Set.ab_semigroup_mult.fold1_insert或插入额外的决胜局，例如

   else if (v x = v y ∧ ~t x y ∧ ~t y x ∧ x < y) then x

如果t是线性订单，您将能够从 simp 规则中删除这个额外的决胜局。请注意，这个额外的决胜局基本上是您从使用sorted_list_of_set.

/一些

您arg_max_tb选择具有某些属性的列表中的一个元素。这也可以直接使用构造THE x. P x或SOME x. P x（选择运算符）定义。前者选择满足属性 P 的唯一元素（如果不存在唯一元素，则结果未定义），后者选择满足属性 P 的某个元素（如果不存在此类元素，则结果未定义）。两者都适用于无限列表。

如果您不需要可执行代码，这些通常是可取的。

获取可执行函数

递归定义的函数（即primrec或fun）function默认情况下是可执行的（如果在其定义中使用的所有函数也是可执行的）。THE并且SOME通常只能对可枚举域执行（这是您从中得到的错误消息value——nat不可枚举，因为它不是有限的）。

但是，您始终可以为代码生成器提供函数的替代定义。请参阅函数定义教程，特别是关于细化的部分。

如果您更喜欢使用选择运算符进行证明的公式，但也希望您的函数是可执行的，那么最简单的方法可能是证明arg_max_tbvia 选择和sorted_list_of_set等价的定义。然后您可以使用[code_unfold]谓词将选择的定义替换为（可执行）定义sorted_list_of_set

于 2013-05-23T06:29:58.940 回答