Skip to content

Instantly share code, notes, and snippets.

@florence

florence/SKIdex

Created September 16, 2016 18:39
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save florence/a0bd28b1dea5cd82eee789053c3ae539 to your computer and use it in GitHub Desktop.
Save florence/a0bd28b1dea5cd82eee789053c3ae539 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
SKIdex
#lang racket
(require redex)
(define-language SKI
(e ::= S K I (e e) natural +))
(define R
(reduction-relation
SKI
(--> (((S e_1) e_2) e_3)
((e_1 e_3) (e_2 e_3)))
(--> ((K e_1) e_2) e_1)
(--> (I e_1) e_1)
(--> ((+ natural_1) natural_2)
,(+ (term natural_1) (term natural_2)))))
(define R* (compatible-closure R SKI e))
(define-term double ((S +) I))
(traces R* (term (double (double 5))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment