How to define a negative number in 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))))

I'm so confused, my negative functions were failed. any idea?

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

user_11479158 · Answer

If you try to use Church encoding define negative number. Use link1 page basic function like cand cor ifthenelse cpair iszero leq... than use link2 page's method use pair define negative number and positive number e.g. pair(true 1) is +1, (false 2) is -2.

Than we use three ifthenelse function build my-add function for two pair number addition.

Use + - 1 * build church-number->n function and pair-to-int function to convert Church number to normal number let us easily check result.

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

How to define a negative number in Racket

1 Answers