问题描述
因此,我想定义一个函数(我们将其称为 applied
),该函数将删除另一个多重集中出现的所有子多重集,并用单个元素替换每个出现。例如,
applied {#a,a,c,c#} ({#a,c#},f) = {#f,f#}
所以一开始我尝试了一个定义:
deFinition applied :: "['a multiset,('a multiset × 'a)] ⇒ 'a multiset" where
"applied ms t = (if (fst t) ⊆# ms then plus (ms - (fst t)) {#snd t#} else ms)"
然而,我很快意识到这只会删除一个子集。所以如果我们按照前面的例子,我们会有
applied {#a,c#}
这并不理想。
然后我尝试使用一个函数(我最初尝试过 primrec 和 fun,但前者不喜欢输入的结构,并且 fun 无法证明函数终止。)
function applied :: "['a multiset,('a multiset × 'a)] ⇒ 'a multiset" where
"applied ms t = (if (fst t) ⊆# ms then applied (plus (ms - (fst t)) {#snd t#}) t else ms)"
by auto
termination by (*Not sure what to put here...*)
不幸的是,我似乎无法证明此功能的终止。我试过使用“终止”、自动、fastforce、force 等,甚至是大锤,但我似乎找不到这个功能工作的证据。
我能帮我解决这个问题吗?
解决方法
像这样递归定义它确实有点棘手,因为不能保证终止。如果 fst t = {# snd t #}
或更一般的 snd t ∈# fst t
会怎样?然后你的函数会一直循环运行,永不终止。
在我看来,最简单的方法是进行“一次性”替换的非递归定义:
definition applied :: "'a multiset ⇒ 'a multiset ⇒ 'a ⇒ 'a multiset" where
"applied ms xs y =
(let n = Inf ((λx. count ms x div count xs x) ` set_mset xs)
in ms - repeat_mset n xs + replicate_mset n y)"
我将元组参数更改为柯里式参数,因为根据我的经验,这在实践中更适用于证明——但元组当然也能工作。
n
是 xs
在 ms
中出现的次数。您可以通过检查其他函数的定义来了解它们的作用。
关于 n
也可以更明确一点,写成这样:
definition applied :: "'a multiset ⇒ 'a multiset ⇒ 'a ⇒ 'a multiset" where
"applied ms xs y =
(let n = Sup {n. repeat_mset n xs ⊆# ms}
in ms - repeat_mset n xs + replicate_mset n y)"
缺点是这个定义不再是可执行的——但是这两个应该很容易证明等价。