我正在使用向量作为函数的自定义实现,其域是自然数的有限“索引集”,并且其图像是某种可以定义最大值的类型,通常是 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
这会不会是因为列表构造函数被定义为数据类型
,而有限集仅被定义为归纳
方案?
随便——你知道在有限集上定义这个函数的方法吗?是直接写下来,还是通过一些类似折叠的实用函数?
最佳答案
折叠有限集要求结果与访问集合元素的顺序无关,因为集合是无序的。关于 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
定义的所有内容推导出专门的代码方程式.请参阅有关程序优化的代码生成器教程。
关于list - 在有限集上定义一个类似于 "arg max"的函数,并证明它的一些属性,并避免通过列表绕道而行,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/16702866/