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

Question

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

有没有好心人用一些例子来解释一下？

Answer 1

primrec是否primitive recursion在代数数据类型上(或者已经设置为看起来像一个的东西，比如自然数；我对它的内部了解不多)。这意味着您可以拥有的递归方案类型有很多限制:

左侧只能有一个非可变参数(即只有一个可以进行模式匹配的参数)。你不能做类似 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) … .

嵌套递归只有在它反射(reflect)了数据类型的定义时才可能。

fun来自函数包，是 function的简化版试图证明穷举性、模式的非重叠性和自动终止。这适用于实践中出现的大多数功能；如果没有，则必须使用 function并亲手证明这些事情。终止通常是一个棘手的问题。
fun的主要区别和 primrec是 fun没有我上面为 primrec 列出的任何限制.与 fun ，几乎一切都会过去。据我所知，一切 primrec可以做， fun也可以。
function还可以做很多其他的事情，例如互递归函数、偏函数(即不会在所有输入上终止的函数)、条件函数方程等。请参阅 function package manual有关这方面的更多信息。
function的另一个特点命令是它为用它定义的每个函数生成许多有用的规则，例如 cases规则， induction规则， elims规则等。此外，您可以使用 fun_cases 自动派生专门的消除规则。命令。这也在手册中描述。

TL;DR:约阿希姆说的。 fun通常是您想要使用的。如果不够用 function .您可以使用 primrec对于非常简单的功能，但这样做没有真正的优势。另一个可能对非终止函数感兴趣的替代方法是 inductive .