Isabelleでの乗算のためのPrimtive Recursionの定義

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

は私が

タイプの統一に失敗した上記のコードのために、次のエラーを取得：「_⇒_」およびアプリケーションの「NATI」

タイプエラータイプのクラッシュ：演算子ではありませんの関数型

演算子：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 'に適用されるか、または同等にCurryingのために、xおよびyに適用される関数fが適用されます。

したがって、mult Suc(Zero) nようなものがmult Suc Zero nとして読み出されることになる、すなわち機能mult 3つのパラメータ、すなわちSuc、Zero、及びnをとる関数でなければならないであろう。それはあなたに型エラーを与えます。同様にadd ((mult m n) m)はadd (mult m n m)と同一であるため機能しません。これは、addが1つのパラメータを取る関数であり、multが3つを取る関数であることを意味します。

最後に、すべてを修正すると、mult関数の左側に非プリミティブなパターンがあるという別のエラーが発生します。 Suc Zeroなどのパターンマッチングはプリミティブパターンではないため、パターンマッチングできません。 primrecの代わりにfunを使用するとできますが、ここでやりたいことではありません。代わりにケースZeroとSuc（私の解決策を参照）を処理したいとします。あなたの定義では、mult Zero nは未定義です。