How can I programmatically expand the "let" family of functions?

Questions & Answers
3

Just as a quick example, let’s see how to do it in an object language with naturals numbers, the usual lambda-calculus constructs (variables, abstractions, and applications), and let forms:

#lang racket/base
(require redex/reduction-semantics)

(define-language Lambda-Let
  (e ::=
     natural                    ; natural numbers
     x                          ; variables
     (lambda (x ...) e)         ; abstractions
     (let ([x e] ...) e)        ; `let` forms
     (e e ...))                 ; applications
  (x ::= variable-not-otherwise-mentioned))

(define-metafunction Lambda-Let
  let->lambda : e -> e
  [(let->lambda (lambda (x ...) e_body))
   (lambda (x ...) (let->lambda e_body))]
  [(let->lambda (let ([x e] ...) e_body))
   (let->lambda ((lambda (x ...) e_body) e ...))]
  [(let->lambda (e ...))
   ((let->lambda e) ...)]
  [(let->lambda e)
   e])

(term (let->lambda (let ([x 1]
                         [y 2])
                     (+ x y))))

The metafunction (i.e., function on terms) is automagically defined according to the object language, which is why Redex is so useful.

Edit: Make it recursive.