Tutorial 4: Equivalence I

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

Adding two even integers 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) )

This is the same as checking the two boolean values for equality:

add [even] [:] (X, Y) ->| ( X == Y )

If an integer 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.