04-02-24.rkt

#lang racket

;; The Church-encoded number N is represented as:
;; - A function (λ (f) ...) which takes a function f
;; - Returns a function which accepts an argument x
;;   and applies f N times to x

;; two, Church-encoded as a *Racket* lambda
(λ (f) (λ (x) (f (f x))))

;; for your project 4, you will return a quoted expression which
;; will be evaluated using eval

;; This is an example of what the project should output for
;; the literal 2
(define church-encoded-two '(λ (f) (λ (x) (f (f x)))))

;; (((eval church-encoded-two (make-base-namespace)) add1) 0)

;; Now, if you give me a Racket lambda which represents
;; the Church-encoded number N, I can translate it to
;; a Racket natural (nonnegative-integer?) by doing this:
(define (church->nat N)
  ((N add1) 0))

(define church-add1-racket-λ (λ (N) (λ (f) (λ (x) (f ((N f) x))))))

;; INPUT language
(define (scheme-ir? e)
  (match e
    [(? number? n) #t]
    [`(add1 ,(? scheme-ir? e)) #t]
    [(? symbol? x) #t]
    [`(lambda ,(? symbol? x) ,(? scheme-ir? e-body)) #t]
    [`(,(? scheme-ir? e0) ,(? scheme-ir? e1)) #t]
    [_ #f]))

;; OUTPUT language
;; Your output MUST be in the λ calculus, with
;; no exceptions
;; We're doing this because we want to understand
;; how to systematically translate all of Racket
;; into *just* the λ calculus. If we know we can do it
;; we've proven that the λ calculus is Turing complete
(define (λ? e)
  (match e
    [(? symbol? x) #t]
    [`(lambda (,(? symbol? x)) ,(? λ? e-body)) #t]
    [`(,(? λ? e0) ,(? λ? e1)) #t]
    [_ #f]))

;; output the Church encoded form of the literal number N
(define (church-literal-N N)
  (define (h n)
    (if (= n 0)
        'x
        `(f ,(h (- n 1)))))
  `(lambda (f) (lambda (x) ,(h N))))

(define church-add1 '(lambda (N) (lambda (f) (lambda (x) (f ((N f) x))))))
(define church-+ '(lambda (N0)
                    (lambda (N1)
                      (lambda (f) (lambda (x)
                                    ((n1 f) ((n0 f) x)))))))


#;(define church-empty-list (scheme->λ '(lambda (when-cons when-null) (when-null))))
#;(define church-cons (scheme->λ '(lambda (the-car the-cdr)
                                    (lambda (when-cons when-null) (when-cons the-car the-cdr)))))
;; Let's start building some of project 4
(define/contract (scheme->λ e)
  (-> any/c λ?)
  
  (match e
    ;; I need to produce a quoted output, *not* a Racket lambda 
    [(? number? n)
     (church-literal-N n)]
    #;[''() church-empty-list]
    #;[`(cons ,e0 ,e1)
     (scheme->λ `(,church-cons ,e0 ,e1))]
    [`(add1 ,e0)
     `(,church-add1 ,(scheme->λ e0))]
    [`(+ ,e0 ,e1)
     ;; this is a mistake because it's a 2-argument call,
     ;; but the λC allows for one-argument calls only
     #;`(,church-+ ,(scheme->λ e0) ,(scheme->λ e1))
     `((,church-+ ,(scheme->λ e0)) ,(scheme->λ e1))]
    ;; to Church encode a single-argument λ, I just need to encode its body
    [`(lambda () ,e-body) `(lambda (_) ,(scheme->λ e-body))]
    [`(lambda (,x) ,e-body)
     `(lambda (,x) ,(scheme->λ e-body))]
    [`(lambda (,x ,y) ,e-body)
     `(lambda (,x) (lambda (,y) ,(scheme->λ e-body)))]
    ;; Variables are already in the λ calculus
    [(? symbol? x) x]
    ;; To handle a single-argument call, I just have to Church encode
    ;; e0 and e1.
    [`(,e0 ,e1 ,e2)
     `((,(scheme->λ e0) ,(scheme->λ e1)) ,(scheme->λ e2))]
    [`(,e0 ,e1)
     `(,(scheme->λ e0) ,(scheme->λ e1))]
    [`(,e0) `(,(scheme->λ e0) (lambda (x) x))]))

;; In the λ calculus, there's no immediate way to handle multiple arguments
;; every function is of a single argument

;; N + K shows that + has to be a binary operator, it needs two arguments
;; unlike add1. So we must have some way to call functions with more than
;; one argument. We also know we need this because we need to Church-encode
;; functions of multiple arguments in project 4.

;; The answer is to use currying, which turns functions of multiple arguments
;; into a function that takes the first argument, and returns a function
;; that takes the next argument, and so on, until only one argument left
;; at which point it's just a normal λ calculus λ.

;; So the function of two arguments:
(λ (x y) x)

;; Would be curried (and in our case, Church encoed) as:
(λ (x) (λ (y) x))

;; Instead of writing
((λ (x y) x) 1 2)

;; I have to write
(((λ (x) (λ (y) x)) 1) 2)

;; Church-encoded lists
;; A Church-encoded list is a λ of two (curried) arguments

;; Church encoded numbers
;; add1, +, need to put the definition of * on slack too
;; lists and bools
;; letrec we left until Thursday