0

给定以下定义的结构和类型，需要编写乘以两个数字的函数。很难做到这一点。任何建议将不胜感激。

(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))]))
4

1 回答 1

1

您的sub-nat实现不正确，不会进行类型检查。Succ-n虽然你可以解决这个问题，但从语义上来说，只在你的multiply-nat（就像你做的那样）中使用更正确add-nat，因为Succ-n是教堂数字等价于sub1. 这是一个更正（和测试）的版本multiply-nat：

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

出于测试目的，我还编写了一个nat->number将 Church 数字转换为实际数字的函数：

(: nat->number : Nat -> Nonnegative-Integer)
(define (nat->number n)
  (if (Zero? n)
      0
      (add1 (nat->number (Succ-n n)))))
于 2016-07-10T19:57:45.833 回答