伊莎贝尔递归函数

Question

我有以下递归函数，它在VDM中创建了一个0的列表(即0，)。怎么能用好玩的方式把翻译成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

我的尝试是可怕的错误，因为我对伊莎贝尔缺乏理解(但下面至少证明了我试过了.)。

伊莎贝尔：

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放在后面的长度为n的0。

但是，当列表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)使用伊莎贝尔/霍尔库的函数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'"