racket - 如何在 Racket 中定义负数

Question

(define my-false
  (lambda (first) (lambda (second) second)))
(define my-true
  (lambda (first) (lambda (second) first)))
(define succ
  (lambda (cn) (lambda (s) ((s my-false) cn))))
(define pred
  (lambda (cn) (cn my-false)))
(define iszero
  (lambda (cn) (cn my-true)))
(define zero
  (lambda (x) x))
(define one
  (lambda (sel) ((sel my-false) zero)))
(define two
  (succ one))
(define three
  (succ two))
(define (easy-add cn1 cn2)
  (if (((iszero cn1) #t) #f)
      cn2
      (easy-add (pred cn1) (succ cn2))))
(define (easy-subtract cn1 cn2)
  (if (((iszero cn2) #t) #f)
      cn1
      (easy-subtract (pred cn1) (pred cn2))))
(define (cn-to-num cn)
  (if (((iszero cn) #t) #f)
      0
      (+ 1 (cn-to-num (pred cn)))))
(define (pos cn)
  (lambda (f)
      ((f cn) zero)))
(define (is-pos n)
  (iszero (n my-false)))
(define pos-cn-to-num
  (lambda (f)(cn-to-num (f my-true))))
(define (neg cn)
    (lambda (f)
      ((f zero) cn)))
(define (is-neg n)
    (iszero (n my-true)))
(define neg-cn-to-num
  (lambda (f)(cn-to-num (f my-false))))

我很困惑，我的消极功能失败了。有什么想法吗？

//try on this on Racket is still return 2 not -2
->>>>(test (neg-cn-to-num (neg two)) -2)

Answer 1

如果您尝试使用 Church 编码定义负数。使用 link1页面基本功能如 cand cor ifthenelse cpair iszero leq... 比使用 link2页面的方法使用对定义负数和正数，例如pair(true 1) 是+1，(false 2) 是-2。

然后我们使用三个ifthenelse 函数构建my-add 函数来进行两对数字相加。

使用+ - 1 *构建church-number->n函数和pair-to-int函数将教堂编号转换为正常数字让我们轻松检查结果。

#lang racket
; basic number
(define zero (λ (f) (λ (x) x)))
(define one (λ (f) (λ (x) (f x))))
(define two (λ (f) (λ (x) (f (f x)))))

(define (church-number->n cn)
  ((cn (λ (x) (+ 1 x))) 0))

(define plus
  (lambda (m)
    (lambda (n)
      (lambda (f)
        (lambda (x)
          ((m f) ((n f) x)))))))

(define pred
  (lambda (n)
    (lambda (f)
      (lambda (x)
        (((n (lambda (g) (lambda (h) (h (g f)))))
          (lambda (u) x))
         (lambda (u) u))))))

(define sub
  (lambda (m)
    (lambda (n)
      ((n pred) m))))

(define mult
  (lambda (m)
    (lambda (n)
      (lambda (f)
        (lambda (x)
          ((m (n f)) x))))))

(define add-1
  (lambda (n)
    (lambda (f)
      (lambda (x) (f ((n f) x))))))

(define true
  (lambda (x)
    (lambda (y)
      x)))

; logic function
;FALSE := λx.λy.y
(define false
  (lambda (x)
    (lambda (y)
      y)))

;AND := λp.λq.p q p
(define cand
  (lambda (p)
    (lambda (q)
      ((p q) p))))

;NOT := λp.p FALSE TRUE
(define cnot
  (lambda (p)
    ((p false) true)))

;IFTHENELSE := λp.λa.λb.p a b
(define ifthenelse
  (lambda (p)
    (lambda (a)
      (lambda (b)
        ((p a) b)))))

;ISZERO := λn.n (λx.FALSE) TRUE
;; returns true if n is zero, false otherwise
(define iszero
  (lambda (n)
    ((n (lambda (x) false)) true)))

;LEQ := λm.λn.ISZERO (SUB m n)
;; returns true if m <= n, false otherwise
(define leq
  (lambda (m)
    (lambda (n)
      (iszero ((sub m) n)))))

; pair related function
(define cpair
  (lambda (x)
    (lambda (y)
      (lambda (f)
        ((f x) y)))))

;FIRST := λp.p TRUE
;; returns first element of a cpair (x, y)
(define cfirst
  (lambda (p)
    (p true)))

;SECOND := λp.p FALSE
;; returns the second element of a cpair (x, y)
(define csecond
  (lambda (p)
    (p false)))

(define posi
  (lambda (a)
    ((cpair true) a)))

(define minus
  (lambda (a)
    ((cpair false) a)))

(define pair-lessthan?
  (lambda (a)
    (lambda (b)
      (cnot ((leq (csecond b)) (csecond a))))))

(define pair-less-zero?
  (lambda (pair-n)
    ((cand (cnot (iszero (csecond pair-n)))) (cnot (cfirst pair-n)))))

(define my-add
  (lambda (a)
    (lambda (b)
      (((ifthenelse (pair-less-zero? a))
        (((ifthenelse (pair-less-zero? b))
          (minus ((plus (csecond a)) (csecond b)))) ; "a<0∧b<0"
         (((ifthenelse ((pair-lessthan? a) b))
           (posi ((sub (csecond b)) (csecond a)))) ; "a<0∧b≥0∧|a|<|b|"
          (minus ((sub (csecond a)) (csecond b)))))) ; "a<0∧b≥0∧|a|≥|b|"

       (((ifthenelse (pair-less-zero? b))
         (((ifthenelse ((pair-lessthan? a) b))
           (minus ((sub (csecond b)) (csecond a)))) ; "a≥0∧b<0∧|a|<|b|"
          (posi ((sub (csecond a)) (csecond b))))) ; "a≥0∧b<0∧|a|≥|b|"
        (posi ((plus (csecond a)) (csecond b)))))))) ; "a≥0∧b≥0"

(define pair-to-int
  (lambda (p)
    (* (((ifthenelse (cfirst p)) 1) (- 1))
       (church-number->n (csecond p)))))

;;; TEST
(define five ((plus (add-1 two)) two))
(define ten ((mult two) five))
(define p-0 (posi zero))
(define m-0 (minus ((sub ((sub ten) five)) five)))
(define p-5 (posi five))
(define p-10 (posi ten))
(define m-5 (minus five))
(define m-10 (minus ten))

(pair-to-int ((my-add p-10) p-5))
(pair-to-int ((my-add p-5) p-10))
(pair-to-int ((my-add m-5) m-10))
(pair-to-int ((my-add m-10) m-5))

(pair-to-int ((my-add p-5) m-5))
(pair-to-int ((my-add m-5) p-5))
(pair-to-int ((my-add p-0) p-0))
(pair-to-int ((my-add m-0) m-0))
(pair-to-int ((my-add m-0) p-0))
(pair-to-int ((my-add p-0) m-0))

(pair-to-int ((my-add m-5) p-10))
(pair-to-int ((my-add m-10) p-5))
(pair-to-int ((my-add p-10) m-5))
(pair-to-int ((my-add p-5) m-10))
(pair-to-int ((my-add ((my-add p-5) m-10)) p-5))