アルファ変換は lambda-calculus-subst そのまま、って理解で良いのかな。あと

((lambda (x) E1) E2)

は

(lambda-calculus-subst '((lambda (x) E1) E2) E2 x)

で良いのかどうか。なんか微妙な気もします。

最後のイータ変換ってのが微妙。だったのですが η-変換 にある以下の例で納得。

(lambda (x) (car x)) = car

でもこれ、lambda-calculus-subst で記述できるのかな。でもこの中で出てくる expression な lambda-exp は引数一つですね。直観的に書いてみると以下になるのかどうか。

(define eta-converts
  (lambda (exp)
    (cases expression exp
      (var-exp (id) ;; 略)
      (lambda-exp (id body)
        (cases expression body
          (app-exp (rator rand)
            (var-exp rator))
          ;; 略))
      ;; 略)))

えらくぐだぐだしてしまいまいたが、ようやく先に進めそうです。