我正在阅读 Isabelle 教程，并试图澄清我对 primrec 和 fun 的使用的概念。到目前为止我搜索过的内容，包括答案here https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-August/msg00042.html;我知道 primrec 内部的构造函数只能有一个方程，而 primrec 默认情况下有 [simp]，而 fun 可以有多个方程，并且需要明确指定自动化策略。然而，我仍然很难清楚地理解它。
有哪位好心人能用一些例子来解释一下吗？
primrec does 原始递归 http://en.wikipedia.org/wiki/Primitive_recursive_function在代数数据类型上（或者已经设置为看起来像这样的东西，比如自然数；我对它的内部了解不多）。这意味着您可以拥有的递归方案类型有很多限制：
- 左侧只能有一个非变量参数（即只有一个参数可以进行模式匹配）。你不能做类似的事情
f (x#xs) (y#ys) = … or 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 and primrec就是它fun没有我上面列出的任何限制primrec. With fun，几乎一切顺利。据我所知，一切primrec可以做，fun也可以做。
function还可以做很多其他事情，例如互递归函数、偏函数（即不在所有输入上终止的函数）、条件函数方程等。请参阅功能包手册 http://isabelle.in.tum.de/dist/Isabelle2014/doc/functions.pdf欲了解更多信息。
该机的另一个特点是function命令的优点是它为用它定义的每个函数生成许多有用的规则，例如cases规则，即induction规则，即elims规则等。此外，您还可以使用以下命令自动导出专门的消除规则fun_cases命令。手册中也对此进行了描述。
TL;DR：约阿希姆所说的。fun通常是您想要使用的。如果还不够，请使用function。您可以使用primrec对于非常简单的功能，但这样做并没有真正的优势。对于可能的非终止函数来说，另一种可能有趣的选择是inductive.
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
