tangledgroup Lambda Calculus and Lisp
Overview
This skill covers the practical and theoretical intersection of lambda calculus and Lisp. While lambda calculus is a minimal formal system with only variables, abstractions, and applications, Lisp was designed for list processing on the IBM 704 with hardware-specific operations like car and cdr. McCarthy borrowed LAMBDA notation from Church but did not intend Lisp as a direct implementation of lambda calculus — as he himself acknowledged, he "didn't understand the lambda calculus, really."
Despite this divergence, Lisp and lambda calculus share deep connections: lambda expressions bind variables and substitute arguments, eval provides self-interpretation (homoiconicity), and the Y combinator enables recursion in systems without named self-reference. This skill covers how to implement lambda calculus concepts in Scheme, encode data types as pure functions using Church encodings, and understand the historical relationship between these two foundational systems.
When to Use
- Implementing a lambda calculus interpreter or evaluator in Lisp/Scheme
- Understanding how recursion works without named functions (Y combinator, fixed-point combinators)
- Encoding data types (numbers, booleans, lists) as pure lambda terms in Scheme
- Studying McCarthy's original
evaland theLAMBDA/LABELmechanism - Building recursive functions in Emacs Lisp or Scheme with tail-call optimization
- Understanding why Lisp is not a direct realization of lambda calculus
Core Concepts
LAMBDA in Lisp vs Lambda Calculus
In McCarthy's 1958 Lisp, LAMBDA was borrowed from Church's lambda calculus as a notation for anonymous functions that bind variables:
(LAMBDA (x y z) (+ (* y x) (* z x)))
;; Applied to 5, 2, 3:
;; (+ (* 2 5) (* 3 5)) = 25
In pure lambda calculus, the equivalent is λx.λy.λz.body — functions take exactly one argument (curried). Lisp's LAMBDA accepts multiple parameters simultaneously, already a departure from pure lambda calculus.
EVAL: The Lisp Interpreter in Lisp
McCarthy's 1960 paper defined eval as a recursive function that interprets Lisp expressions. This is the foundation of homoiconicity — code as data:
(label eval
(lambda (e a)
(cond
((atom e) (assoc e a))
((atom (car e))
(cond
((eq (car e) 'quote) (cadr e))
((eq (car e) 'atom) (atom (eval (cadr e) a)))
((eq (car e) 'eq) (eq (eval (cadr e) a)
(eval (caddr e) a)))
((eq (car e) 'car) (car (eval (cadr e) a)))
((eq (car e) 'cdr) (cdr (eval (cadr e) a)))
((eq (car e) 'cons) (cons (eval (cadr e) a)
(eval (caddr e) a)))
((eq (car e) 'cond) (evcon (cdr e) a))
('t (eval (cons (assoc (car e) a)
(cdr e))
a))))
((eq (caar e) 'label) (eval (cons (caddar e) (cdr e))
(cons (list (cadar e) (car e)) a)))
((eq (caar e) 'lambda) (eval (caddar e)
(append (pair (cadar e)
(evlis (cdr e) a))
a))))))
This eval, combined with helper functions (evcon, evlis, assoc, pair), forms a complete Lisp interpreter. Steve Russell compiled this theoretical code into IBM 704 machine code, creating the first Lisp interpreter.
car/cdr: Hardware Origins, Not Pure Theory
car and cdr come from the IBM 704's memory architecture, not lambda calculus:
- CAR = Contents of the Address part of the Register
- CDR = Contents of the Decrement part of the Register
Lists are singly-linked structures where each node has a value field (car) and a next field (cdr). The list (a b c) is (cons a (cons b (cons c nil))). Pure lambda calculus has no car, cdr, cons, or eq — these must be encoded from the three basic constructs.
Recursion Without Names: The Y Combinator
Pure lambda calculus has no named functions, so a term cannot call itself by name. The Y combinator solves this by finding a fixed point of any function f:
Y f = f (Y f)
In Scheme (with beta-abstraction for strict evaluation):
(define Y
(lambda (f)
((lambda (x) (f (lambda (n) ((x x) n))))
(lambda (x) (f (lambda (n) ((x x) n)))))))
This enables recursion in systems without define or named self-reference.
Usage Examples
Church Numerals in Scheme
Encode natural numbers as function application counts:
(define lc-zero (lambda (f) (lambda (x) x)))
(define lc-succ (lambda (n) (lambda (f) (lambda (x) (f ((n f) x))))))
(define (church-to-int n)
((n (lambda (x) (+ x 1))) 0))
(define lc-one (lc-succ lc-zero))
(define lc-two (lc-succ lc-one))
(church-to-int lc-zero) ; 0
(church-to-int lc-two) ; 2
Factorial with the Y Combinator
Define factorial without naming the recursive function:
(define fact-generator
(lambda (self)
(lambda (n)
(if (= n 0)
1
(* n (self (- n 1)))))))
(define fact (Y fact-generator))
(fact 5) ; 120
Church Booleans and Conditionals
Encode logic as selection functions:
(define lc-true (lambda (x) (lambda (y) x)))
(define lc-false (lambda (x) (lambda (y) y)))
(define lc-if
(lambda (condition)
(lambda (then-val)
(lambda (else-val)
((condition then-val) else-val)))))
(((lc-if lc-true) "yes") "no") ; "yes"
Tail-Recursive Fibonacci in Emacs Lisp
Using cl-labels with accumulator for tail-call optimization:
(defun fib (n)
(cl-labels ((fib* (a b accum)
(let* ((accum (cons a accum))
(accum-lng (length accum)))
(if (< n accum-lng)
(nreverse accum)
(fib* b (+ b a) accum)))))
(fib* 0 1 nil)))
(fib 10) ; (0 1 1 2 3 5 8 13 21 34)
Advanced Topics
History and Origins: McCarthy's EVAL, the IBM 704 hardware origins of car/cdr, "Lisp ≠ Lambda Calculus" — why Lisp diverged from pure theory → History and Lisp Origins
Recursion in Lisp: Tail-call optimization, cl-labels, accumulator patterns, streams, and the excessive-lisp-nesting limits in Emacs Lisp → Recursion in Lisp
Y Combinator and Fixed-Points: Derivation of Y g = g(Y g), beta-abstraction for strict evaluation, Z combinator variant, complete factorial examples → Y Combinator and Fixed-Points
Church Encodings in Scheme: Booleans, numerals with arithmetic, pairs, lists with map/filter/fold, comparison operations, and recursion on Church terms → Church Encodings in Scheme