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

Question

我正在阅读Isabelle教程，并试图阐明我对使用Primrec和乐趣的概念。到目前为止，我已经搜索了所有内容，包括此处的答案；我知道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。