COMP 105, Fall 2019
This web page 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.
(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
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)
(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
(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))
(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
(member? x '()) == #f
(member? x (cons x s)) == #t
(member? x (cons y s)) == (member? x s), x != y
(find x '()) == '()
(find (bind ...)) == a homework problem
(alist-first-key (bind k v ps)) == k
(alist-first-attribute (bind k v ps)) == v
(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