module de hachage récursivité primitive

Question

J'essaie de créer une fonction de module dans haskell en utilisant primtive recursive fonctions. Je sais que c'est possible (parce que c'est sur la liste des exemples de fonctions sur wikipedia)

Et je sais comment je ferais logiquement aussi .. Mais je ne peux pas l'implémenter!

IE, la logique est (non récursivité primtive ou haskell)

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

Ce que je peux définir l'aide récursion (encore une fois pas Haskel)

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

Mais je ne peux pas sembler mettre en œuvre en utilisant des fonctions récursives primitives. Je peu que je ne peux pas faire est la logique d'un < b

Je pense vraiment résoudre mon problème je besoin d'une sorte de logique définie comme la (encore une fois non Haskel)

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

Si quelqu'un pouvait aidez-moi avec une partie de ceci je l'apprécierais vraiment, merci

Edit :: Je pensais à potentiellement définir une fonction de module en utilisant la division, à savoir mod (a, b) = a - (a/b) * b, mais puisque ma fonction récursive primitive pour diviser repose sur modulo je ne peux pas le faire haha ​​

Answer 1

La solution est

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

Jetez un oeil à cela pour quelques pointeurs: http://www.proofwiki.org/wiki/Quotient_and_Remainder_are_Primitive_Recursive

Notez également que la définition de wikipedia est quelque peu étroite. Toute fonction construite par induction sur une structure de données finie unique est récursive primitive, bien qu'il faille un peu montrer que cela se traduit par les outils donnés dans wikipedia. Et notez que nous pouvons représenter les naturels dans le style peano classique. Vous n'avez pas à le faire bien sûr, mais cela rend le raisonnement sur l'induction beaucoup plus naturel. Voir le wiki agda pour une citation de cette notion de récursion primitive: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Totality#Primitiverecursion

La page suivante a aussi ce que je pense est une exposition un peu plus claire de la récursion primitive: http://plato.stanford.edu/entries/recursive-functions/#1.3