p4-starter.rkt

#lang racket

;; CIS352 -- Spring 2023, 4/4/2023
;; Beginning to the Church encoding project

;; output
(define (lambda-calculus? e)
  (match e
    [(? symbol? x) #t]
    [`(lambda (,(? symbol? x)) ,(? lambda-calculus? e-body)) #t]
    [`(,(? lambda-calculus? e-f) ,(? lambda-calculus? e-a)) #t]
    [_ #f]))

;; Let's assume you have this encoding, and now
;; you want to transform it to plain Racket
;; i.e., your input is a procedure? and your output
;; is a Racket number?
(define (church->nat church-encoded-number)
  ((church-encoded-number add1) 0))


;; going to take a program in (a subset of) Racket
(define (churchify e)
  (match e
    ;; generate the church-encoded number n
    ;; assuming n is a natural, i.e., >= 0
    [(? number? n)
     ;; generate (f (f (f ... (f x)...)))
     ;; if n = 0, return x
     ;; if n > 0, return (f y) where y = (gen (- n 1))
     (define (gen n)
       (match n
         [0 'x]
         [n `(f ,(gen (- n 1)))]))
     `(λ (f) (λ (x) ,(gen n)))]
    [(? symbol? x) x]
    [`(lambda (,x) ,e)
     `(lambda (,x) ,(churchify e))]
    [`(,e-f ,e-a)
     `(,(churchify e-f) ,(churchify e-a))]
    [`(let ([,x ,e]) ,eb)
     (pretty-print eb)
     (pretty-print e)
     `((lambda (,x) ,(churchify eb)) ,(churchify e))]))

(define (church-compile e)
  (churchify
   `(let ([add1 (lambda (n) (lambda (f) (lambda (x) (f ((n f) x)))))])
      ,e)))

(church-compile '(let ([x (add1 5)])
                   (let ([y (add1 x)])
                     y)))


;(churchify '(let ([add1 (λ (n) (λ (f) (λ (x) (f ((n f) x)))))]) (add1 5)))
;(churchify '((λ (add1) (add1 5)) (λ (n) (λ (f) (λ (x) (f ((n f) x)))))))

;;(church->nat (eval '((λ (add1) (add1 (λ (f) (λ (x) (f (f (f (f (f x)))))))))
;;                     (λ (n) (λ (f) (λ (x) (f ((n f) x))))))))
  
(define example-e
  '(let ([x 5])
     (let ([y (add1 x)])
       (add1 y))))


;; This is the chruch-encoded number 0
(λ (f) (λ (x) x))

;; This is the church-encoded number 1
(λ (f) (λ (x) (f x)))

;; This is two
(λ (f) (λ (x) (f (f x))))

;; This is three
(λ (f) (λ (x) (f (f (f x)))))

;; This is four
(λ (f) (λ (x) (f (f (f (f x))))))

;; This is five
(λ (f) (λ (x) (f (f (f (f (f x)))))))



;;(((λ (f) (λ (x) (f (f (f (f (f x)))))))
;;  add1)
;; 0)

;;((λ (x) (add1 (add1 (add1 (add1 (add1 x))))))
;; 0)

(add1 (add1 (add1 (add1 (add1 0)))))

;; let's define the successor function
(define succ
  ;; this takes an f and an x and applies f to x n times in a row
  (λ (n)
    ;; this is the function we are going to apply n+1 times
    (λ (f)
      ;; this is the value x to which we are going to apply f n+1 times
      (λ (x)
        ;; calculate a function that applies f n times, and then
        ;; apply that to x
        ;; then, apply f to that whole result once more
        (f ((n f) x))))))

;; another way to write the body
        #;(let ([apply-f-n-times (n f)])
          (let ([result-of-applying-f-n-times-to-x (apply-f-n-times x)])
            (f result-of-applying-f-n-times-to-x)))