ricorsione primitiva modulo haskell

Question

Sto provando a creare una funzione modulo all'interno di haskell usando le funzioni primtive recursive. So che è possibile (perché è sulla lista delle funzioni di esempio su wikipedia)

E so come lo farei anche io logicamente .. Ma non riesco proprio ad implementarlo!

IE, la logica è (non ricorsione primtive o Haskell)

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

Che posso definire utilizzando la ricorsione (ancora una volta non Haskel)

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

Ma io proprio non riesco a implementare usando le funzioni ricorsive primitive. Mi morsi che non posso fare è la logica di una < b

Credo che per risolvere davvero il mio problema ho bisogno di un qualche tipo di logica definita come (ancora una volta non Haskel)

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

se qualcuno potrebbe aiutatemi con qualsiasi parte di questo lo apprezzerei molto, grazie

Modifica :: Ho pensato di definire potenzialmente una funzione modulo facendo uso della divisione, cioè mod (a, b) = a - (a/b) * b, ma poiché la mia funzione ricorsiva primitiva per divisione si basa su modulo I non può farlo haha ​​

Answer 1

La soluzione a questo è

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

Dai uno sguardo a questo per alcuni suggerimenti: http://www.proofwiki.org/wiki/Quotient_and_Remainder_are_Primitive_Recursive

Inoltre, la definizione di wikipedia è alquanto limitata. Qualsiasi funzione creata per induzione su una singola struttura di dati finiti è ricorsiva primitiva, anche se ci vuole un po 'per mostrare che questo si traduce negli strumenti forniti in wikipedia. E nota che possiamo rappresentare i naturali nel classico stile peano. Non devi farlo ovviamente, ma rende molto più naturale il ragionamento sull'induzione. Vedere il wiki agda per una citazione di questa nozione di ricorsione primitiva: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Totality#Primitiverecursion

la seguente pagina ha anche quello che penso è un'esposizione un po 'più chiara di ricorsione primitiva: http://plato.stanford.edu/entries/recursive-functions/#1.3