There are books out there that teach you way more than expected. One of these books is 'The Little Prover', which is around proving certain things about code by transforming it into different code that actually has the exact same behaviour. From it, I learned an improved ability to massage code, and twist it to whatever way I need. This also helps untwisting code so that we can make it understandable.

Equivalent code

First of all, we must indicate that each and every of these code equivalences assume that each of the parts has no side effects. No getters, setters, updaters, no side effects at all. Pure Functional Programming. If your code has limited and isolated side effects, you may be able to apply some of these. If your code has random side effects all over the place, code equivalence is another tool you can't use.

Remember it for when you are about to place side effects all over the place.

Two pieces of code are equivalent, if under all circumstances, they return the same value, differing (maybe) on performance. For example, all stable sorting algorithms are equivalent, because all will return the same result, but may (and will) differ in performance. Which means you can go around swapping one stable sorting algorithm with another, and get different performance characteristics. The point is that you can go swapping things for equivalent things without affecting the correctness of the code.

Following this train of thought, we can begin our journey with sorting:

(equals
  mergesort
  bubblesort)

This tells us that mergesort is equivalent to bubblesort, in the sense that I can pick a piece of code that uses bubblesort, replace bubblesort with mergesort, and it is guaranteed that the code will return the same values for the same inputs. Also, because mergesort has better performance characteristics than bubblesort, we are likely to get a significant performance improvement.

Thus the first rule is that we can replace equivalent code with its equivalence. A corollary is that we can replace the equivalence with equivalent code, with may sound confusing, but means we can apply the rules both ways.

If a = b, then when I see a, I can replace it with b; but also, when I see b, I can replace it with a.

Having said this, let's check some rules.

Any value is equals to itself: equal-same

The rule equal-same tells us that any value is equals to itself.

(equals
  (equals a a)
  true)

This is true almost everywhere, with very few exceptions:

• Floating point Not-a-Number (NaN). The IEEE decided that two NaNs can't be equal even if they are made of the same underlying bits. They have their reasons, so let's push floating point numbers outside this equivalence for now.
• Botched equality comparisons. If your language allows you to define your own equality, you can make a broken one that doesn't follow the basic rules and expectations from equality.

This means that, wherever we see a == a, we can replace it with true, and if we see true, we can replace it with a == a for any a.

Side note: How to make non-broken equality

The rules for equality are very simple:

• Any entity is equal to itself.
• Reflexivity: Given two entities a and b; if a == b, then b == a. If a != b then b != a.
• Transitivity: Given three entities a, b and c; if a == b and b == c, then a == c.

Write code that ensures these rules are followed. There are two super-simple implementations that follow it:

• Good simple implementation 1: two entities are equal if they are the same entity, and not equal if they aren't the same entity.

  This is usually implemented as comparing the memory address of the two entities. If the address is the same, inevitably both entities will be the same, because if you modify one, the other will be affected exactly the same way.

• Good simple implementation 2: two entities are equal if, comparing each and every field from the two, each and every pair of fields (the same fields from the two entities) are equals, and different if any pair of fields is different.

  This is usually implemented as a massive and of e1.field1 == e2.field1, e1.field2 == e2.field2 and so on, assuming the field equality is also well implemented.

If your entities cannot have these simple implementations, you should strive to confirm the three rules above are followed.

A conditional branch with true as the condition is equivalent to the then branch: if-true

Given a conditional if, if the condition is true, then the result is the then branch.

(equals
  (if true b c)
  b)

This may look obvious, but it is often the case that the true you get in the condition may come from other transformations, so it may become obvious after we have done the right transformations.

You can use it in reverse to introduce a condition. Just put b in the then branch, and use whatever c you require for the situation.

A conditional branch with false as the condition is equivalent to the else branch: if-false

Given a conditional if, if the condition is false, then the result is the else branch.

(equals
  (if false b c)
  c)

Again, this may look obvious, but it is often the case that the false you get in the condition may come from other transformations, so it may become obvious after we have done the right transformations.

You can use it in reverse to introduce a condition. Just put c in the else branch, and use whatever b you require for the situation.

A conditional with the same values in both then and else branches is equivalent to any of the branches: if-same

Given a conditional if, with any condition, if both branches then and else are equal, the result is the same.

(equals
  (if a b b)
  b)

Now we start to dig into nasty code. There have been cases I have seen in the past, that, refactor after refactor, change after change, you start to see things like:

if(user.role === "OWNER") {
  if(user.plan === "BUSINESS") {
    navigateToHome();
  } else {
    navigateToHome();
  }
} else {
  navigateToHome();
}

In the past we may have implemented special actions for the role OWNER and BUSINESS plans, but we eventually moved these actions to somewhere else. So now, if your role is OWNER and your plan is BUSINESS, then you go to the home page. If your role is OWNER, but your plan is not BUSINESS, then you also go the the home page. Finally, if your role is not OWNER, then you also go to the home page.

Use if-same twice to replace the whole mess with navigateToHome();.

Nested true comparisons: if-nest-A

If we can confirm a condition on a outside conditional, the condition remains true in an internal conditional.

(if x
  (equal (if x y z) y)
  true)

This is somewhat equivalent to if-true. First, we confirm that the condition is true, then we can guarantee that it will be true. Let's see an example:

if(user.role === "OWNER") {
  if(user.plan === "BUSINESS") {
    if(user.role === "OWNER" {  // We checked on the outer condition for `user.role === "OWNER"`.
      d                         // It is guaranteed here that it will be true.
    } else {
      c                         // This is dead code
    }
  } else {
    b
  }
} else {
  a
}

We can replace this code, applying if-nest-A (user.role === "OWNER") (d) (c) with:

if(user.role === "OWNER") {
  if(user.plan === "BUSINESS") {
    d
  } else {
    b
  }
} else {
  a
}

and we removed all traces of c and a conditional. Nice improvement.

Nested false comparisons: if-nest-E

If we can disprove a condition on a outside conditional, the condition remains false in an internal conditional.

(if x
  true
  (equal (if x y z) z))

This axiom is similar to if-nest-A, but applied to the else branch. Let's work out another example:

if(user.role === "OWNER") {
  a
} else {
  if(user.role === "OWNER") {  // If we got here, is because user.role !== "OWNER"
    b                          // Therefore it's guaranteed that we will never return `b`
  } else {
    c                          // and will always return `c`
  }
}

Applying if-nest-E with parameters user.role === "OWNER", b and c, we can conclude that the code above is equivalent to:

if(user.role === "OWNER") {
  a
} else {
  c
}

Multiple nested true comparisons: if-and

The Little Prover doesn't have this rule, but we can derive it and understand it:

(equal
  (if x (if y a b) b)
  (if (and x y) a b))

Which means if we have two conditions nested one inside the other, the final then branch will be called only if both the two conditions turn to be true, which is equivalent to an and of the two conditions.

You can use this rule to construct or split complex conditions. An example:

if(user.role === "OWNER") {
  if(user.plan === "BUSINESS") {
    b
  } else {
    c
  }
} else {
  c
}

is equivalent to

if(user.role === "OWNER && user.plan === "BUSINESS") {
  b
} else {
  c
}

Code Mathematics

This is one small example on how you can apply Mathematics (and Symbolic Calculus) to reason and operate on code. You can use these kind of rules to modify and refactor code while guaranteeing that you are preserving the behaviour of the program.