Tutorial 6: Normal Path Composition

In last tutorial, you learned about expressions similar to:

concat [length] <=> add

It is common to use len as a shorthand for length, skip spaces in front of paths and not use [:] explicitly.

For example:

concat[len] <=> add

add[even](true, true) = true

Now, consider the following:

∵ concat[len][odd]
∴ add[odd]
∴ xor

The ∵ symbol means "because" and the ∴ symbol means "therefore".

One can also do this:

∵ concat[len x len -> len][odd x odd -> odd]
∴ concat[len][odd]
∴ add[odd]
∴ xor

Or, this:

∵ concat[odd . len]
∴ concat[len][odd]
∴ add[odd]
∴ xor

Here, the . in odd . len is function composition.

Or, even this:

∵ concat[(odd . len) x (odd . len) -> (odd . len)]
∴ concat[odd . len]
∴ concat[len][odd]
∴ add[odd]
∴ xor

When we chain expressions of the form f[g1][g2], this is called "normal path composition".

Consider the following:

∵ concat[len x len -> id][id x id -> len]
∴ concat[(id . len) x (id . len) -> (len . id)]
∴ concat[len x len -> len]
∴ concat[len]
∴ add

The problem here is that we started thinking about a normal path which is completely imaginary:

concat[len x len -> id]

There is no solution!

This means, that normal paths have to be treated as mathematical objects on their own, not just syntax sugar.

f[g1 -> g2] == g2 . f . inv(f)

Here, the inv operator is imaginary, hence an "imaginary inverse" operator.

In Path Semantical Logic, one expresses an "actual inverse" of f as a proof of ~inv(f). By decoupling the model of the inverse from syntactical manipulation of expressions, solvers (such as theorem proving assistants or automated theorem provers) can prove more stuff in less steps.

This idea is very similar to how complex numbers were introduced to solve algebraic problems, because complex numbers are easier to use in the theorem proving process than real numbers.

Normal paths simplifies reasoning about functions in the same way complex numbers simplifies reasoning about real numbers.

In the next tutorial, you will learn about hypertorus homotopy.