Isabelle/HOL 中的 primrec 和 fun 有什么区别？

Question

我正在阅读 Isabelle 教程，并试图澄清我对 primrec 和 fun 的使用的概念。到目前为止我搜索过的内容，包括答案here；我知道 primrec 内部的构造函数只能有一个方程，而 primrec 默认情况下有 [simp]，而 fun 可以有多个方程，并且需要明确指定自动化策略。然而，我仍然很难清楚地理解它。

有哪位好心人可以举例说明吗？

Answer 1

primrec

对代数数据类型（或者已经设置为看起来像一个的东西，比如自然数；我不太了解它的内部结构）进行原始递归。这意味着您可以拥有的递归方案类型有很多限制：

• 左侧只能有一个非变量参数（即只有一个参数可以进行模式匹配）。您不能做类似

  f (x#xs) (y#ys) = …

  或

  f n = (if n = 0 then … else …)

  的事情。
• 您只能在单个构造函数上进行模式匹配（即

  x # xs

  ，但不能

  x # y # xs

  ）
• 您只能在左侧匹配的变量（即

  f (Node l r) = … f l … f r …

  ）上递归调用该函数，但不能对

  f (Node l r) = … f (Node r l) …

  进行调用。
• 嵌套递归仅在反映数据类型的定义时才可能。

fun

来自函数包，是

function

的简化版本，试图证明模式的穷举性、非重叠性和自动终止性。这适用于实践中出现的大多数功能；如果不存在，则必须使用

function

并用手证明这些事情。终止通常是一个棘手的问题。

fun

和

primrec

之间的主要区别在于

fun

没有我上面列出的

primrec

的任何限制。有了

fun

，几乎一切都会顺利。据我所知，

primrec

能做的事情，

fun

也能做。

function

还可以做很多其他事情，例如互递归函数、偏函数（即不在所有输入上终止的函数）、条件函数方程等。有关更多信息，请参阅函数包手册关于这一点。

function

命令的另一个功能是，它为用它定义的每个函数生成许多有用的规则，例如

cases

规则、

induction

规则、

elims

规则等。此外，您可以通过

fun_cases

命令自动导出专门的消除规则。手册中也对此进行了描述。

TL;DR：约阿希姆所说的。

fun

通常是您想要使用的。如果还不够，请使用

function

。您可以使用

primrec

来实现非常简单的功能，但这样做并没有真正的优势。对于可能的非终止函数来说，另一个可能有趣的替代方案是

inductive

。