Tutorial 4: Equivalence I

In the last tutorial you learned that mathematical ideas can be expressed using paths.

Adding two even numbers always results in an even number.

can be expressed as:

add [even] [:] (true, true) -> true

However, this is not the whole story!

add [even] [:]
  (true, true) -> true
  (false, false) -> true
  (true, false) -> false
  (false, true) -> false

We could write all these functions as a computation using ^ (xor) and ! (not):

add [even] [:] (X, Y) -> ( !(X ^ Y) )

If a number is even, then it is not odd and vice versa.

So, we can write:

add [odd] [:] (X, Y) -> ( X ^ Y )

With a function xor(bool, bool) -> bool, we can write:

add [odd] = xor

Now we have expressed an equivalence between two functions.

In the next tutorial we will explore further what equivalence means.