untyped lambda calculus

gistfile1.rkt

#lang racket

(require redex)
(require redex/tut-subst)

(define-language L
  (e (e e)
     x
     v)
  (v (lambda (x) e))
  (c (v c)
     (c e)
     hole)
  (x variable-not-otherwise-mentioned))

(define red
  (reduction-relation
   L
   #:domain e
   (--> (in-hole c ((lambda (x) e) v))
        (in-hole c (subst x v e))
        "beta")))

;; subst : [Listof LTerm] [Listof LTerm] LTerm -> LTerm
(define-metafunction L
  subst : x v e -> e
  [(subst x v e)
   ,(subst/proc x? (list (term x)) (list (term v)) (term e))])
;; x? : LTerm -> Boolean
(define x? (redex-match L x))

(traces red (term ((lambda (x) x) (lambda (y) y))))
(traces red (term ((lambda (x) (lambda (y) (y (x x)))) (lambda (z) z))))