Typed/Racket : 주어진 자연수 정의 유형은 두 개의 숫자 함수를 곱해야합니다.

Question

다음과 같이 정의 된 구조와 유형을 곱하면 두 개의 숫자 함수가 작성되어야합니다. 그렇게하는 데 어려움이 있습니다. 모든 조언을 크게 주시면 감사하겠습니다.

(define-struct Zero()) 

(define-struct Succ 
    ([n : Nat])) 

(define-type Nat (U Zero Succ)) 

(: one Nat) 
(define one (Succ (Zero))) 
(: two Nat) 
(define two (Succ one)) 

(: sub-nat : Nat Nat -> Nat) 
    (define (sub-nat a y) 
    (cond 
     [(Zero? a) a] 
     [(eq? one y) 
      (- a y)])) 

(: add-nat (-> Nat Nat Nat)) 
(define (add-nat a b) 
    (cond 
    [(Zero? a) b] 
    ((Zero? b) a) 
    [else (add-nat (Succ-n a) (Succ b))])) 

(: multiply-nat : Number Nat -> Nat) 
(define (multiply-nat a b) 
(cond 
    [(Zero? a) a] 
    [(Zero? b) b] 
    [else 
    (add-nat b (multiply-nat (sub-nat a one) b))])) 

Answer 1

sub-nat 구현이 잘못되어 유형을 확인하지 않습니다. 고칠 수는 있지만 Succ-n을 add-nat과 마찬가지로 으로 사용하는 것이 더 정확합니다. Succ-n은 sub1의 교회 숫자입니다. 여기에 multiply-nat의 수정 (및 테스트) 버전의 : 문제는 함께하지

(: nat->number : Nat -> Nonnegative-Integer) 
(define (nat->number n) 
    (if (Zero? n) 
     0 
     (add1 (nat->number (Succ-n n)))))