Commit Graph

46 Commits (4a6f44ff90436d30dd9f3b98502969bee65c7ccf)

Author SHA1 Message Date
Mike Gerwitz 4a6f44ff90 design/tpl: Formatting of source files
This introduces missing license headers in files and better organizes
tpl.sty into sections.
2021-05-19 10:05:29 -04:00
Mike Gerwitz dfdf92848a design/tpl (Classification Introduction): Codomain {Real=>Bool}
Whoops.  The values of the params are reals, but predicates are all
booleans, having been first transformed by the yet-to-be-formally-defined
matches.
2021-05-19 09:02:48 -04:00
Mike Gerwitz f5b2261f0d design/tpl: Euler font
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.
2021-05-18 16:28:43 -04:00
Mike Gerwitz a488e3549d design/tpl (Classification System): Intro src formatting
Just aligning.  Meant to do this in the previous commit.
2021-05-18 16:15:05 -04:00
Mike Gerwitz bf6cf96169 design/tpl (Classification System): Reduce height for intro vdots
The subscript of the matrix family adds too much vertical space.  This
offsets that to restore it to about what it otherwise would be, since the
second subscript does not get in the way.
2021-05-18 16:14:10 -04:00
Mike Gerwitz 158e045762 design/tpl: geometry package for letterpaper
Was not working properly in vanilla TeX Live image.
2021-05-18 16:03:06 -04:00
Mike Gerwitz d65c061b29 design/tpl: configure script (for appendix)
It's not required; TPL will fall back when missing conf.tex.
2021-05-18 15:56:25 -04:00
Mike Gerwitz 80fd239d95 design/tpl: Letter paper
This is what we'll usually be printing on, after all.
2021-05-18 15:06:35 -04:00
Mike Gerwitz 83e3ade149 design/tpl (Classification System)[Classification Yield]: Allow break after "then"
This was rendering poorly, breaking instead in the middle of "Axiom".
2021-05-18 14:15:52 -04:00
Mike Gerwitz ef231f89fa design/tpl (Classification System): Remove TODO for always/never
This was done in the previous commit.
2021-05-18 14:11:40 -04:00
Mike Gerwitz 8957e6caf0 design/tpl (Classification System): Add always and never figure
This demonstrates the vacuity lemma.
2021-05-18 14:09:27 -04:00
Mike Gerwitz dfa37f5b77 design/tpl: Use \{emph=>dfn} for term introductions
This uses \textsl rather than \emph.
2021-05-18 12:16:11 -04:00
Mike Gerwitz 8a2407d66f design/tpl: Emphasize commutativity of monoids in classification system 2021-05-18 12:13:58 -04:00
Mike Gerwitz 1ec0fc0c7b design/tpl (Notational Convetions): Clean up unneeded bicompi
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.
2021-05-18 10:16:06 -04:00
Mike Gerwitz 2d268f2a55 design/tpl: Initial definition of classifications
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.
2021-05-18 10:09:29 -04:00
Mike Gerwitz 4ea2574a8c design/tpl/tpl.sty: Use autoref for theorem macros 2021-05-17 13:21:56 -04:00
Mike Gerwitz fbe76a5616 design/tpl: Beginnings of classifications in terms of first-order logic
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).
2021-05-14 12:14:11 -04:00
Mike Gerwitz 9bcd7e1d7e design/tpl: Abstract theorem env + label creation 2021-05-14 10:50:49 -04:00
Mike Gerwitz 9fd57872ed design/tpl (Monoids and Sequences): Add missing index entries
Forgot in previous commit.
2021-05-14 10:38:17 -04:00
Mike Gerwitz 8d54420656 design/tpl (Monoids and Sequences): New section 2021-05-14 10:34:13 -04:00
Mike Gerwitz 060a7d0e6c design/tpl: \{log=>l}{and,or}
Don't I feel silly.
2021-05-14 10:34:09 -04:00
Mike Gerwitz 63b502b7df design/tpl: Add ccicons for Copyright line 2021-05-12 10:37:20 -04:00
Mike Gerwitz 1ad6bc93d7 design/tpl (Meta: Typesetting): Correct use of \tameclass
That macro previously expanded into \Classify, but that was undone before
committing to make it clear when one is referring to a variable vs. a
classification as a definition.
2021-05-11 16:52:03 -04:00
Mike Gerwitz 3cb2726737 desgin/tpl: Appendices begin on a new page 2021-05-11 16:50:23 -04:00
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