lambda_calc_thesis_1.rkt

#lang racket

(define const? number?)
(define var? symbol?)

(define (ev σ θ e)
  (match e
    [(? const? e) (cons σ e)]
    [(? var? e) (cons σ (hash-ref θ e))]
    ; Comma here matches any var
    [`(lambda (,varname) ,body)
     (cons σ (cons e θ))]
    [`(,e1 ,e2)
     (let* ([e1result (ev σ θ e1)]
            [σ1 (car e1result)]
            [fun (car (cdr e1result))]
            [θ1 (cdr (cdr e1result))]
            [e2result (ev σ1 θ e2)]
            [σ2 (car e2result)]
            [v1 (cdr e2result)])
       (match fun
         [`(lambda (,var) ,body)
          (ev
           σ2
           (hash-set θ1 var v1)
           body)]
         [_ (ev σ2 θ1 '())]
          ))]))

; Test S-CONST
;(ev (hash) (hash-set (hash) 'y 23) 3)

; Test S-VAR
;(ev (hash) (hash-set (hash) 'y 23) 'y)

; Test S-FUN
;(ev (hash) (hash-set (hash) 'y 23)
;    '(lambda (x) x))

; Test S-APP 1
;(ev (hash) (hash-set (hash) 'y 23)
;    '((lambda (x)
;        ((lambda (y) 23) x)) 1))

; Test S-APP 2
;(ev (hash) (hash-set (hash) 'y 23)
;    '((lambda (x) x) 1))

; Test S-APP-BOT
(ev (hash) (hash-set (hash) 'y 23)
    '((lambda (x) '()) 1))