Skip to content

Instantly share code, notes, and snippets.

@kayceesrk
Created January 19, 2016 13:01
Show Gist options
  • Save kayceesrk/b585566a3c6ddd02b2b3 to your computer and use it in GitHub Desktop.
Save kayceesrk/b585566a3c6ddd02b2b3 to your computer and use it in GitHub Desktop.
Redex amb
#lang racket
(require redex)
(define-language L
(e (e e)
(λ (x t) e)
x
(amb e ...)
number
(+ e ...)
(if0 e e e)
(fix e))
(t (→ t t) num)
(x variable-not-otherwise-mentioned))
(define-extended-language L+Γ L
[Γ · (x : t Γ)])
(define-judgment-form
L+Γ
#:mode (types I I O)
#:contract (types Γ e t)
[(types Γ e_1 (→ t_2 t_3))
(types Γ e_2 t_2)
-------------------------
(types Γ (e_1 e_2) t_3)]
[(types (x : t_1 Γ) e t_2)
-----------------------------------
(types Γ (λ (x t_1) e) (→ t_1 t_2))]
[(types Γ e (→ (→ t_1 t_2) (→ t_1 t_2)))
---------------------------------------
(types Γ (fix e) (→ t_1 t_2))]
[---------------------
(types (x : t Γ) x t)]
[(types Γ x_1 t_1)
(side-condition (different x_1 x_2))
------------------------------------
(types (x_2 : t_2 Γ) x_1 t_1)]
[(types Γ e num) ...
-----------------------
(types Γ (+ e ...) num)]
[--------------------
(types Γ number num)]
[(types Γ e_1 num)
(types Γ e_2 t)
(types Γ e_3 t)
-----------------------------
(types Γ (if0 e_1 e_2 e_3) t)]
[(types Γ e num) ...
--------------------------
(types Γ (amb e ...) num)])
(define-extended-language Ev L+Γ
(p (e ...))
(P (e ... E e ...))
(E (v E)
(E e)
(+ v ... E e ...)
(if0 E e e)
(fix E)
hole)
(v (λ (x t) e)
(fix v)
number))
(define-metafunction Ev
Σ : number ... -> number
[(Σ number ...)
,(apply + (term (number ...)))])
(require redex/tut-subst)
(define-metafunction Ev
subst : x v e -> e
[(subst x v e)
,(subst/proc x? (list (term x)) (list (term v)) (term e))])
(define x? (redex-match Ev x))
(define red
(reduction-relation
Ev
#:domain p
(--> (in-hole P (if0 0 e_1 e_2))
(in-hole P e_1)
"if0t")
(--> (in-hole P (if0 v e_1 e_2))
(in-hole P e_2)
(side-condition (not (equal? 0 (term v))))
"if0f")
(--> (in-hole P ((fix (λ (x t) e)) v))
(in-hole P (((λ (x t) e) (fix (λ (x t) e))) v))
"fix")
(--> (in-hole P ((λ (x t) e) v))
(in-hole P (subst x v e))
"βv")
(--> (in-hole P (+ number ...))
(in-hole P (Σ number ...))
"+")
(--> (e_1 ... (in-hole E (amb e_2 ...)) e_3 ...)
(e_1 ... (in-hole E e_2) ... e_3 ...)
"amb")))
(define expr (term (
((λ (x num) (+ x 1)) 10)
)))
(apply-reduction-relation* red expr)
(define expr2 (term (
((fix (λ (sum (→ num num)) (λ (n num) (if0 n 0 (+ n (sum (+ n -1))))))) 3)
)))
(apply-reduction-relation* red expr2)
(define expr3 (term (
((fix (λ (rand (→ num num)) (λ (n num) (if0 n 0 (amb n (rand (+ n -1))))))) 10)
)))
(apply-reduction-relation* red expr3)
(traces red expr3)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment