suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Changes example from arithmetic to pairs

Browse Source
This commit is contained in:
Casey Klein 2011-08-12 04:33:07 -05:00
parent 281e1003e3
commit cd1281fa65
1 changed files with 73 additions and 35 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

108
collects/redex/examples/define-judgment-form/multi-val.rkt
View File

@ -1,51 +1,89 @@
#lang racket #lang racket
(require redex) (require redex/reduction-semantics)
(define-language non-det-arith (define-language funny-pairs
(e (e e) (e (e e ...)
x x
v) v)
(v (λ (x) e) (v (λ (x ...) e)
integer (pair v v)
add1) pair
b
number)
(b fst
snd
one)
(E hole (E hole
(E e) (v ... E e ...))
(v E))
(x variable-not-otherwise-mentioned)) (x variable-not-otherwise-mentioned))
(define reduction (define reduction
(reduction-relation (reduction-relation
non-det-arith funny-pairs #:domain e
(--> (in-hole E ((λ (x) e) v)) (--> (in-hole E ((λ (x ..._1) e) v ..._1))
(in-hole E (subst e x v))) (in-hole E (subst e [x v] ...)))
(--> (in-hole E (add1 integer)) (--> (in-hole E (b v_1))
(in-hole E v) (in-hole E v_2)
(judgment-holds (δ add1 integer v))))) (judgment-holds (δ b v_1 v_2)))))
(define-judgment-form non-det-arith (define-judgment-form funny-pairs
#:mode (δ I I O) #:mode (δ I I O)
[(δ add1 integer 0)] [(δ fst (pair v_1 v_2) v_1)]
[(δ add1 integer v) [(δ snd (pair v_1 v_2) v_2)]
(where v (Σ 1 integer))]) [(δ one (pair v_1 v_2) v_1)]
[(δ one (pair v_1 v_2) v_2)])
(define-metafunction non-det-arith (define-metafunction funny-pairs
Σ : integer ... -> integer subst : e [x v] ... -> e
[(Σ integer ...) [(subst e) e]
,(apply + (term (integer ...)))]) [(subst e [x_1 v_1] [x_2 v_2] ...)
(subst (subst1 e x_1 v_1) [x_2 v_2] ...)])
(define-metafunction non-det-arith (define-metafunction funny-pairs
subst : e x v -> e subst1 : e x v -> e
[(subst (e_1 e_2) x v) [(subst1 (e ...) x v)
((subst e_1 x v) (subst e_2 x v))] ((subst1 e x v) ...)]
[(subst x x v) v] [(subst1 x x v) v]
[(subst x_1 x_2 v) x_1] [(subst1 x_1 x_2 v) x_1]
[(subst (λ (x) e) x v) [(subst1 (λ (x_1 ... x_i x_i+1 ...) e) x_i v)
(λ (x) e)] (λ (x_1 ... x_i x_i+1 ...) e)]
[(subst (λ (x_1) e) x_2 v) [(subst1 (λ (x_1 ...) e) x v)
; capture shmapture... ; capture shmapture...
(λ (x_1) (subst e x_2 v))] (λ (x_1 ...) (subst1 e x v))]
[(subst integer x v) integer] [(subst1 pair x v) pair]
[(subst add1 x v) add1]) [(subst1 b x v) b])
(traces reduction (term (((λ (x) (λ (x) (x (add1 7)))) (add1 0)) add1))) (test-->> reduction
(term (fst (pair 1 2)))
(term 1))
(test-->> reduction
(term (snd (pair 1 2)))
(term 2))
(test-->> reduction
(term (snd (λ (x) x)))
(term (snd (λ (x) x))))
(test-->> reduction
(term (one (pair 1 2)))
(term 1)
(term 2))
(test-->> reduction
(term ((one (pair fst snd))
((one (pair fst snd))
(pair (pair 1 2) (pair 3 4)))))
(term 1)
(term 2)
(term 3)
(term 4))
(test-->> reduction
(term ((λ (x) x) 1))
(term 1))
(test-->> reduction
(term ((λ (x y) y) 1 2))
(term 2))
(test-->> reduction
(term (((λ (x) (λ (x) x)) 1) 2))
(term 2))
(test-->> reduction
(term (((λ (x) (λ (y) (x y))) (λ (z) z)) 1))
(term 1))