Commit Graph

30 Commits (22a9596cf436c4e63290c6468cf9f815b1081a03)

Author SHA1 Message Date
Mike Gerwitz 9c72d397d4 design/tpl: Introduce bibliography
This starts with the Hadamard Product as an example.  It also:

  - Configures BibLaTeX with biber.
  - Renames \undef, since BibLaTeX apparently defines it.
  - Redefines the citation and url colors, since they're bright and ugly.
2021-05-26 13:07:46 -04:00
Mike Gerwitz 972ea13623 design/tpl: {\bullet=>\monoidop}
This abstraction was introduced in the previous commit.
2021-05-26 10:38:36 -04:00
Mike Gerwitz e70933eef8 design/tpl (Vectors and Index Sets): Refinement and rectangular matrix intro
This refines the section a bit and introduces the familiar notation for
rectangular matrices (which normal people just call "matrices").
2021-05-21 16:10:44 -04:00
Mike Gerwitz 8edef8a8c8 design/tpl (\rank): Add macro 2021-05-20 15:28:10 -04:00
Mike Gerwitz 98d724a7d7 design/tpl (Vectors and Index Sets): Remove unique value set example
This ended up not being needed for the definition of the classification
system and just adds noise.
2021-05-20 12:42:51 -04:00
Mike Gerwitz 9ad144d3d4 design/tpl (Classification System): Initial match definition
This is a bit raw; it needs some explanation and examples.
2021-05-20 10:45:44 -04:00
Mike Gerwitz 0d59ff607e design/tpl (XML Notation): Add additional example for literal binding 2021-05-19 13:06:40 -04:00
Mike Gerwitz f71c58b1da design/tpl (Vectors and Index Sets) [Rank]: New definition 2021-05-19 12:58:20 -04:00
Mike Gerwitz aafebbc716 design/tpl: Classification index entries 2021-05-19 10:48:35 -04:00
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 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 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 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 bff2b32a52 design/tpl: More TODOs and margin remarks 2021-05-11 16:50:11 -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 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 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 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 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