(= caddr car:cddr)
(= cdddr cdr:cddr)

(= variable?
  [and _ (isa _ 'sym)])
(= application?
  [and (acons _) (acons:cdr _) (no:cddr _)])
(= abstraction?
  [and (acons _) (acons:cdr _) (acons:cddr _) (no:cdddr _)
       (is 'lambda (car _)) (variable? (cadr _))])

(= substitute
  (fn (x al)
    (if
      (variable? x) (aif (assoc x al) (cdr it) x)
      (application? x) (list (substitute (car x) al) (substitute (cadr x) al))
      (abstraction? x)
        ([_ (cdr x) (uniq)]
         (fn ((var expr) val)
           (list 'lambda val (substitute expr (cons (cons var val) al))))))))

(= beta? [and (application? _) (abstraction?:car _)])
(= beta
  (fn (x)
    (if
      (beta? x)
        (let ((lambd@ var expr) val) x
          (substitute expr (list (cons var val))))
      (variable? x)
        x
      (application? x)
        (let (proc arg) x
          (ccc
            (fn (return)
              ([if (~is _ proc) (return:list _ arg)] (beta proc))
              ([if (~is _ arg) (return:list proc _)] (beta arg))
              x)))
      (abstraction? x)
        (let (var expr) (cdr x)
          ([if (~is _ expr) (list 'lambda var _) x] (beta expr))))))
(= beta*
  [let x (beta _) (if (is _ x) x (do (write x) (prn) (beta* x)))])
(= testdata
  '((lambda x (x x))
    (((lambda s (lambda k (lambda x ((x s) k))))
      (lambda x (lambda y (lambda z ((x z) (y z))))))
     (lambda x (lambda y x)))))