伊莎贝尔递归函数

Question

我有以下递归函数，它在 VDM 中创建一个 0 列表（即 [0,...,0]）。这怎么可能 translated to Isabelle using fun-where?

VDM:

NewList: nat1 * seq of nat -> seq of nat
NewList(n, l) == 
    if len l = n then l
    else NewList(n, l ^ [0])
-- pre/post-conditions excluded here

由于我对伊莎贝尔缺乏了解，我的尝试大错特错（但下面至少证明我尝试过...）。

伊莎贝尔：

fun
  NewList:: "N ⇒ (VDMNat VDMSeq) ⇒ (VDMNat VDMSeq)"
where
  "NewList n [] = NewList n [0]"
| "NewList n [x] = (if len [x] = n then [x] else NewList n (x#[0]))"
| "NewList n (x # xs) = (if len (x # xs) = n then (x # xs) else NewList n ((x # xs) # [(0::VDMNat)]))"

*数据类型VDMNat和VDMSeq在一些库中定义。请暂时忽略 VDMNat 和 VDMSeq - 欢迎使用 Isabelle 的数据类型进行任何类型的实现（至少它会为我的实现提供一个很好的参考）。有关预期的数据类型，请参阅 VDM 代码。

能否请您解释一下 x、xs 和 (x # xs) 指的是什么？我在几个递归函数示例中看到了这一点（尽管 none 帮助了我）。

感谢您的帮助！

Answer 1

首先，x和xs是变量。在列表上定义递归函数时，这些通常用于表示列表的第一个元素 (x) 和其余列表 (xs)。表达式 x # xs 表示“x 放在列表 xs 前面”，这就是为什么 (x # xs) # [0] 在您的问题中不起作用的原因：x # xs 是一个list 并且 [0] 也是一个列表。您必须执行 x # xs @ [0}，其中 @ 是连接两个列表的函数。

现在，对于你的函数：我对你的函数定义的解释是你有一个自然数 n 和一个列表 l 并且想要用零填充列表 l后面的长度为 n.

但是，当列表 l 的开头长度为 > n 时，您的函数不会终止。在这种情况下，您将不得不考虑该怎么做。

以下是我对您可以做什么的建议：

可能性 1

将 = n 更改为 ≥ n。然后你可以通过查看

来证明函数的终止

function new_list :: "nat ⇒ nat list ⇒ nat list" where
  "new_list n l = (if length l ≥ n then l else new_list n (l @ [0]))"
by pat_completeness auto
termination by (relation "measure (λ(n, l). n - length l)") auto

然而，证明关于这个的定理可能会变得很糟糕。因此，我会敦促你做类似以下两种可能性的事情。理想情况下，使用 Isabelle 标准库中的函数，因为它们通常有很好的自动化设置。或者，为您的数据类型定义您自己的小构建块（如 take 和 replicate），并证明它们的可重用事实并将它们组合起来以执行您想要的操作。像你这样的“整体”函数定义在做证明时很难处理。

可能性 2

使用内置函数 replicate，它接受一个自然数 n 和一个元素以及 returns 一个 n 乘以该元素的列表：

definition new_list :: "nat ⇒ nat list ⇒ nat list" where
  "new_list n l = l @ replicate (n - length l) 0"

您也可以用 fun 做同样的事情，但 definition 是更底层的工具。请注意，definition 并未添加函数定义定理 new_list_def 作为简化规则；你可以写 declare new_list_def [simp].

可能性 3

您可以将可能性 2 与内置函数 take 结合起来，以确保您总是得到一个长度恰好的列表n，即使输入列表较长（然后可能被截断）：

definition new_list :: "nat ⇒ nat list ⇒ nat list" where
  "new_list n l = take n l @ replicate (n - length l) 0"

总结

前两种情况，你可以证明定理

length l ≤ n ⟹ length (new_list n l) = n
take (length l) (new_list n l) = l

（在第一种情况下使用new_list.induct进行归纳；在第二种情况下只需展开定义并简化）

第三种情况，可以证明

length (new_list n l) = n
take (length l) (new_list n l) = take n l

显然，如果length l ≤ n，前两个和最后一个完全重合

Answer 2

简单的解决方案是：replicate n (0::nat) 使用 Isabelle/HOL 库中的函数 replicate。

如果您想通过 fun 自己实现该功能，那么请按照您在函数式编程中始终应该做的事情去做；) 尝试将您的问题拆分为可以递归解决的较小问题：

fun newlist :: "nat => nat list"
where
  "newlist 0 = []" -- "the only list of length 0*)
| "newlist (Suc n) = ..." -- "use result for 'n' to obtain result for 'n+1'"

伊莎贝尔递归函数

Isabelle recursive function

recursion

isabelle

可能性 1

可能性 2

可能性 3

总结