Basic Laws of μScheme

This handout shows algebraic laws for many of the syntactic forms, primitive functions, and predefined functions of μScheme. A law is typically named by the function that is applied and the form it is applied to. Some names are shown in comments.

Primitive list functions

(null? '())         == #t   ; null-empty
(null? (cons x xs)) == #f   ; null-cons
(car   (cons x xs)) == x    ; car-cons
(cdr   (cons x xs)) == xs   ; cdr-cons

Calling (car '()) or (cdr '()) results in a checked run-time error.

(pair? '())         == #f  ; pair-empty
(pair? (cons x xs)) == #t  ; pair-cons

Laws of if

(if #t x y) == x  ; if-true
(if #f x y) == y  ; if-false
(if (not p) x y) == (if p y x) ; if-not
(if p #t #f) == p
(if p #f #t) == (not p)

Boolean functions

(and p q) == (and q p)
(and p #t) == p
(and p #f) == #f

(or p q) == (pr q p)
(or p #t) == #t
(or p #f) == p

List functions

(append '()         xs) == xs
(append (cons z zs) ys) == (cons z (append zs ys))

(reverse '())         == '()
(reverse (cons x xs)) == (append (reverse xs) (cons x '()))

(revapp '()         ys) == ys
(revapp (cons x xs) ys) == (revapp xs (cons x ys))

(length '())         == 0
(length (cons x xs)) == (+ 1 (length xs))

S-expressions

(equal? v1 v2)                 == (= v1 v2), both atoms
(equal? (cons x y) (cons w z)) == (and (equal? x w) 
                                       (equal? y z))
(equal? v1 v2)                 == #f, all other cases

Sets as lists

(member? x '())        == #f
(member? x (cons x s)) == #t
(member? x (cons y s)) == (member? x s), x != y

Association lists

(find x '()) == '()
(find (bind ...)) == a homework problem

(alist-first-key       (bind k v ps)) == k
(alist-first-attribute (bind k v ps)) == v

Higher-order functions

(exists? p? '()) == #f
(exists? p? (cons x xs)) == #t, when (p? x) 
(exists? p? (cons x xs)) == (exists? p? xs), when not (p? x)

(all? p? '()) == #t
(all? p? (cons x xs)) == (all? p? xs), when (p? x)
(all? p? (cons x xs)) == #f, when not (p? x)

(filter p? '()) == '()
(filter p? (cons y ys)) == (cons y (filter p? ys)), if (p? y)
(filter p? (cons y ys)) == (filter p? ys), if not (p? y)

(map f '())         == '()                     ; map-nil
(map f (cons y ys)) == (cons (f y) (map f ys)) ; map-cons

(foldr (plus z '()))         == z
(foldr (plus z (cons y ys))) == (plus y (foldr plus z ys))

(foldl (plus z '()))         == z
(foldl (plus z (cons y ys))) == (foldl plus (plus y z) ys)

(((curry f) x) y) == (f x y) 
((uncurry f) x y) == ((f x) y)

((o f g) x) == (f (g x)) ; apply-compose