Untyped lambda calculus

lambda.el

;; Term = (Var index context-size)
;;      | (Abs term bound-var-name)
;;      | (App term term)
;; Context = [(name, _)]

(defun var-name (context-elm)
  "Get name of CONTEXT-ELM."
  (car context-elm))

(defun add-var (var context)
  "Add VAR (string) to CONTEXT"
  (cons (list var nil) context))

(defvar test nil)

;;; Print

(defun show (term &optional context raw)
  "Display TERM in CONTEXT."
  (pcase term
    ;; variable
    (`(Var ,index ,size)
     (if (eq (length context) size)
         (if raw (number-to-string index)
           (index2name context index))
       (error "Bad index: %s, term: %s context: %s" index term context)))
    ;; abstraction
    (`(Abs ,body ,x)
     (pcase-let ((`(,context1 ,x1) (unique-name context x)))
       (format "λ%s.%s" (if raw "" x1) (show body context1 raw))))
    ;; application
    (`(App ,t1 ,t2)
     (let ((t1t (show t1 context raw))
           (t2t (show t2 context raw)))
       ;; add parenthesis for abs and app, but not var
       (format "%s%s"
               (if (eq (car t1) 'Var) t1t (concat "(" t1t ")"))
               (if (eq (car t2) 'Var) t2t (concat "(" t2t ")")))))
    (_ (error "No matching pattern: %s" term))))

(when test
  (show '(Var 0 1) '(("x" nil)))
  (show '(App (Var 0 2) (Var 1 2)) '(("x" nil) ("y" nil)))
  (show '(Abs (Var 0 2) "x") '(("x" nil)))

  (show '(Abs (App (Var 0 3) (Var 1 3)) "x")
        '(("x" nil) ("y" nil)))

  (show '(Abs (App (Var 0 3) (Var 2 3)) "x")
        '(("x" nil) ("y" nil))))

(defun unique-name (context name)
  "Return a list (CONTEXT’ NAME’).
If NAME is in CONTEXT, generate a unique one (NAME’) and push to
CONTEXT (CONTEXT’), otherwise return (CONTEXT NAME)."
  (cl-labels ((f (context-elm) (equal (var-name context-elm) name))
              ;; f returns t if CONTEXT-ELM has the same name as NAME
              (or2 (a b) (or a b))) ; or is a special form
    (if (and context (cl-reduce #'or2 (mapcar #'f context)))
        ;; exists another NAME
        (unique-name context (concat name "'"))
      ;; NAME is unique, push to context
      (list (add-var name context) name))))

(when test
  (let ((cxt '(("a" nil) ("b" nil))))
    (unique-name cxt "a")))

(defun index2name (context index)
  "Translate INDEX to variable name in CONTEXT."
  (var-name (nth index context)))

;;; Parse

(defun parse (term &optional context)
  "Parse TERM into internal structure.
CONTEXT is current context."
  (pcase term
    (`(λ ,var . ,body)
     `(Abs ,(parse body (add-var (symbol-name var) context))
           ,(symbol-name var)))
    (`(,t1 ,t2) `(App ,(parse t1 context)
                      ,(parse t2 context)))
    (`(,symbol) (parse symbol context))
    ((pred symbolp)
     (cl-labels ((f (a b) (equal a (var-name b))))
       `(Var ,(or (cl-position (symbol-name term) context :test #'f)
                  (error "No previous declaration: %s" term))
             ,(length context))))
    (_ (error "No matching pattern: %s" term))))

(when test
  (parse '(λ x x))
  (parse '(λ x (λ y (x y))))
  (parse '(((λ x (λ y (x y))) (λ x x))))
  (show (parse '(λ x x)))
  (show (parse '(λ x (λ y (x y)))))
  (show (parse '(((λ x (λ y (x y))) (λ x x)))))
  (show (parse '(λ x (λ x (x x)))))
  (show (parse '(λ x ((λ x x) x)))))

;;; Shift

(defun shift (d term)
  (shift1 0 d term))

(defun shift1 (c d term)
  "Shift up D for indexes >= C in TERM."
  (pcase term
    ;; when we shift up, that always means we are put into another
    ;; layer of abstraction, so size + 1
    (`(Var ,idx ,size)
     (if (>= idx c) `(Var ,(+ idx d) ,(+ size d))
       `(Var ,idx ,(+ size d))))
    ;; go into one more layer of abstraction, c+1
    (`(Abs ,body ,var) `(Abs ,(shift1 (1+ c) d body) ,var))
    ;; simply recurs
    (`(App ,t1 ,t2) `(App ,(shift1 c d t1)
                          ,(shift1 c d t2)))
    (_ (error "No matching pattern: %s" term))))

;;; Substitution

(defun subst (j s term)
  "Substitute J with T in TERM.
Like “[j → s] t”."
  (pcase term
    (`(Var ,index ,size)
     (if (= index j) s term))
    (`(Abs ,body ,var)
     `(Abs ,(subst (1+ j) (shift 1 s) body) ,var))
    (`(App ,t1 ,t2)
     `(App ,(subst j s t1) ,(subst j s t2)))
    (_ (error "No matching pattern: %s" term))))

(defun beta (t1 v)
  "Perform β-reduction.
TM is body of function, V is argument."
  (pcase t1
    (`(Abs ,body ,_) (shift -1 (subst 0 (shift 1 v) body)))
    (_ (error "No matching pattern: %s" t1))))

;;; Evaluation

(defun valuep (term)
  (eq (car term) 'Abs))

(defun eval1 (term &optional step context)
  "Evaluate TERM in CONTEXT.
STEP, if non-nil, is the number of steps to evaluate."
  (let* ((step (or step 1.0e+INF)))
    ;; t := var | abs | app
    ;; v := abs
    (if (<= step 0)
        term
      (pcase term
        (`(Var . ,_) term)
        (`(Abs . ,_) term)
        ;; first reduce t1 to a value
        ((and `(App ,t1 ,t2) (guard (not (valuep t1))))
         (eval1 `(App ,(eval1 t1 step context) ,t2) (1- step) context))
        ;; then reduce t2 to a value
        ((and `(App ,t1 ,t2) (guard (not (valuep t2))))
         (eval1 `(App ,t1 ,(eval1 t2 step context)) (1- step) context))
        ;; finally apply
        ((and `(App ,t1 ,t2) (guard (valuep t1)) (guard (valuep t2)))
         (beta t1 t2))
        ;; no more to apply
        (_ term)))))

(when test
  (show (eval1 (parse '((λ x x) (λ y y)))))
  (show (eval1 (parse '((λ y (λ x x y)) (λ y y)))))
  (show (eval1 (parse '((λ y (λ x x y)) ((λ y y) (λ z z))))))
  (show (eval1 (parse '((λ x x) ((λ y y) (λ z z))))))
  (show (eval1 (parse '((λ x x) ((λ y y) (λ z z)))) 1))
  (show (parse '(((λ x x) (λ n (λ m m n))) ((λ y y) (λ z z)))))
  (show (eval1 (parse '(((λ x x) (λ n (λ m m n))) ((λ y y) (λ z z)))))))