4-6.rkt

#lang racket

;; CIS352 -- Spring 2023, 4/4 and 4/6/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)))]))
     `(lambda (f) (lambda (x) ,(gen n)))]
    [#t '(lambda (x) (lambda (y) (x (lambda (x) x))))]
    [#f (churchify '(lambda (t f) (f)))]
    [`(let ([,x ,e]) ,eb)
     `((lambda (,x) ,(churchify eb)) ,(churchify e))]
    [(? symbol? x) x]
    [`(if ,e0 ,e1 ,e2)
     (churchify `(,e0 (lambda () ,e1) (lambda () ,e2)))]
    [`(lambda () ,e)
     `((lambda (_) ,(churchify e)) (lambda (x) x))]
    [`(lambda (,x) ,e)
     `(lambda (,x) ,(churchify e))]
    [`(,e-f)
     `(,(churchify e-f) (lambda (x) x))]
    [`(,e-f ,e-a)
     `(,(churchify e-f) ,(churchify e-a))]
    [`(,e0 ,e1 ,e2)
     (churchify `((,e0 ,e1) ,e2))]))

(define (church-compile e)
  (churchify
   `(let ([+ (lambda (n0)
               (lambda (n1)
                 (lambda (f)
                   (lambda (x)
                     ((n1 f) ((n0 f) x))))))])
      ,e)))


;(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)))
        

;; Builtins we covered: succ, plus, times
;; you need to go look up (try Wikipedia) or figure out (on paper) the other ones--many are extra credit
;; car / cdr / cons / null / null? are all in the video / slides

;;(define succ (lambda (n) (lambda (f) (lambda (x) (f ((n f) x))))))

(define plus
  ;; number i'm starting with
  (lambda (n0)
    ;; number i'm adding to n0
    (lambda (n1)
      ;; give me the f that I'm going to apply n0+n1 times
      (lambda (f)
        ;; give me the x that I'm going to apply f to n0+n1 times
        (lambda (x)
          ;; (n1 f) -- a function that applies f to some argument
          ;; n1 times in a row
          ;; (n0 f) -- a function that applies f to some argument
          ;; n0 times in a row
          ((n1 f) ((n0 f) x)))))))

                   ;; number I'm starting with
(define times (lambda (n0)
                      ;; number to which i'm multiplying n0
                (lambda (n1)
                      ;; function i'm doing n0 * n1 times
                  (lambda (f)
                        ;; element I'm calling f on n0 * n1 times
                    (lambda (x)
                      ((n0 (n1 f)) x))))))

;; multi-binding let is really just multi-argument application
;; in another form
(let ([x 1]
      [y 2])
  x)

((lambda (x y) x) 1 2)

(((lambda (x) (lambda (y) x)) (lambda (f) (lambda (x) (f x))))
 (lambda (f) (lambda (x) (f (f x)))))

(church-compile '(+ 5 7)) ;; (e.g., (church->nat (eval (church-compile '(+ 5 7)))) should give you 12)