Ivory: Zero

zero is the highest level that actually contains values. In fact it contains a single value (+):

(define zero? (curry equal? '(+))

This value (a list containing the symbol +) represents the empty sum, i.e. what we get when adding nothing together. Since it’s a sum, its behaviour can be derived from the sum and product laws.

Addition

Addition is associative: nested sums like (+ a (+ b c) d) are equal to a single sum containing all of those elements, i.e. (+ a b c d).

Since the empty sum (+) contains no elements, its presence in a sum makes no difference to the result, e.g. (= (+ x (+) y) (+ x y)). In other words, it is the identity element for addition.

If all of the elements of a sum are empty sums, the result is equal to the empty sum; for example (+ (+) (+) (+)) is equal (via associativity) to (+). Hence summing any zero values results in another zero value, making zero closed under addition.

Multiplication

We can likewise derive the behaviour of (+) in a product. This time, we use distributivity: a product containing a sum, like (× a b (+ c d) e), equals a sum of products; in this case (+ (× a b c e) (× a b d e)). Importantly, that original sum has the same number of elements as the result; if the original was empty, so is the result! For example (× a b (+) d) equals (+), and likewise for any product containing the empty sum (+). This makes (+) the absorbing element for multiplication; and zero is closed under multiplication.

Negation

Distributivity also applies to negation, so (- (+))

Other operations

zero is closed under negation, since

zero is trivially closed under min and max, since those return one of their given arguments.

We can extend the gcd (greatest common divisor) and lcm (least common multiple) functions to operate on values from zero; in which case those are also closed.

zero is hence a unit type, and a terminal object. It is dual to empty type void.

This level seems rather trivial, but nevertheless it is a valid number system, which is closed under common operations like +, -, ×, max, min, gcd and lcm.