#lang racket ; file contains Unicode characters - download rather than cut/paste from browser ;; proust-just-comp: substitution and computation for the lambda calculus ;; Prabhakar Ragde (September 2021) ;; Starting from a cut-back version of proust-pred-start.rkt, ;; we implement the rules for substitution and computation. ;; Grammar: ;; expr = (λ x => expr) ; lambda abstraction ;; | (expr expr) ; function application ;; | x ; variable / uninterpreted base type ;; Structures for Expr (abstract syntax tree representing terms). (struct Lam (var body) #:transparent) (struct App (rator rand) #:transparent) (struct Ann (expr type) #:transparent) ;; Parsing. ;; parse-expr : sexp -> Expr (define (parse-expr s) (match s [`(λ ,(? symbol? x) => ,e) (Lam x (parse-expr e))] [`(,e1 ,e2) (App (parse-expr e1) (parse-expr e2))] [`(,e1 ,e2 ,e3 ,r ...) (parse-expr `((,e1 ,e2) ,e3 ,@r))] [(? symbol? x) x] ; variable [else (error 'parse "bad syntax: ~a\n" s)])) ;; Unparsing, that is, pretty-printing. ;; pretty-print-expr : Expr -> String (define (pretty-print-expr e) (match e [(Lam x b) (format "(λ ~a => ~a)" x (pretty-print-expr b))] [(App e1 e2) (format "(~a ~a)" (pretty-print-expr e1) (pretty-print-expr e2))] [(? symbol? x) (symbol->string x)])) ;; substitution (define (subst oldx newx expr) (match expr [(? symbol? x) (if (equal? x oldx) newx x)] [(Lam x b) (cond [(equal? x oldx) expr] [(side-cond? x (list newx) false) (define repx (refresh x (list newx b))) (Lam repx (subst oldx newx (subst x repx b)))] [else (Lam x (subst oldx newx b))])] [(App f a) (App (subst oldx newx f) (subst oldx newx a))] [(Ann e t) (Ann (subst oldx newx e) (subst oldx newx t))])) (define (refresh x lst) (if (side-cond? x lst true) (refresh (freshen x) lst) x)) (define (freshen x) (string->symbol (string-append (symbol->string x) "_"))) (define (side-cond? x lst check-binders?) (ormap (lambda (expr) (sc-helper x expr check-binders?)) lst)) (define (sc-helper x expr check-binders?) (match expr [(? symbol? y) (equal? x y)] [(Lam y b) (cond [check-binders? (or (equal? x y) (sc-helper x b check-binders?))] [else (if (equal? x y) false (sc-helper x b check-binders?))])] [(App f a) (side-cond? x (list f a) check-binders?)] [(Ann e t) (side-cond? x (list e t) check-binders?)])) ;; reduction (define (reduce expr) (match expr [(? symbol? x) x] [(Lam x b) (Lam x (reduce b))] [(App f a) (define fr (reduce f)) (define fa (reduce a)) (match fr [(Lam x b) (reduce (subst x fa b))] [else (App fr fa)])])) ;; The usual very inadequate testing (easier to test with more features added) (require test-engine/racket-tests) (check-expect (reduce (parse-expr '(λ x => x))) (parse-expr '(λ x => x))) (check-expect (reduce (parse-expr '((λ x => x)(λ x => x)))) (parse-expr '(λ x => x))) (check-expect (reduce (parse-expr '(λ y => ((λ x => x)(λ x => x))))) (parse-expr '(λ y => (λ x => x)))) (test)