"Why then, build me thy fortunes upon the basis"
-- Shakespeare, Twelfth Night
Act III, Scene II, Line 31
I recently finished The Little Prover. In The Little Prover we find the following Axioms of Con:
(dethm atom/cons (x y)
(equal (atom (cons x y)) 'nil)
(dethm car/cons (x y)
(equal (car (cons x y)) x))
(dethm cdr/cons (x y)
(equal (cdr (cons x y)) y))
(dethm cons/car+cdr (x)
(if (atom x)
't
(equal (cons (car x) (cdr x)) x)))
The way I learn best is by showing myself that something makes sense, so I went through showing myself these axioms in Clojure.
Looking at atom/cons in the code above we see that Clojure does not have atom but (complement sequential?) is close enough if we are working with sequential collections so we'll use that. Using the definition that an atom is not a sequential collection we see in the code above that cons "always" yields not an atom.
Next looking at car/cons in the code above we see that using first (Clojure's car) on a cons "always" yields the head of the sequential collection, which makes prefect sense since that is what one expects from first.
The other side of car/cons is cdr/cons. Looking at the code above we see that using rest (Clojure's cdr) on a cons "always" yields the tail of the sequential collection, which again makes prefect sense since that is what one expects from rest.
Last we look at cons/car+cdr. Looking at the code we see that if we do not have an atom that first and rest (Clojure's car and cdr) together yield the sequential collection, which again is what one would expect.
So what does any of this give us? We now have a firm foundation on which to define other theorems and proofs about our statements using these axioms as our basis. This is very powerful and I would argue that this is better having tests.
If this interests you I would recommend reading The Little Prover or working your way through the flying tour of ACL2.
