Created
November 29, 2022 21:44
-
-
Save kmicinski/b59591f1b2c4cb0f143714b179fe2d21 to your computer and use it in GitHub Desktop.
This file contains hidden or 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 | |
;; Assignment 4: A church-compiler for Scheme, to Lambda-calculus | |
(provide church-compile | |
; provided conversions: | |
church->nat | |
church->bool | |
church->listof) | |
;; Input language: | |
; | |
; e ::= (letrec ([x (lambda (x ...) e)]) e) | |
; | (let ([x e] ...) e) | |
; | (let* ([x e] ...) e) | |
; | (lambda (x ...) e) | |
; | (e e ...) | |
; | x | |
; | (and e ...) | (or e ...) | |
; | (if e e e) | |
; | (prim e) | (prim e e) | |
; | datum | |
; datum ::= nat | (quote ()) | #t | #f | |
; nat ::= 0 | 1 | 2 | ... | |
; x is a symbol | |
; prim is a primitive operation in list prims | |
; The following are *extra credit*: -, =, sub1 | |
(define prims '(+ * - = add1 sub1 cons car cdr null? not zero?)) | |
;; we can remember (and e0 e1) is really (let ([v e0]) (if v e1 v)) | |
;; (or e0 e1) is really (let ([v e0]) (if v v e1)) | |
;; (if e0 e1 e2) gets translated to | |
;; ((e0 (lambda () e1)) (lambda () e2)) | |
;; it's helpful to use the encoder on "partial" encodings, things that need some encoding | |
;; but you need to be careful to make sure you don't hit nontermination. | |
; This input language has semantics identical to Scheme / Racket, except: | |
; + You will not be provided code that yields any kind of error in Racket | |
; + You do not need to treat non-boolean values as #t at if, and, or forms | |
; + primitive operations are either strictly unary (add1 sub1 null? zero? not car cdr), | |
; or binary (+ - * = cons) | |
; + There will be no variadic functions or applications---but any fixed arity is allowed | |
;; Output language: | |
; e ::= (lambda (x) e) | |
; | (e e) | |
; | x | |
; | |
; also as interpreted by Racket | |
;; Using the following decoding functions: | |
; A church-encoded nat is a function taking an f, and x, returning (f^n x) | |
(define (church->nat c-nat) | |
((c-nat add1) 0)) | |
; A church-encoded bool is a function taking a true-thunk and false-thunk, | |
; returning (true-thunk) when true, and (false-thunk) when false | |
(define (church->bool c-bool) | |
((c-bool (lambda (_) #t)) (lambda (_) #f))) | |
; A church-encoded cons-cell is a function taking a when-cons callback, and a when-null callback (thunk), | |
; returning when-cons applied on the car and cdr elements | |
; A church-encoded cons-cell is a function taking a when-cons callback, and a when-null callback (thunk), | |
; returning the when-null thunk, applied on a dummy value (arbitrary value that will be thrown away) | |
(define ((church->listof T) c-lst) | |
; when it's a pair, convert the element with T, and the tail with (church->listof T) | |
((c-lst (lambda (a) (lambda (b) (cons (T a) ((church->listof T) b))))) | |
; when it's null, return Racket's null | |
(lambda (_) '()))) | |
;; Write your church-compiling code below: | |
; churchify recursively walks the AST and converts each expression in the input language (defined above) | |
; to an equivalent (when converted back via each church->XYZ) expression in the output language (defined above) | |
;; n = 0 -> (lambda (f) (lambda (x) x)) | |
;; n = 1 -> (lambda (f) (lambda (x) (f x))) | |
;; n = 2 -> (lambda (f) (lambda (x) (f (f x)))) | |
(define (nat->church n) | |
;; generates (f (f ... (f n))...) | |
(define (generate n) | |
(if (= n 0) | |
'x | |
`(f ,(generate (- n 1))))) | |
`(lambda (f) (lambda (x) ,(generate n)))) | |
;; input is assumed to satisfy the language specified above... | |
;; output needs to be some quoted expression in the λ-calculus | |
;; example: '((lambda (x) x) (lambda (y) y)) | |
(define (churchify e) | |
(match e | |
; Tagged expressions | |
[`(letrec ([,f (lambda (,args ...) ,e0)]) ,e1) | |
(churchify `(let ([,f (Y-comb (lambda @,args ,e0))]) ,e1))] | |
[`(let () ,e1) | |
;; wrong | |
(churchify e1)] | |
[`(let ([,xs ,e0s] ...) ,e1) | |
;; if input is '(let ([x 1] [y 2] [z 3]) e1) | |
;; xs is something like '(x y z) | |
;; e0s is something like '(1 2 3) | |
;; I know I can make the expression "simpler" -- by using multi-arg lambdas, | |
;; and then multi-argument calls | |
(churchify `((lambda ,xs ,e1) ,@e0s))] | |
[`(let* () ,e1) | |
(churchify e1)] | |
[`(let* ([,x0 ,e0] ,rest ...) ,e1) | |
;; "pull off" one binding pair, handle the rest down the line | |
;; eventually, you'll get `(let () ,e1) and that will be handled | |
;; by the previous case... | |
(churchify `(let ([,x0 ,e0]) (let ,rest ,e1)))] | |
[`(lambda () ,e0) | |
`(lambda (_) ,e0)] | |
[`(lambda (,x) ,e0) | |
`(lambda (,x) ,(churchify e0))] | |
[`(lambda (,x . ,rest) ,e0) | |
(churchify `(lambda (,x) (lambda ,rest ,e0)))] | |
[`(and) (churchify '#t)] | |
[`(and ,e0 ,rest ...) (churchify `(if ,e0 (and ,@rest) #f))] | |
[`(or) (churchify '#f)] | |
[`(or ,e0 ,rest ...) | |
;; similar to multi-and | |
'todo] | |
[`(if ,e0 ,e1 ,e2) | |
(churchify `(,e0 (lambda () ,e1) (lambda () ,e2)))] | |
; Variables | |
[(? symbol? x) x] | |
; Datums | |
[(? natural? nat) | |
(nat->church nat)] | |
[''() '(lambda (when-cons) (lambda (when-null) (when-null (lambda (x) x))))] | |
[#t 'todo] | |
[#f 'todo] | |
[`(,fun) | |
(churchify `(,fun (lambda (x) x)))] | |
[`(,fun ,arg) | |
`(,(churchify fun) ,(churchify arg))] | |
[`(,fun ,arg . ,rest) | |
(churchify `((,fun ,arg) ,@rest))])) | |
;; examples with U/Y | |
;; (+ 1 2) | |
;; ((+ 1) 2) | |
;;((+ (lambda (f) (lambda (x) (f x)))) | |
;; (lambda (f) (lambda (x) (f (f x))))) | |
;; calls churchify with some scaffolding of builtin expressions. | |
(define (church-compile program) | |
(define Y-comb `((lambda (u) (u u)) (lambda (y) (lambda (mk) (mk (lambda (x) (((y y) mk) x))))))) | |
(define church:add1 `(lambda (n0) (lambda (f x) (f ((n0 f) x))))) | |
(define church:+ `(lambda (n0 n1) (lambda (f x) ((n1 f) ((n0 f) x))))) | |
(define church:* `(lambda (n0 n1) (lambda (f) (lambda (x) ((n0 (n1 f)) x))))) | |
(churchify | |
`(let ([Y-comb ,Y-comb]) | |
,program))) | |
(letrec ([f (lambda (x) | |
(if (= x 0) | |
1 | |
(* x (f (sub1 x)))))]) | |
(f 20)) | |
;; if x = 0, return 1 | |
;; if x = 1, return 1 | |
;; otherwise, return f(x-1) + f(x-2) | |
(define (fib-using-letrec x) | |
(letrec ([fib (lambda (x) | |
(cond [(= x 0) 1] | |
[(= x 1) 1] | |
[else (+ (fib (- x 1)) (fib (- x 2)))]))]) | |
(fib x))) | |
(define (fib-using-Y x) | |
(define Y-comb ((lambda (u) (u u)) | |
(lambda (y) (lambda (mk) (mk (lambda (x) (((y y) mk) x))))))) | |
(let ([fib (Y-comb | |
(lambda (fib) | |
(lambda (x) | |
(cond [(= x 0) 1] | |
[(= x 1) 1] | |
[else (+ (fib (- x 1)) (fib (- x 2)))]))))]) | |
(fib x))) | |
(define U (lambda (f) (f f))) | |
(define (fib-using-U x) | |
(let ([fib (U (lambda (f) (lambda (x) | |
(cond [(= x 0) 1] | |
[(= x 1) 1] | |
[else (+ ((f f) (- x 1)) ((f f) (- x 2)))]))))]) | |
(fib x))) | |
(define (length-using-letrec lst) | |
(letrec ([len (lambda (x) | |
(if (null? x) | |
0 | |
(add1 (len (rest x)))))]) | |
(len lst))) | |
(define (length-using-u lst) | |
(let ([len (U (lambda (f) | |
(lambda (x) | |
(if (null? x) | |
0 | |
(add1 ((f f) (rest x)))))))]) | |
(len lst))) | |
(define (fib-using-U-again x) | |
(let ([fib (U | |
(lambda (fib) | |
(lambda (x) | |
(cond [(= x 0) 1] | |
[(= x 1) 1] | |
[else (+ ((fib fib) (- x 1)) ((fib fib) (- x 2)))]))))]) | |
(fib x))) | |
'((lambda (f) (f (lambda (f) (lambda (x) (f (f (f (f (f x))))))))) | |
(Y-comb todo)) | |
'((lambda (f) (f (lambda (f) (lambda (x) (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x)))))))))))))))))))))))) (Y-comb todo)) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
I need help with this code. Please respond asap.