我是 Isabelle 的新手，我正在尝试定义原始递归函数。我已经尝试过加法，但乘法有问题。
datatype nati = Zero | Suc nati
primrec add :: "nati ⇒ nati ⇒ nati" where
"add Zero n = n" |
"add (Suc m) n = Suc(add m n)"
primrec mult :: "nati ⇒ nati ⇒ nati" where
"mult Suc(Zero) n = n" |
"mult (Suc m) n = add((mult m n) m)"
上述代码出现以下错误
类型统一失败：类型“_ ⇒ _”和“nati”的冲突
应用程序中的类型错误：运算符不是函数类型
运算符：mult m n :: nati
操作数：m :: nati
有什么想法吗？
【问题讨论】：
标签： isabelle
问题是你的mult 函数：它应该是这样的：
primrec mult :: "nati ⇒ nati ⇒ nati" where
"mult Zero n = Zero" |
"mult (Suc m) n = add (mult m n) m"
函数式编程/Lambda演算中的函数应用是绑定最强的操作，它关联到左侧：类似f x y的意思是'f应用于x，结果应用于y' -或者，由于 Currying：函数f 应用于参数x 和y。
因此，mult Suc(Zero) n 之类的内容将被读作mult Suc Zero n，即函数mult 必须是一个带有三个参数的函数，即Suc、Zero 和n。这会给你一个类型错误。同样，add ((mult m n) m) 不起作用，因为它与add (mult m n m) 相同，这意味着add 是一个带一个参数的函数，mult 是一个带三个参数的函数。
最后，如果你修复了所有这些，你会得到另一个错误，说你在 mult 函数的左侧有一个非原始模式。您不能在 Suc Zero 之类的东西上进行模式匹配，因为它不是原始模式。如果您使用fun 而不是primrec，则可以这样做，但这不是您想要在这里做的：您想处理Zero 和Suc 的情况（请参阅我的解决方案）。在您的定义中，mult Zero n 甚至是未定义的。
【讨论】：