#lang racket
(require redex)

(define-language λ-calc
  ((M N) (λ X M)
         X
         (M M))
  (X variable-not-otherwise-mentioned))

(define-metafunction λ-calc
  [(FV X) ,(set (term X))]
  [(FV (λ X M)) ,(set-subtract (term (FV M)) (set (term X)))]
  [(FV (M_1 M_2)) ,(set-union (term (FV M_1))
                              (term (FV M_2)))])

(define-metafunction λ-calc
  [(subst X_1 M X_1) M]
  [(subst X_1 M X_2) X_2]
  [(subst X_1 M_2 (λ X_1 M_1)) (λ X_1 M_1)]
  [(subst X_2 M_2 (λ X_1 M_1))
   (λ X_3 (subst X_2 M_2 (subst X_1 X_3 M_1)))
   (where X_3 ,(variable-not-in 
                (set->list (set-union 
                            (term (FV X_1))
                            (term (FV X_2))
                            (term (FV M_2))
                            (term (FV (λ X_1 M_1)))))
                (term X_1)))]
  [(subst X M_3 (M_1 M_2)) ((subst X M_3 M_1)
                            (subst X M_3 M_2))])

(define general-red
  (reduction-relation
   λ-calc
   (--> (λ X_1 M)
        (λ X_2 (subst X_1 X_2 M))
        (where X_2 ,(variable-not-in (set->list (term (FV M)))
                                     (term X_1)))
        α)
   (--> ((λ X M_1) M_2)
        (subst X M_2 M_1)
        β)
   (--> (λ X (M X))
        M
        (side-condition
         (not (set-member? (term (FV M)) (term X))))
        η)))

(traces general-red
        (term (λ x y)))

(traces general-red
        (term (λ x (z x))))

(traces general-red
        (term ((λ x (x x)) (λ y (y y)))))