renames.lisp

;;;;renames.lisp

(in-package :lambda.renames)

;;; Renaming λ terms: α conversion
;;
;; This is something about which I read "You don't understand renaming until
;; you've implemented it", and I didn't quite believe it. Now I do. I have
;; thoroughly tested the functions in this file (see test/renames.lisp and
;; test/quickcheck/renames-equality.lisp).
;;
;; Notation: I use gensym-var as an argument to a function, when that
;; function should receive a gensym generated symbol, for it to hope to be
;; part of a safe rename.

(defun rename-error () ; => string
  "~%Symbol conflict while renaming a λ term. You probably didn't use a
new variable generated by (gensym).~%")

(defun rename-variable (term var gensym-var) ; => ^term
  (cond ((eq term var)
	 gensym-var)
	((eq term gensym-var)
	 (error (rename-error)))
	(T
	 term)))	   

(defun α-convert (var body) ; => ^abstraction
  "α conversion: renames the VAR of the abstraction (λ VAR BODY) with a 
GENSYM-generated variable."
  (let ((gensym-var (gensym)))
    (list 'λ gensym-var (rename body var gensym-var))))

(defun rename-in-abstraction (old-var var body gensym-var ; => ^abstraction
			      &aux (var% var) (body% body))
  "Renames OLD-VAR to GENSYM-VAR in the abstraction (λ VAR BODY)."
  (when (or (eq var old-var)
	    (eq var gensym-var))
    ;; in this case α convert and then apply rename-in-abstraction
    (destructuring-bind (λ% var%% body%%) 
	(α-convert var body)
      (setf var% var%%
	    body% body%%)))
  (list 'λ var% (rename body% old-var gensym-var)))

(defun rename (term var gensym-var) ; => λ-term
  "Replaces VAR with GENSYM-VAR, erroring if it finds GENSYM-VAR, at any place
in a possibly nested list of symbols. GENSYM-VAR must be a previously 
GENSYM-generated variable, for this to work correctly on λ terms."
  (^ecase term
         ((:variable
           (rename-variable term var gensym-var))
          ((operation operand) :application
           (list (rename operation var gensym-var)
                 (rename operand   var gensym-var)))
	  ((var% body) :abstraction
           (rename-in-abstraction var var% body gensym-var)))))