Small-step SOS with define-judgment-form

small-sos.rkt

#lang racket

(require redex)


;                                                                        
;                                                                        
;                                                                        
;   ;;;;             ;;    ;             ;             ;                 
;   ;   ;           ;      ;             ;     ;       ;                 
;   ;   ;           ;                          ;                         
;   ;   ;   ;;;    ;;;     ;    ;;;;     ;    ;;;      ;     ;;;   ;;;;  
;   ;   ;  ;   ;    ;      ;    ;   ;    ;     ;       ;    ;   ;  ;   ; 
;   ;   ;  ;;;;;    ;      ;    ;   ;    ;     ;       ;    ;   ;  ;   ; 
;   ;   ;  ;        ;      ;    ;   ;    ;     ;       ;    ;   ;  ;   ; 
;   ;   ;  ;   ;    ;      ;    ;   ;    ;     ;       ;    ;   ;  ;   ; 
;   ;;;;    ;;;     ;      ;    ;   ;    ;      ;;     ;     ;;;   ;   ; 
;                                                                        
;                                                                        
;                                                                        


(define-language STLC
  (e (e e)
     x
     v)
  (v (λ (x) e)
     integer
     add1)
  (x variable-not-otherwise-mentioned))

(define-judgment-form STLC
  mode : I O
  small-step ⊆ e × e
  [(small-step ((λ (x) e) v) (subst e x v))]
  [(small-step (add1 integer) (δ add1 integer))]
  [(small-step (e_1 e_2) (e_1′ e_2))
   (small-step e_1 e_1′)]
  [(small-step (v e_2) (v e_2′))
   (small-step e_2 e_2′)])

(define-judgment-form STLC
  mode : I O
  small-step* ⊆ e × e
  [(small-step* e e)]
  [(small-step* e_1 e_3)
   (small-step e_1 e_2)
   (small-step* e_2 e_3)])

(define-judgment-form STLC
  mode : I O
  eval ⊆ e × e
  [(eval e v)
   (small-step* e v)])

(define-metafunction STLC
  [(δ add1 integer) ,(add1 (term integer))])

(define-metafunction STLC
  subst : e x v -> e
  [(subst (e_1 e_2) x v)
   ((subst e_1 x v) (subst e_2 x v))]
  [(subst x x v) v]
  [(subst x_1 x_2 v) x_1]
  [(subst (λ (x) e) x v)
   (λ (x) e)]
  [(subst (λ (x_1) e) x_2 v)
   ; capture shmapture...
   (λ (x_1) (subst e x_2 v))]
  [(subst integer x v) integer]
  [(subst add1 x v) add1])

(test-equal (judgment-holds (eval (add1 (add1 (add1 0))) v) v) 
            (list (term 3)))
(test-equal (judgment-holds 
             (eval (((λ (x) (λ (x) (x (add1 7)))) 0) add1)
                   v)
             v)
            (list (term 9)))


;                                                                               
;                                                                               
;                                                                               
;   ;;;;;                                                     ;                 
;     ;                                        ;      ;       ;                 
;     ;                                        ;      ;                         
;     ;    ;   ;  ;;;;    ;;;    ;;;    ;;;   ;;;    ;;;      ;    ;;;;    ;;;; 
;     ;    ;   ;  ;   ;  ;   ;  ;   ;  ;   ;   ;      ;       ;    ;   ;  ;   ; 
;     ;    ;   ;  ;   ;  ;;;;;   ;;;   ;;;;;   ;      ;       ;    ;   ;  ;   ; 
;     ;    ;   ;  ;   ;  ;          ;  ;       ;      ;       ;    ;   ;  ;   ; 
;     ;    ;   ;  ;   ;  ;   ;  ;   ;  ;   ;   ;      ;       ;    ;   ;  ;   ; 
;     ;     ;;;;  ;;;;    ;;;    ;;;    ;;;     ;;     ;;     ;    ;   ;   ;;;; 
;              ;  ;                                                           ; 
;          ;   ;  ;                                                       ;   ; 
;           ;;;                                                            ;;;  


(define (rewrite-subst lws)
  (list "" (list-ref lws 2) "{" (list-ref lws 3) ":=" (list-ref lws 4) "}"))
(define (rewrite-small-step lws)
  (list "" (list-ref lws 2) " → " (list-ref lws 3)))

(with-compound-rewriter
 'small-step rewrite-small-step
 (with-compound-rewriter
  'subst rewrite-subst
  (with-atomic-rewriter
   'integer "Z"
   (render-judgment-form small-step))))


;                                                   
;                                                   
;                                                   
;   ;;;;;                         ;                 
;     ;                           ;                 
;     ;                                             
;     ;    ; ;;    ;;;;   ;;;     ;    ;;;;    ;;;; 
;     ;    ;;  ;  ;   ;  ;   ;    ;    ;   ;  ;   ; 
;     ;    ;   ;  ;   ;  ;        ;    ;   ;  ;   ; 
;     ;    ;      ;   ;  ;        ;    ;   ;  ;   ; 
;     ;    ;      ;  ;;  ;   ;    ;    ;   ;  ;   ; 
;     ;    ;       ;; ;   ;;;     ;    ;   ;   ;;;; 
;                                                 ; 
;                                             ;   ; 
;                                              ;;;  


(define small-step-rr
  (reduction-relation
   STLC
   (--> e_1 e_2
        (judgment-holds (small-step e_1 e_2)))))

(traces small-step-rr (term ((λ (x) (add1 x)) 0)))