I find this provides a visualization that is likely to be significantly more
intuitive for others. It even holds when the matrix is not
rectangular (yes, I know, it's not really a matrix then), so long as all
matrices share the same respective K_j.
This uses the same variable subscript on \equiv itself to define the symbol,
rather than the previous symbol which looked like equiv rotated, but also
looked too much like a turnstile used for "infer", a metalanguage construct
that is not appropriate here. It kept bothering me.
I removed this when I added concmath, thinking that it would include it for
me, and apparently I never re-added it after realizing that it didn't.
I'm a big fan of the typography of Concrete Mathematics.
This was originally going to be used to define @yields for the classifier,
but I took a very different approach which doesn't require reasoning about
the system in terms of recursion.
This defines @as and @yields, but does not yet define matches formally.
It's also missing index entries, which I'll take the time to add after I'm
sure things are staying as they are.
This was quite a bit of work, and the approach I took is different than I
originally expected, so Section 0 can use some cleanup.
There is more to come from here.
This is going to evolve a great deal, and note that the yield definition is
completely absent.
It may be time to switch to natural deduction (Gentzen-style).
This will be used as an IR of sorts to eliminate the XML, which will be far
too verbose to use in proofs. It also allows us to attach behavior to the
operator, which will end up defining two values for @as and @yields.
This is an unnecessary feature to maintain right now. I will include
symbols at the very beginning of the index, which is common in mathematics
texts, and may will add a table of common symbols in the future.
Stacking originally seemed like a good idea, but perhaps this does read a
bit better (and looks more like the composition operation being applied),
and composes a bit better if we needed e.g. \bicomp\bicomp{R}.
It's also less ambiguous when it's over a larger expression. For example,
\bicomp{[A]} places \circ over top of the A, which looks as if it's
[\bicomp{A}]. It's obvious what the intention is in that context, since
\bicomp{A} makes no sense, but there could be other situations where it
doesn't. With this change, it results in {[A]}^\circ.
There's a lot of change that's likely going to take place with this thing,
but it's a start. The abstract summarizes the purpose of this---to formally
define TAME in terms of algebra, first-order logic, and [ZFC] set theory.
This came about while working on compiler changes and optimizations, since
it's difficult to ensure correctness (and discover further optimizations)
without being able to formally define the language. The focus at the moment
is the classification system rewrite, which can be expressed in terms of
first order logic and set theory.
This commit contains essentially a POC with some carefully chosen
mathematical foundations (abstractions of which are subject to change) and a
basic representation of a subset of the classification system for scalars.
Mike Gerwitz