在Isabelle中定義用於乘法的初始遞歸

Question

我是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)" 

我得到以下錯誤上面的代碼

類型統一失敗：類型「_⇒_」，並在申請「那提」

類型錯誤衝突：不是運營商功能類型

運營商：MULT MN :: NATI

操作數：米:: NATI

任何想法？

Answer 1

的問題是你的mult功能：它應該是這樣的：在函數式編程

primrec mult :: "nati ⇒ nati ⇒ nati" where 
    "mult Zero n = Zero" | 
    "mult (Suc m) n = add (mult m n) m" 

功能的應用程序/λ演算是結合強大的運行和它關聯到左：像f x y手段「 f適用於x，結果適用於y' - 或等同地歸因於柯里格：功能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甚至可能是未定義的。