CODEWITHSUNDEEP
isabelle
Perseus14
Perseus14

Reputation: 487

Defining Primtive Recursion for multiplication in Isabelle

I am new to Isabelle and I am trying to define primitive recursive functions. I have tried out addition but I am having trouble with multiplication.

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

I get the following error for the above code

Type unification failed: Clash of types "_ ⇒ _" and "nati"

Type error in application: operator not of function type

Operator: mult m n :: nati

Operand: m :: nati

Any ideas?

Upvotes: 1

Views: 249

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8258

The problem is your mult function: It should look like this:

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

Function application in functional programming/Lambda calculus is the operation that binds strongest and it associates to the left: something like f x y means ‘f applied to x, and the result applied to y’ – or, equivalently due to Currying: the function f applied to the parameters x and y.

Therefore, something like mult Suc(Zero) n would be read as mult Suc Zero n, i.e. the function mult would have to be a function taking three parameters, namely Suc, Zero, and n. That gives you a type error. Similarly, add ((mult m n) m) does not work, since that is identical to add (mult m n m), which would mean that add is a function taking one parameter and mult is one taking three.

Lastly, if you fix all that, you will get another error saying you have a non-primitive pattern on the left-hand side of your mult function. You cannot pattern-match on something like Suc Zero since it is not a primitive pattern. You can do that if you use fun instead of primrec, but it is not what you want to do here: You want to instead handle the cases Zero and Suc (see my solution). In your definition, mult Zero n would even be undefined.

Upvotes: 2

Related Questions