# Code equivalences from The Little Prover

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

Back to index