Tutorial 5: Equivalence II

In the last tutorial you learned that we can express equivalence:

add [even] <=> eq
add [odd] <=> xor

What does equivalence mean?

Equivalences as relation == in mathematics is a relation with 3 axioms:

• A == A (reflexivity)
• (A == B) => (B == A) (symmetry)
• (A == B) & (B == C) => (A => C) (transitivity)

However, from a "path" perspective, equivalence can be translated as "uniquely determined". Equivalence gives us the tools to talk about what it means to distinguish objects or make them equal to each other.

Other words that mathematicians use is "extensionality" and "intensionality" to talk about whether objects are made equal when their properties are equal (extensional), or not (intensional).

Any argument we can give to add [odd] will return the same results as xor. Therefore, add [odd] is extensionally equal to xor.

But, add [odd] takes (bool, bool) and returns a bool! These are types and not values! How can this be equivalence?

Wait a second! What is going on here?

Path semantics defines equivalence between two functions as them being identical.

Remember the following rule:

[F] [:] X == [:] [F] X

Since we can put an [:] after add [odd], anything that follows must also satisfy add [:] [odd]. It means, when using xor [:], it can be interpreted in a different way using add and odd.

The rule above ensures that these two functions are not just equivalent, but also identical.

How is "identical" different from "equal"?

This gets easier to understand through a thought experiment:

You have a key to a door A.
If a door B is identical to door A, then you can use the same key!
If door A leads down a corridor, then B must lead down the same corridor!
Whatever you see when opening door A, you see when opening door B!
A and B are identical!

When two functions are identical, they behave exactly the same, no matter what paths you use as arguments.

For example, when concatenating two lists, the length of the resulting list is the sum of the two lists:

concat [length] <=> add

Since add [odd] <=> xor, we can write:

concat [length] [odd] <=> xor

So, when concatenating two lists, one with odd number of elements and one with even number of elements, the resulting list always has an odd number of elements.

No matter which path we take from a function identical to another, we get the same results.

In the next tutorial, you will learn about normal path composition.