Axioms of Equal in Clojure

"In quantity equals not one of yours."
-- Shakespeare, Henry IV Part I
Act III, Scene I, Line 93

In The Little Prover we find the following Axioms of Equal:

(dethm equal-same (x) 
  (equal (equal x x) 't))

(dethm equal-swap (x y) 
  (equal (equal x y) (equal y x)))

(dethm equal-if (x y)
  (if (equal x y
    (equal x y)
    't)))

I learn best by doing, so I showed myself these axioms in Clojure.



Looking at equal-same we see that if we have something which is the same then those values are equal.  Nothing shocking, unless you are using reference equivalence which we are not.

Next we look at equal-swap which states that equivalence is commutative meaning x = y is the same as y = x.  Again nothing shocking.

Last we look at equal-if which states that if something is equal once it will be equal again.  Note that this assumes that values are immutable which they are (for the most part) in Clojure.  This axiom is rather interesting when paired with lazy evaluation, as we see with the following:

(is (true? 
  (if (= :yep :yep) 
      (= :yep :yep) 
      (throw 
        (IllegalStateException. "How the hell did we get here?")))))

When the statement is evaluated we do not have the Exception thrown!  This is a great benefit of the if special form in Clojure.  We do see this awesomeness has limits:

(let [x (repeat 42)
      y x]
  (is (true? 
    (if (= x y)
      (= x y)
      false)))) 

but fails when the infinite sequence is not the same "reference"

(let [x (repeat 42) 
      y (repeat 42)]
  (is (true?
    (if (= x y)
        (= x y)
        false)))))

Despite the second example of comparing with an infinite sequence not finishing, the if special form is awesome and shows the power of the equal-if axiom paired with lazy evaluation.

These axioms are very powerful and I would argue are more useful than tests. If this interests you I would recommend reading The Little Prover or working your way through the flying tour of ACL2.

Axioms of If in Clojure

"How if I answer no?"
-- Shakespeare, Hamlet
Act V, Scene II, Line 167

In The Little Prover we find the following Axioms of If:

(dethm if-true (x y)
  (equal (if 't x y) x))

(dethm if-false (x y)
  (equal (if 'nil x y) y)

(dethm if-same (x y)
  (equal (if x y y) y)

(dethm if-nest-A (x y z)
  (if x
    (equal (if x y z) y)
    't))

(dethm if-nest-E (x y z)
  (if x
    't
    (equal (if x y z) z)))

The way I learn best is by trying doing, so I showed myself these axioms in Clojure.



Looking at if-true we see that if we have a true premise that we always take the answer part of the if.

(if premise answer else)

This is not a shock to anyone, but is very useful.

Moving on we see if-false states that if we have a false premise that we always take the else part of the if.  Again nothing shocking but very useful.

Next we see if-same which states that if the answer and else are the same then the premise does not matter.  This makes complete logical sense, but I'll admit I never really thought of it before.

Now let us look at if-nest-A which states that if the condition is true in the premise then it must be true in the answer part.  This is very awesome, we can now eliminate code by simply looking for redundant ifs.  We see this in the following:

given x is true 

(if x 
  (if x :yep :nope)
  :nope)))))

We see that we have  the(if what-ever in the outside which matches the (if what-ever in the answer part thus we can eliminate it pulling it up (in the code above the :yep), since if the premise is true on the outside it is true on the inside.  This axiom is very useful in refactoring code and I figured it out for myself a long time ago and find myself using it all the time, it is nice to know that it has a solid theoretical basis.

Last we see the anti of if-nest-A, if-nest-E.  if-nest-E states that if the condition is false in the premise then it must be false in the else part.  We see this in the following:

given x is false

(if x
  :nope
  (if x :nope :yep))

We see that we have the (if what-ever in the outside which matches the (if what-ever in the else part thus we can eliminate it pulling it up (in the code above the :yep), since if the premise is false on the outside it is false on the inside.  Again, this is very useful in eliminating code.

These axioms are very powerful and I would argue are more useful than tests.  If this interests you I would recommend reading The Little Prover or working your way through the flying tour of ACL2.

Axioms of Cons in Clojure

"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.

Showing Map Distributes Over Functional Composition OR Fun With Clojure

"Here by the cheeks I'll drag thee up and down."
-- Shakespeare, Henry VI Part 1
Act I, Scene III, Line 51

I love to try things out for myself.  Whenever I am trying to understand idea I need to show myself that the idea is valid.  Sometimes I will just accept something, but if I really want to understand it I will show myself that it makes sense.

While rereading Dr. Hutton's paper "A tutorial on the universality and expressiveness of fold", I came back across the following statement, "the map operator distributes over function composition".  Being the kind of person which likes to show things to myself I figured I'd show myself this idea in Clojure as part of my daily kata.



Looking at the code above we see the following:

• map f · map g = map (f · g)
• r/map f · r/map g = r/map (f · g)
• reduction f · reduction g = reduction (f · g)

So what does this give us?  Having this property we are allowed to improve the performance of our code by composing a series of transformation against a collection to a single transformation of the collection dragged through a series of composed functions.  In fact this is the whole idea behind streams.

Taken straight from Raoul-Gabriel Urma's article in Java Magazine, "[i]n a nutshell, collections are about data and streams are about computations."  Thinking about processing as a series of computation we see how we can naturally think about composing our computations together and then drag the data through using a higher order function like map to preform the series of transformations in one pass.