Primitive recursion of haskell module module

Question

I am trying to create a module function in haskell using primitive recursive functions . I know this is possible (because it is on the list of function examples on wikipedia)

And I know how I logically do this. But I just can’t realize it!

IE, logic (not primitive recursion or haskell)

function mod(a, b){ while(a > b) a -= b return a; } 

What can I determine with recursion (again not haskel)

 function mod(a, b){ if(a < b) return a; return mod(a - b, b); } 

But I just can't implement it with primitive recursive functions. I beat what I can’t do, this is the logic <b

I think that to solve my problem I need some kind of specific logic, such as (again not haskel)

 reduce(a, b) = a >= b -> ab otherwise x 

If anyone could help me with any part of this, I would really appreciate it, thanks

Edit :: I was thinking about the potential definition of a module function using division, i.e. Mod (a, b) = a - (a / b) * b, but since my primitive recursive division function relies on modulo, I cannot do this haha

Answer 1

The solution to this is

 mod(0, y) = zero(y) mod(x, 0) = zero(x) mod(x + 1, y) = mult3(succ(mod(x, y)), sign(y), notsign(eq(mod(x, y), diff(y, 1)))) 

Answer 2

Take a look at this for some pointers: http://www.proofwiki.org/wiki/Quotient_and_Remainder_are_Primitive_Recursive

Also note that the definition of Wikipedia is somewhat narrow. Any function created by induction on one finite data structure is primitive recursive, although it takes a little to show that this translates to the tools provided on Wikipedia. And note that we can represent straight people in the classic peano style. Of course, you do not have to do this, but it makes the argument about induction more natural. See Wiki agda for a quote on this concept of primitive recursion: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Totality#Primitiverecursion

The next page also has what I consider to be a slightly clearer statement of primitive recursion: http://plato.stanford.edu/entries/recursive-functions/#1.3