# 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-nil
(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``