### Lambda Calculus Interpreter.

 Later edit: there is newer, improved version of this interpreter, check this post and few posts before that.

; Lambda calculus implemented in Newlisp. It would be too ambitious
; to explain what is lambda calculus in this post, so I'll assume
; that reader familiarized himself with notion of lambda calculus
; somewhere else, and I'll provide only code for evaluation ("reduction")
; of lambda-expressions. Instead of lambda symbol, I'll use ^ -
; and it was original symbol used by Church.

; Only beta-reduction (but this is only important one) and normal
; order evaluation (better one, used for Haskell and fexprs) - from
; outside to inside implemented.

(set 'is-variable (lambda(x)(symbol? x)))

(set 'is-function (lambda(L)(and (list? L)
(= (first L) '^)
(= (nth 2 L) '.))))

(set 'function-variable (lambda(f)(nth 1 f)))
(set 'function-body (lambda(f)(last f)))

(set 'is-application (lambda(L)(and (list? L)
(= (length L) 2))))

(set 'substitute-free-occurences ; of variable V in E with F
(lambda(V E F)

(cond ((is-variable E) (if (= E V) F E))

((is-function E)

(if (= (function-variable E) V)

E ; V is bounded in E - no substitution

(list '^
(function-variable E)
'.
(substitute-free-occurences V
(function-body E)
F))))

((is-application E)
(list (substitute-free-occurences V (first E) F)
(substitute-free-occurences V (last E) F))))))

(set 'reduce-once
(lambda(E)
(cond ((is-variable E) E)
((is-function E) E)
((is-application E)
(let ((E1 (first E))
(E2 (last E)))

(if (is-function E1)

;E=((^V._) E2) ==> E10[V:=E2]

(substitute-free-occurences (function-variable E1)
(function-body E1)
E2)

;E=(E1 E2) ==>

(let ((new-E1 (reduce-once E1)))

(if (!= new-E1 E1)
(list new-E1 E2)
(list E1 (reduce-once E2))))))))))

(set 'reduce (lambda(new-expression)
(local(expression)
(println "\n--------------\n\n" (string new-expression))
(do-while (!= new-expression expression)
(setf expression new-expression)
(setf new-expression (reduce-once expression))
(if (!= new-expression expression)
(println " ==> " (string new-expression))
(println "\n     Further reductions are impossible."))
new-expression))))

; The list of reduced expressions

(dolist (i '( x
(^ x . x)
((^ x . x) y)
((^ x . a) ((^ y . y) z))
((^ y . (^ z . z)) ((^ x . (x x)) (^ v . (v v))))
((((^ v . (^ t . (^ f . ((v t) f)))) (^ x . (^ y . x))) a) b)
((((^ v . (^ t . (^ f . ((v t) f)))) (^ x . (^ y . y))) a) b)
; (^ f . ((^ x . (f (x x))) (^ x . (f (x x))))) Y-combinator - test it!
((^ x . (x x)) (^ x . (x x)))
;((^ x . (x (x x))) (^ x . (x (x x))))
))

;(println "\n\n=== " (+ \$idx 1) ": "  i "\n\n")

(reduce i))

(exit)

OUTPUT

--------------

x

Further reductions are impossible.

--------------

(^ x . x)

Further reductions are impossible.

--------------

((^ x . x) y)
==> y

Further reductions are impossible.

--------------

((^ x . a) ((^ y . y) z))
==> a

Further reductions are impossible.

--------------

((^ y . (^ z . z)) ((^ x . (x x)) (^ v . (v v))))
==> (^ z . z)

Further reductions are impossible.

--------------

((((^ v . (^ t . (^ f . ((v t) f)))) (^ x . (^ y . x))) a) b)
==> (((^ t . (^ f . (((^ x . (^ y . x)) t) f))) a) b)
==> ((^ f . (((^ x . (^ y . x)) a) f)) b)
==> (((^ x . (^ y . x)) a) b)
==> ((^ y . a) b)
==> a

Further reductions are impossible.

--------------

((((^ v . (^ t . (^ f . ((v t) f)))) (^ x . (^ y . y))) a) b)
==> (((^ t . (^ f . (((^ x . (^ y . y)) t) f))) a) b)
==> ((^ f . (((^ x . (^ y . y)) a) f)) b)
==> (((^ x . (^ y . y)) a) b)
==> ((^ y . y) b)
==> b

Further reductions are impossible.

--------------

((^ x . (x x)) (^ x . (x x)))

Further reductions are impossible.

--