Create a gist now

Instantly share code, notes, and snippets.

Small-step SOS with define-judgment-form
#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)))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment