haskell modulus 원시 재귀

Question

나는 함수 primtive recursive을 사용하여 haskell에서 모듈러스 함수를 만들려고합니다. 나는 그것이 가능하다는 것을 알고있다. (위키 피 디아의 예제 함수 목록에 있기 때문에)

그리고 나는 논리적으로도 그것을 할 수있다. 그러나 나는 그것을 구현할 수 없다!

IE는 논리는 내가 (다시하지 해스켈)

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

하지만 난 그냥 구현할 수없는 것 재귀를 사용하여 정의 할 수 있습니다 (하지 primtive 재귀 또는 하스켈)

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

입니다 그것은 원시 재귀 함수를 사용합니다. I는 내가 할 수 없어 난 정말 내가 그런 (다시하지 해스켈)

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

사람이 할 수 있다면 정의 논리의 일종을 필요로 내 문제를 해결하기 위해 생각 <

(B)의 논리입니다 비트

편집 :: 편집 : 나는 modulus 함수를 나누기를 사용하여 잠재적으로 정의한다고 생각했는데,) * b, 그러나 나눗셈을위한 원시 함수는 modulo에 의존하기 때문에 그것을 할 수 없다. 하하

Answer 1

이에 대한 해결책은

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

입니다 : 다음 페이지에는 내가 원시 재귀 다소 명확 박람회 무슨 생각이 http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Totality#Primitiverecursion

: 원시 재귀의이 개념의 인용에 대한 AGDA 위키를 참조하십시오

Answer 2

일부 포인터는 다음을 참조하십시오. http://www.proofwiki.org/wiki/Quotient_and_Remainder_are_Primitive_Recursive

또한 위키피디아 정의는 다소 좁습니다. 하나의 유한 데이터 구조를 통해 유도 (induction)에 의해 구축 된 함수는 모두 원시적 인 재귀 적 (recursive)이지만 위키 피 디아 (wikipedia)에서 주어진 도구로 변환된다는 것을 보여주기에는 약간의 시간이 걸린다. 클래식 피노 스타일의 원주민을 대표 할 수 있습니다. 당연히 이것을 할 필요는 없지만 유도에 대한 추론은 훨씬 자연 스럽습니다. http://plato.stanford.edu/entries/recursive-functions/#1.3