#lang racket (require redex) ;; language of arith (define-language arith ;; number values (I integer) ;; boolean values (B true false) ;; values ((U V W) I B) ;; arithemtic operators (Op1 BoolOp1) (Op2 BoolOp2 NumOp2 CmpOp2) (BoolOp1 ¬) (BoolOp2 ∧ ∨) (NumOp2 + - * /) (CmpOp2 < >) ;; types (t Int Bool) ;; expressions ((E F G) V (Op1 E) (E Op2 F) (if E then F else G) ) ;; evaluation context ((C) hole (C Op2 E) (V Op2 C) (OP1 C) (if C then F else G) ) ) ;; test sntax ;(redex-match arith E (term (1 + 2))) ;;(redex-match arith E (term (1 ∧ 2))) ; not valid, but correct syntax ;(redex-match arith E (term (1 < 2))) ;(redex-match arith E (term (true ∧ false))) ;(redex-match arith E (term (¬ true))) ;(redex-match arith E (term ((1 + (1 + 2)) * (2 + 2)))) ;(redex-match arith E (term (if (1 < 2) then (1 + 2) else (1 * 2)))) ;(redex-match arith (in-hole C (4 * E)) (term (4 * (2 + 2)))) ;(redex-match arith (in-hole C (1 + E)) (term ((1 + 2) < (4 * (2 + 2))))) ;(redex-match arith (in-hole C E) (term (if (1 < 2) then (1 + 2) else (1 * 2)))) ;; contract transformations (define-metafunction arith [(δ (I_1 + I_2)) ,(+ (term I_1) (term I_2))] [(δ (I_1 - I_2)) ,(- (term I_1) (term I_2))] [(δ (I_1 * I_2)) ,(* (term I_1) (term I_2))] [(δ (I_1 / I_2)) ,(/ (term I_1) (term I_2))] [(δ (I_1 < I_2)) ,(if (< (term I_1) (term I_2)) (term true) (term false))] [(δ (I_1 > I_2)) ,(if (> (term I_1) (term I_2)) (term true) (term false))] [(δ (B_1 ∧ B_2)) ,(if (eq? (term B_1) (term true)) (term B_2) (term false))] [(δ (B_1 ∨ B_2)) ,(if (eq? (term B_1) (term true)) (term true) (term B_2))] [(δ (¬ B_1)) ,(if (eq? (term B_1) (term true)) (term false) (term true))] ) (define arith-reduction (reduction-relation arith (--> (in-hole C (OP1 V)) (in-hole C (δ (OP1 V))) δ1 ) (--> (in-hole C (V OP2 W)) (in-hole C (δ (V OP2 W))) δ2 ) (--> (in-hole C (if true then F else G)) (in-hole C F) If-true ) (--> (in-hole C (if false then F else G)) (in-hole C G) If-false ) )) ;(traces arith-reduction (term (2 + 2))); ;(traces arith-reduction (term (true ∨ true))) ;;(traces arith-reduction (term (1 ∨ 2))) ; valid syntax, but cannot be reduced ;(traces arith-reduction (term ((4 * 2) + 2))) ;(traces arith-reduction (term (4 < (2 + 2)))) ;(traces arith-reduction (term (true ∨ (4 < (2 + 2))))) ;(traces arith-reduction (term ((1 + (1 + 2)) * (2 + 2)))) ;(traces arith-reduction (term ((1 + 2) < (4 * (2 + 2))))) ;(traces arith-reduction (term (if (1 < 2) then (1 + 2) else (1 * 2)))) ;(define-extended-language typed-arith arith ; [Γ · (x : t Γ)]) (define-judgment-form arith #:mode (types I O) #:contract (types E t) [-------------------- (types I Int)] [-------------------- (types B Bool)] [(types E Bool) ----------------------- (types (BoolOp1 E) Bool)] [(types E Bool) (types F Bool) ----------------------- (types (E BoolOp2 F) Bool)] [(types E Int) (types F Int) ----------------------- (types (E CmpOp2 F) Bool)] [(types E Int) (types F Int) ----------------------- (types (E NumOp2 F) Int)] [(types E Bool) (types F t) (types G t) ----------------------------- (types (if E then F else G) t)] ) (judgment-holds (types (1 + 1) Int)) ;(judgment-holds (types (true + 1) Int)) (judgment-holds (types (if (1 < 2) then (1 + 2) else (2 + 1)) Int)) (judgment-holds (types (if (1 < 2) then (1 + 2) else (true + 1)) Int))