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))))