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: equalsame
The rule equalsame
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 NotaNumber (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 nonbroken equality
The rules for equality are very simple:
 Any entity is equal to itself.
 Reflexivity: Given two entities
a
andb
; ifa == b
, thenb == a
. Ifa != b
thenb != a
.  Transitivity: Given three entities
a
,b
andc
; ifa == b
andb == c
, thena == c
.
Write code that ensures these rules are followed. There are two supersimple 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
ofe1.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: iftrue
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: iffalse
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: ifsame
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 ifsame
twice to replace the whole mess with navigateToHome();
.
Nested true comparisons: ifnestA
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 iftrue
. 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 ifnestA (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: ifnestE
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 ifnestA
, 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 ifnestE
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: ifand
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.