lc.scm

;;; Lambda calculus interpreter with precomputed free variables
(use-modules (srfi srfi-1)
             (srfi srfi-9)
             (ice-9 match))

;;; Set Type
(define set list)
(define member? member)
(define (union s1 s2)
  (lset-union eqv? s1 s2))
(define (difference s1 s2)
  (lset-difference eqv? s1 s2))
(define (intersection s1 s2)
  (lset-intersection eqv? s1 s2))

(define-record-type <lambda>
  (%make-lambda fv var body)
  lambda?
  (fv   lambda-free-vars)
  (var  lambda-var)
  (body lambda-body))

(define (make-lambda v b)
  (define fv
    (difference (free-vars b) (set v)))
  (%make-lambda fv v b))

(define-record-type <application>
  (%make-application fv f a)
  application?
  (fv application-free-vars)
  (f  application-function)
  (a  application-argument))

(define (make-application f a)
  (define fv
    (union (free-vars f) (free-vars a)))
  (%make-application fv f a))

(define-record-type <var>
  (make-var name)
  var?
  (name var-name))

(define (term? x)
  (or (lambda? x)
      (var? x)
      (application? x)))

(define (free-vars x)
  (cond ((lambda? x)
         (lambda-free-vars x))
        ((application? x)
         (application-free-vars x))
        ((var? x) (set x))))

(define (free? v exp)
  (member? v (free-vars exp)))

(define (subst var val body)
  (cond ((not (free? var body)) body)
        ((var? body)
         (if (equal? (var-name body) var)
             val
             body))
        ((application? body)
         (make-application
          (subst var val (application-function body))
          (subst var val (application-argument body))))
        ((lambda? body)
         (if (equal? (lambda-var body) var)
             body
             (make-lambda (lambda-var body)
                          (subst var val (lambda-body body)))))))

(define (evaluate term)
  (cond ((lambda? term) term)
        ((var? term) term)
        ((application? term)
         (let ((f (evaluate (application-function term)))
               (a (evaluate (application-argument term))))
           (if (lambda? f)
               (subst (lambda-var f) a (lambda-body f))
               (make-application f a))))))

(define (lc body)
  (match body
    (('lambda (var vars ...) body)
     (make-lambda var (fold-right make-lambda (lc body) vars)))
    ((? symbol? sym) (make-var sym))
    ((f a as ...)
     (fold make-application
           (make-application (lc f) (lc a))
           (map lc as)))))

(define test-term
  (lc '((lambda (f g x)
          (f (g x)))
        c)))

(define (gx-not-reduced?)
  (define (p x)
    (application-argument (lambda-body (lambda-body x))))
  (eqv? (p (lambda-body (application-function test-term)))
        (p (evaluate test-term))))

(gx-not-reduced?)