Created
March 28, 2024 16:19
-
-
Save kmicinski/dbd22135e55476d67aa3afafed0bf2e6 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#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)))))) | |
;; 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)] | |
[`(add1 ,e0) | |
`(,church-add1 ,(scheme->λ e0))] | |
;; to Church encode a single-argument λ, I just need to encode its 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))])) | |
;; 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) | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment