Isabelle 递归函数

Question

我有以下递归函数，它在 VDM 中创建一个 0 列表（即 [0,...,0]）。如何使用fun-where翻译到Isabelle？

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

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

伊莎贝尔：

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) 指的是什么？我在几个递归函数示例中看到了这一点（尽管没有一个对我有帮助）。

感谢您的帮助！

Answer 1

首先，x 和 xs 是变量。在列表上定义递归函数时，它们通常用于表示列表的第一个元素 (x) 和剩余的列表 (xs)。表达式x # xs 表示“x 附加到列表xs”，这就是您问题中的(x # xs) # [0] 不起作用的原因：x # xs 是一个列表，[0] 也是一个列表。您必须使用x # xs @ [0}，其中@ 是连接两个列表的函数。

现在，对于您的函数：我对您的函数定义的解释是，您有一个自然数 n 和一个列表 l，并希望在列表 l 后面用零填充到长度 @987654336 @。

但是，当列表 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和一个元素并返回一个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'"