As in divination, pattern matching. Continues from Groups are numbers (1).
We start from elementary variables, then we define number terms by two operations: substraction and multiplication.
- Variables are terms.
- Substraction (the first line): a is a variable and b is a term, then is a term.
- Multiplication (2nd line): a, b are terms, then is a term.
By pattern matching we can prove for example this:
[update: figure replaced, the initial one was wrong by pattern matching only. The difference is that in this correct figure appears “(a-b)d” instead of the wrong “d(a-b)”]
What does it mean? These are just binary trees. Well let’s take a typing convention
where e, x, … are elements of a vector space and the variables are invertible scalars. Moreover take for simplicity.
Then the previous pattern matching dream says that
which is true, but from all the irrelevant reasons (vector space, associativity and commutativity of addition, distributivity, etc):
What about this one, which is also by pattern matching:
With the previous typing conventions it reads:
which is true because the right hand side is:
Which is funny because it does not make any sense.