Lambda Calculus Implementation in Scheme
Table of Contents
1. Introduction
This org-mode file contains a Lambda Calculus implementation in Scheme. Each section includes self-contained code blocks that can be run independently in a Scheme interpreter.
2. Lambda Expressions
; Step 1: Understand Lambda Expressions
(define identity (lambda (x) x))
(display (identity 5))
; Output: 5
3. Church Booleans
; Step 2: Implement Church Booleans
(define lc-true (lambda (x) (lambda (y) x)))
(define lc-false (lambda (x) (lambda (y) y)))
(define lc-if (lambda (condition) (lambda (then) (lambda (else) ((condition then) else)))))
(display (((lc-if lc-true) "yes") "no"))
(newline)
; Output: yes
4. Basic Combinators
; Step 3: Implement Basic Combinators
(define I (lambda (x) x))
(define K (lambda (x) (lambda (y) x)))
(define KI (lambda (x) (lambda (y) y)))
(display (I 5))
(newline)
(display ((K 3) 4))
(newline)
(display ((KI 3) 4))
(newline)
; Output:
; 5
; 3
; 4
5. Church Numerals
; Step 4: Create Church Numerals
(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))
(display (church-to-int lc-zero))
(newline)
(display (church-to-int lc-one))
(newline)
(display (church-to-int lc-two))
(newline)
; Output:
; 0
; 1
; 2
6. Basic Arithmetic
; Step 5: Implement Basic Arithmetic
(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-add (lambda (m) (lambda (n) (lambda (f) (lambda (x) ((m f) ((n f) x)))))))
(define lc-mult (lambda (m) (lambda (n) (lambda (f) (m (n f))))))
(define lc-one (lc-succ lc-zero))
(define lc-two (lc-succ lc-one))
(define lc-three (lc-succ lc-two))
(display (church-to-int ((lc-add lc-one) lc-two)))
(newline)
(display (church-to-int ((lc-mult lc-two) lc-three)))
(newline)
; Output:
; 3
; 6
7. Pairs
; Step 6: Implement Pairs
(define lc-pair (lambda (x) (lambda (y) (lambda (f) ((f x) y)))))
(define lc-first (lambda (p) (p (lambda (x) (lambda (y) x)))))
(define lc-second (lambda (p) (p (lambda (x) (lambda (y) y)))))
(define my-pair ((lc-pair 3) 4))
(display (lc-first my-pair))
(newline)
(display (lc-second my-pair))
(newline)
; Output:
; 3
; 4
8. Lists
; Step 7: Build Lists Using Pairs
(define lc-true (lambda (x) (lambda (y) x)))
(define lc-false (lambda (x) (lambda (y) y)))
(define lc-pair (lambda (x) (lambda (y) (lambda (f) ((f x) y)))))
(define lc-first (lambda (p) (p (lambda (x) (lambda (y) x)))))
(define lc-second (lambda (p) (p (lambda (x) (lambda (y) y)))))
(define lc-nil (lambda (x) lc-true))
(define lc-cons lc-pair)
(define lc-is-nil (lambda (l) (l (lambda (h) (lambda (t) lc-false)))))
(define lc-head lc-first)
(define lc-tail lc-second)
; Helper function to convert Scheme list to Church-encoded list
(define (list-to-church lst)
(if (null? lst)
lc-nil
((lc-cons (car lst)) (list-to-church (cdr lst)))))
; Helper function to convert Church-encoded list to Scheme list
(define (church-to-list l)
(if ((l (lambda (h) (lambda (t) lc-false))) #t #f)
'()
(cons (lc-head l) (church-to-list (lc-tail l)))))
(define my-list (list-to-church '(1 2 3)))
(display (church-to-list my-list))
(newline)
(display (lc-head my-list))
(newline)
(display (church-to-list (lc-tail my-list)))
(newline)
(display ((lc-is-nil my-list) #t #f))
(newline)
(display ((lc-is-nil lc-nil) #t #f))
(newline)
; Output:
; (1 2 3)
; 1
; (2 3)
; #f
; #t
9. Comparison Operations
; Step 8: Implement Comparison Operations
(define lc-zero (lambda (f) (lambda (x) x)))
(define lc-succ (lambda (n) (lambda (f) (lambda (x) (f ((n f) x))))))
(define lc-true (lambda (x) (lambda (y) x)))
(define lc-false (lambda (x) (lambda (y) y)))
(define lc-is-zero (lambda (n) ((n (lambda (x) lc-false)) lc-true)))
(define lc-leq (lambda (m) (lambda (n) (lc-is-zero ((lc-sub m) n)))))
(define lc-eq (lambda (m) (lambda (n) ((lc-and (lc-leq m n)) (lc-leq n m)))))
(define lc-and (lambda (x) (lambda (y) ((x y) lc-false))))
(define lc-sub
(lambda (m)
(lambda (n)
((n (lambda (n)
(lambda (f)
(lambda (x)
((n (lambda (g) (lambda (h) (h (g f)))))
(lambda (y) x)
(lambda (y) y))))))
m))))
(define lc-one (lc-succ lc-zero))
(define lc-two (lc-succ lc-one))
(display ((lc-is-zero lc-zero) #t #f))
(newline)
(display ((lc-is-zero lc-one) #t #f))
(newline)
(display (((lc-leq lc-one) lc-two) #t #f))
(newline)
(display (((lc-eq lc-one) lc-one) #t #f))
(newline)
(display (((lc-eq lc-one) lc-two) #t #f))
(newline)
; Output:
; #t
; #f
; #t
; #t
; #f
10. Higher-Order List Operations
; Step 9: Implement Higher-Order List Operations
(define lc-zero (lambda (f) (lambda (x) x)))
(define lc-succ (lambda (n) (lambda (f) (lambda (x) (f ((n f) x))))))
(define lc-true (lambda (x) (lambda (y) x)))
(define lc-false (lambda (x) (lambda (y) y)))
(define lc-pair (lambda (x) (lambda (y) (lambda (f) ((f x) y)))))
(define lc-first (lambda (p) (p (lambda (x) (lambda (y) x)))))
(define lc-second (lambda (p) (p (lambda (x) (lambda (y) y)))))
(define lc-nil (lambda (x) lc-true))
(define lc-cons lc-pair)
(define lc-is-nil (lambda (l) (l (lambda (h) (lambda (t) lc-false)))))
(define lc-head lc-first)
(define lc-tail lc-second)
(define lc-if (lambda (condition) (lambda (then) (lambda (else) ((condition then) else)))))
(define lc-map
(lambda (f)
(lambda (l)
(((lc-if (lc-is-nil l))
lc-nil)
(lambda () ((lc-cons (f (lc-head l))) ((lc-map f) (lc-tail l))))))))
(define lc-filter
(lambda (p)
(lambda (l)
(((lc-if (lc-is-nil l))
lc-nil)
(lambda ()
(((lc-if (p (lc-head l)))
(lambda () ((lc-cons (lc-head l)) ((lc-filter p) (lc-tail l)))))
(lambda () ((lc-filter p) (lc-tail l)))))))))
(define lc-fold
(lambda (f)
(lambda (acc)
(lambda (l)
(((lc-if (lc-is-nil l))
acc)
(lambda () (((lc-fold f) (f acc (lc-head l))) (lc-tail l))))))))
(define (list-to-church lst)
(if (null? lst)
lc-nil
((lc-cons (car lst)) (list-to-church (cdr lst)))))
(define (church-to-list l)
(if ((l (lambda (h) (lambda (t) lc-false))) #t #f)
'()
(cons (lc-head l) (church-to-list (lc-tail l)))))
(define my-list (list-to-church '(1 2 3)))
(define doubled-list ((lc-map (lambda (x) (* x 2))) my-list))
(display "Doubled list: ")
(display (church-to-list doubled-list))
(newline)
(define filtered-list ((lc-filter (lambda (x) (> x 1))) my-list))
(display "Filtered list: ")
(display (church-to-list filtered-list))
(newline)
(define sum-list (((lc-fold (lambda (x) (lambda (y) (+ x y)))) 0) my-list))
(display "Sum of list: ")
(display sum-list)
(newline)
; Output:
; Doubled list: (2 4 6)
; Filtered list: (2 3)
; Sum of list: 6
11. Recursion and Fixed-Point Combinators
; Step 10: Explore Recursion and Fixed-Point Combinators
(define lc-zero (lambda (f) (lambda (x) x)))
(define lc-succ (lambda (n) (lambda (f) (lambda (x) (f ((n f) x))))))
(define lc-true (lambda (x) (lambda (y) x)))
(define lc-false (lambda (x) (lambda (y) y)))
(define lc-if (lambda (condition) (lambda (then) (lambda (else) ((condition then) else)))))
(define lc-is-zero (lambda (n) ((n (lambda (x) lc-false)) lc-true)))
(define lc-sub
(lambda (m)
(lambda (n)
((n (lambda (n)
(lambda (f)
(lambda (x)
((n (lambda (g) (lambda (h) (h (g f)))))
(lambda (y) x)
(lambda (y) y))))))
m))))
(define lc-mult (lambda (m) (lambda (n) (lambda (f) (m (n f))))))
(define (church-to-int n)
((n (lambda (x) (+ x 1))) 0))
(define lc-one (lc-succ lc-zero))
(define Y
(lambda (f)
((lambda (x) (f (lambda (y) ((x x) y))))
(lambda (x) (f (lambda (y) ((x x) y)))))))
(define factorial
(Y (lambda (f)
(lambda (n)
(((lc-if (lc-is-zero n))
lc-one)
(lambda () ((lc-mult n) (f ((lc-sub n) lc-one)))))))))
(define lc-five (lc-succ (lc-succ (lc-succ (lc-succ lc-one)))))
(display "Factorial of 5: ")
(display (church-to-int (factorial lc-five)))
(newline)
; Output:
; Factorial of 5: 120
12. Conclusion
This org-mode file provides a comprehensive implementation of Lambda Calculus in Scheme, including Church encodings for booleans, numerals, and lists, as well as higher-order functions and recursion using the Y combinator. Each section can be run independently in a Scheme interpreter to explore different aspects of Lambda Calculus.