;;; church.scm
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Composition helper functions
;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define compose
(lambda (f g)
(lambda (x)
(f (g x)))))
(define compose-n
(lambda (f n)
(if (= n 1)
f
(compose f (compose-n f (- n 1))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Helper functions for lambda calculus.
;;
;; For our purposes here, the lambda calculus is a subset
;; of Scheme that has only symbols, lambda abstractions with
;; exactly one variable, and function applications.
;;
;; We will use Scheme's default evaluation strategy.
;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (listn? n lst)
(and (list? lst)
(= n (length lst))))
;; helper function: tests if e is a list with exactly one element
(define (singleton? e)
(listn? 1 e))
;; test for function application: (e1 e2)
(define (application? e)
(listn? 2 e))
;; test for lambda term: (lambda (x) a)
(define (abstraction? e)
(and (listn? 3 e)
(eq? 'lambda (first e))
(singleton? (second e))
(symbol? (first (second e)))))
;; returns true if e is a lambda term, and false otherwise
(define (term? e)
(cond
((symbol? e)
#t)
((application? e) ;; (e1 e2)
(and (term? (first e))
(term? (second e))))
((abstraction? e) ;; (lambda (x) a)
(term? (third e)))
(else
#f)
)
)
;; helper function: removes all top-level occurrences of x from lst
(define (remove-all x lst)
(cond
((null? lst)
'())
((equal? x (car lst))
(remove-all x (cdr lst)))
(else
(cons (car lst) (remove-all x (cdr lst)))
)
)
)
;; returns a list of all the free variables in lambda term e
(define (freevars e)
(cond
((symbol? e)
(list e))
((application? e) ;; (e1 e2)
(append (freevars (car e))
(freevars (second e))))
((abstraction? e) ;; (lambda (x) a)
(remove-all (car (second e)) (freevars (third e))))
(else
(error "freevars: not a lambda term" e))
)
)
;; returns true if x is free in term e
(define (free-in x e)
(if (symbol? e)
(eq? x e)
(member x (freevars e))
)
)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Natural numbers
;;
;; This the Church encoding of natural numbers, where each n
;; is defined to be a function that applies a given function f
;; n times to some input x.
;;
;; e.g. ((three 1+) 5) --> 8
;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define zero
(lambda (f)
(lambda (x)
x)))
(define one
(lambda (f)
(lambda (x)
(f x))))
(define two
(lambda (f)
(lambda (x)
(f (f x)))))
(define three
(lambda (f)
(lambda (x)
(f (f (f x))))))
;; ... etc ...
;; convert a Church numeral to its equivalent int
(define to-int
(lambda (c)
((c 1+) 0)))
;; returns the successor of the Church numeral n
(define succ
(lambda (n)
(lambda (f)
(lambda (x)
(f ((n f) x))))))
(define four (succ three))
(define five (succ four))
;; return m + n, the sum of two Church numerals
(define plus
(lambda (m)
(lambda (n)
(lambda (f)
(lambda (x)
((m f) ((n f) x)))))))
(define six ((plus one) five))
(define seven ((plus three) four))
;; returns m * n, the product of two Church numerals
(define mult
(lambda (m)
(lambda (n)
((m (plus n)) zero))))
(define eight ((mult two) four))
(define nine ((mult three) three))
;; returns a^b, i.e. a to the power of b
(define pow
(lambda (a)
(lambda (b)
(b a)
)
)
)
(define sixteen ((pow two) four))
;; Subtraction can also be defined using a PRED predecessor function,
;; but this turns out to be much trickier than SUCC and addition.
;PRED := λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)
;; returns n-1, where n is a Church numeral
(define pred
(lambda (n)
(lambda (f)
(lambda (x)
(((n (lambda (g) (lambda (h) (h (g f)))))
(lambda (u) x))
(lambda (u) u)
)))))
; SUB := λm.λn.n PRED m
;; returns m - n when m > n, otherwise 0
(define sub
(lambda (m)
(lambda (n)
((n pred) m)
)
)
)
;;
;; Basic Logic
;;
;TRUE := λx.λy.x
(define true
(lambda (x)
(lambda (y)
x)))
;FALSE := λx.λy.y
(define false
(lambda (x)
(lambda (y)
y)))
(define (to-bool b)
((b 'true) 'false))
;AND := λp.λq.p q p
(define cand
(lambda (p)
(lambda (q)
((p q) p))))
;OR := λp.λq.p p q
(define cor
(lambda (p)
(lambda (q)
((p p) q))))
;NOT := λp.p FALSE TRUE
(define cnot
(lambda (p)
((p false) true)))
;IFTHENELSE := λp.λa.λb.p a b
(define ifthenelse
(lambda (p)
(lambda (a)
(lambda (b)
((p a) b)))))
;ISZERO := λn.n (λx.FALSE) TRUE
;; returns true if n is zero, false otherwise
(define iszero
(lambda (n)
((n (lambda (x) false)) true)))
;LEQ := λm.λn.ISZERO (SUB m n)
;; returns true if m <= n, false otherwise
(define leq
(lambda (m)
(lambda (n)
(iszero ((sub m) n)))))
;PAIR := λx.λy.λf.f x y
;; represents the pair (x, y)
(define cpair
(lambda (x)
(lambda (y)
(lambda (f)
((f x) y)))))
;FIRST := λp.p TRUE
;; returns first element of a cpair (x, y)
(define cfirst
(lambda (p)
(p true)))
;SECOND := λp.p FALSE
;; returns the second element of a cpair (x, y)
(define csecond
(lambda (p)
(p false)))
;NIL := λx.TRUE
;; represents the empty list
(define cnil
(lambda (x) true)
)
;NULL := λp.p (λx.λy.FALSE)
;; tests for NIL
(define cnull
(lambda (p)
(p (lambda (x)
(lambda (y)
false)))))
;; a (proper) list is either nil, or pair whose second element is a shorter
;; list.
; Y := λf.(λx.f (x x)) (λx.f (x x))
;; the Y combinator --- used to simulate recursion
;;
;; The following implementation of the Y combinator comes from Rosetta Code:
;; https://rosettacode.org/wiki/Y_combinator#Scheme
;;
;; For covenience, it does not use Church numerals or other such basic
;; constructions.
(define Y
(lambda (h)
((lambda (x) (x x))
(lambda (g)
(h (lambda args (apply (g g) args)))))))
(define fac
(Y
(lambda (f)
(lambda (x)
(if (< x 2)
1
(* x (f (- x 1))))))))
(define fib
(Y
(lambda (f)
(lambda (x)
(if (< x 2)
x
(+ (f (- x 1)) (f (- x 2))))))))