Commit Graph

72 Commits (57a805b4953ac4b5473d21c3043bc36a7e17b1e5)

Author SHA1 Message Date
Mike Gerwitz bff2b32a52 design/tpl: More TODOs and margin remarks 2021-05-11 16:50:11 -04:00
Mike Gerwitz 9d9535a1b8 design/tpl: Introduce \Classify mathop
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.
2021-05-11 16:37:08 -04:00
Mike Gerwitz d78186461f desgin/tpl: Add \todo margin notes 2021-05-11 16:36:43 -04:00
Mike Gerwitz 08109bc35d design/tpl: Vector addition example: \bicomp{=>i}
The example as presented was incorrect, since \bicomp is undefined for
scalar values.
2021-05-11 13:49:18 -04:00
Mike Gerwitz 7735ba1f29 design/tpl: Remove \exists from classification definitions
The previously-existing notation for this has been removed.  These will be
updated soon to account for vectors and matrices, but until then, this is
simply nonsense.
2021-05-11 13:28:02 -04:00
Mike Gerwitz d49133e8e9 design/tpl: (Disjunctive Classification): Footnote formatting correction
Missing `,' in the \forall set.
2021-05-11 13:24:20 -04:00
Mike Gerwitz 51c87f9938 design/tpl: Reposition disjunctive classification footnote
The original position made it look to much like d^2.
2021-05-11 13:21:05 -04:00
Mike Gerwitz 6dc0ca2454 design/tpl: Show listings in draft mode
What an odd default.
2021-05-11 13:08:25 -04:00
Mike Gerwitz 5808afc8a2 design/tpl: Universal=>conjunctive, existential=>disjunctive classification 2021-05-11 13:06:06 -04:00
Mike Gerwitz 2407af56e4 design/tpl: _-notation clarification (wildcard/hole) 2021-05-11 12:47:28 -04:00
Mike Gerwitz 13317aac6c design/tpl: Vectors and Index Sets \goodbreak
This fits nicely on a single page.  At the time of writing, the previous
section is near the end of the page, so this works reasonably well.
2021-05-11 11:39:23 -04:00
Mike Gerwitz 7f4fc8e3b7 design/tpl: Mostly-complex symbol index entries for Chapter 0 2021-05-11 11:33:12 -04:00
Mike Gerwitz 7624bd2958 design/tpl: TAMER case fix
'T' was lowercased.
2021-05-11 11:32:19 -04:00
Mike Gerwitz 02335f9a4a design/tpl: Clear copyright on Index pages
Apparently index page output uses a different even/odd determination than
the normal article page output.
2021-05-11 11:31:27 -04:00
Mike Gerwitz dfb013ca74 design/tpl: Corrected conjunction/disjunction index placement
They were incorrectly placed at the quantifiers.
2021-05-11 09:59:03 -04:00
Mike Gerwitz cb9ccfe5f3 design/tpl: \vdash=>\infer and index entry 2021-05-10 16:54:19 -04:00
Mike Gerwitz 4e7b882aed design/tpl: Begin symbol list at beginning of index 2021-05-10 16:50:30 -04:00
Mike Gerwitz 176c7785e9 design/tpl: Remove stackengine import
This is no longer needed after conversion of \bicomp to superscript.
2021-05-10 14:29:42 -04:00
Mike Gerwitz c371d12a02 design/tpl: Remove glossary
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.
2021-05-10 14:28:37 -04:00
Mike Gerwitz 8d1c29b4cc design/tpl: bicomp: Use superscript instead of stacking
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.
2021-05-10 14:19:49 -04:00
Mike Gerwitz 0a16808542 design/tpl: Subscript notation for function application
This is convenient and visually appealing in certain circumstances.  That's
highly subjective.
2021-05-10 14:08:11 -04:00
Mike Gerwitz bd454f7a7c design/tpl: The Tame Programming Language initial concept
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.
2021-05-10 13:46:49 -04:00