diff options
Diffstat (limited to 'lc.rkt')
| -rw-r--r-- | lc.rkt | 97 |
1 files changed, 0 insertions, 97 deletions
@@ -1,97 +0,0 @@ -#lang racket ; note: do NOT use racket/base -(require "lib.rkt") - -;; The Untyped Lambda Calculus - -; note: default arguments MUST all be at the end -(define (interpret expr [ctx '()]) - (match expr - [`(λ ,id ,body) - `(λ ,id ,(interpret body ctx))] - [`((λ ,id ,body) ,arg) - (interpret body (dict-set ctx id arg))] - [`(,id ,arg) #:when (dict-has-key? ctx id) - (interpret `(,(interpret (dict-ref ctx id) ctx) ,arg))] - [`(,body ,arg) - (let ([reduced (interpret body ctx)]) - (if (equal? body reduced) - `(,reduced ,(interpret arg ctx)) - (interpret `(,reduced ,arg) ctx)))] - [id #:when (dict-has-key? ctx id) - (interpret (dict-ref ctx id) ctx)] - [val #:when (symbol? val) val] - [_ (err (format "unknown expression ~a" expr))])) - -(require rackunit) -(check-equal? (interpret '(λ x x)) '(λ x x)) -(check-equal? (interpret '((λ a a) (x y))) '(x y)) -(check-equal? (interpret '((λ a (x y)) (λ z z))) '(x y)) -(check-equal? (interpret '((λ a (a y)) x)) '(x y)) - -;; normalizes an expression into binding variables descending -;; (α-convert Expr Table[Old New] Set[New]) -(define (α-convert expr [ctx '()] [used '()]) - (match expr - [`(λ ,id ,body) - (let ([new (fresh used)]) - `(λ ,new ,(α-convert body (dict-set ctx id new) (set-add used new))))] - [`(,body ,arg) - `(,(α-convert body ctx used) ,(α-convert arg ctx used))] - [id #:when (dict-has-key? ctx id) - (dict-ref ctx id)] - [val #:when (symbol? val) val] - [_ (err (format "α-converting unknown expression ~a" expr))])) - -;; FIXME lmfao -(define (fresh used) - (cond - [(set-member? used 'i) 'j] - [(set-member? used 'h) 'i] - [(set-member? used 'g) 'h] - [(set-member? used 'f) 'g] - [(set-member? used 'e) 'f] - [(set-member? used 'd) 'e] - [(set-member? used 'c) 'd] - [(set-member? used 'b) 'c] - [(set-member? used 'a) 'b] - [else 'a])) - -(check-equal? - (α-convert '(λ a (λ b (λ c (a (b c)))))) - (α-convert '(λ c (λ a (λ b (c (a b))))))) - -; fixme: at least two issues: -; β-reduction is not normally strongly normalizing! -; we want to find a tradeoff in presentation to get termination here -; the β-reduction step, i'm pretty sure, needs to α-convert some stuff... -; b/c we're getting weird failures in the very last terms -; i.e. '(λ a (λ b ((a b) a))) vs '(λ a (λ b (a a))) - -;; (β-reduce Expr Table[]) -(define (β-reduce expr [ctx '()]) - (match expr - [`(λ ,id ,body) - `(λ ,id ,(β-reduce body ctx))] - [`((λ ,id ,body) ,arg) - (β-reduce body (dict-set ctx id arg))] - [`(,id ,arg) #:when (dict-has-key? ctx id) - (β-reduce `(,(β-reduce (dict-ref ctx id) ctx) ,arg))] - [`(,body ,arg) `(,body ,(β-reduce arg ctx))] - [`(,body ,arg) - (let ([reduced (β-reduce body ctx)]) - (if (equal? body reduced) - `(,reduced ,(β-reduce arg ctx)) - (β-reduce `(,reduced ,arg) ctx)))] - [id #:when (dict-has-key? ctx id) - (β-reduce (dict-ref ctx id) ctx)] - [val #:when (symbol? val) val] - [_ (err (format "β-reducing unknown expression ~a" expr))])) - -(define (normalize expr) - (α-convert (β-reduce expr))) - -(check-equal? - (normalize '(λ a (λ b (λ c (a (b c)))))) - (normalize '(λ c (λ a (λ b (c (a b))))))) - -(provide interpret normalize α-convert β-reduce) |