public
Created

A non-deterministic semantics with define-judgment-form

  • Download Gist
not-det-delta.rkt
Racket
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51
#lang racket
 
(require redex)
 
(define-language STLC
(e (e e)
x
v)
(v (λ (x) e)
integer
add1)
(E hole
(E e)
(v E))
(x variable-not-otherwise-mentioned))
 
(define reduction
(reduction-relation
STLC
(--> (in-hole E ((λ (x) e) v))
(in-hole E (subst e x v)))
(--> (in-hole E (add1 integer))
(in-hole E v)
(judgment-holds (δ add1 integer v)))))
 
(define-judgment-form STLC
mode : I I O
[(δ add1 integer 0)]
[(δ add1 integer v)
(where v (Σ 1 integer))])
 
(define-metafunction STLC
Σ : integer ... -> integer
[(Σ integer ...)
,(apply + (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])
 
(traces reduction (term (((λ (x) (λ (x) (x (add1 7)))) (add1 0)) add1)))

Please sign in to comment on this gist.

Something went wrong with that request. Please try again.