型付き/ラケット：指定された自然数定義型は、2つの数値を乗算する必要があります。

Question

次の定義された構造体と型には、2つの数値の乗算が必要です。それをするのに困っている。アドバイスをいただければ幸いです。

(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をmultiply-nat（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)))))