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?

Any argument we can give to add [odd] will return the same results as xor.

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

Wait a second! What is going on here?

Path semantics defines equivalence between two functions as them being 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.