summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/stex/doc/packages/stex-features.tex
diff options
context:
space:
mode:
Diffstat (limited to 'macros/latex/contrib/stex/doc/packages/stex-features.tex')
-rw-r--r--macros/latex/contrib/stex/doc/packages/stex-features.tex277
1 files changed, 224 insertions, 53 deletions
diff --git a/macros/latex/contrib/stex/doc/packages/stex-features.tex b/macros/latex/contrib/stex/doc/packages/stex-features.tex
index e70bbaa0e8..b5ce5906d1 100644
--- a/macros/latex/contrib/stex/doc/packages/stex-features.tex
+++ b/macros/latex/contrib/stex/doc/packages/stex-features.tex
@@ -1,18 +1,173 @@
+\begin{sfragment}{The \texttt{mathstructure} Environment}
+\begin{smodule}[ns=https://github.com/slatex/sTeX/doc]{MathStructures}
+ A common occurence in mathematics is bundling several
+ interrelated ``declarations'' together into \emph{structures}.
+ For example:
+ \begin{itemize}
+ \item A \emph{monoid} is a structure $\mathstruct{M,\circ,e}$
+ with $\circ:M\times M\to M$ and $e\in M$ such that...
+ \item A \emph{topological space} is a structure
+ $\mathstruct{X,\mathcal T}$ where $X$ is a set and
+ $\mathcal T$ is a topology on $X$
+ \item A \emph{partial order} is a structure $\mathstruct{S,\leq}$
+ where $\leq$ is a binary relation on $S$ such that...
+ \end{itemize}
+
+ This phenomenon is important and common enough to warrant special
+ support, in particular because it requires being able
+ to \emph{instantiate} such structures (or, rather,
+ structure \emph{signatures}) in order to talk about (concrete
+ or variable) \emph{particular} monoids, topological spaces,
+ partial orders etc.
+
+ \begin{environment}{mathstructure}
+ The \stexcode"mathstructure" environment allows us to do
+ exactly that. It behaves exactly like the
+ \stexcode"smodule" environment, but is itself only allowed
+ inside an \stexcode"smodule" environment, and allows
+ for instantiation later on.
+ \end{environment}
+
+ How this works is again best demonstrated by example:
+ \symdef{funtype}[args=ai]{#1 \comp\to #2}{##1 \comp\times ##2}
+ \symdef{fun}[args=bi]{#1 \comp\mapsto #2}
+ \symdef{set}{\comp{\texttt{Set}}}
+
+ \stexexample{%
+\begin{mathstructure}{monoid}
+ \symdef{universe}[type=\set]{\comp{U}}
+ \symdef{op}[
+ args=2,
+ type=\funtype{\universe,\universe}{\universe},
+ op=\circ
+ ]{#1 \comp{\circ} #2}
+ \symdef{unit}[type=\universe]{\comp{e}}
+\end{mathstructure}
+
+A \symname{monoid} is...
+ }
+ Note that the \stexcode"\symname{monoid}" is appropriately
+ highlighted and (depending on your pdf viewer)
+ shows a URI on hovering -- implying that the \stexcode"mathstructure"
+ environment has generated a \emph{symbol} |monoid| for us.
+ It has not generated a semantic macro though, since
+ we can not use the |monoid|-symbol \emph{directly}. Instead,
+ we can instantiate it, for example for integers:
+
+ \stexexample{%
+\symdef{Int}[type=\set]{\comp{\mathbb Z}}
+\symdef{addition}[
+ type=\funtype{\Int,\Int}{\Int},
+ args=2,
+ op=+
+]{##1 \comp{+} ##2}
+\symdef{zero}[type=\Int]{\comp{0}}
+
+$\mathstruct{\Int,\addition!,\zero}$ is a \symname{monoid}.
+ }
+
+ So far, we have not actually instantiated |monoid|, but now
+ that we have all the symbols to do so, we can:
+
+ \stexexample{%
+\instantiate{intmonoid}{monoid}{\mathbb{Z}_{+,0}}[
+ universe = Int ,
+ op = addition ,
+ unit = zero
+]
+
+$\intmonoid{universe}$, $\intmonoid{unit}$ and $\intmonoid{op}{a}{b}$.
+
+Also: $\intmonoid!$
+ }
+ \begin{function}{\instantiate}
+ So summarizing:
+ \stexcode"\instantiate" takes four arguments: The
+ (macro-)name of the instance, a key-value pair assigning
+ declarations in the corresponding \stexcode"mathstructure"
+ to symbols currently in scope, the name of the \stexcode"mathstructure"
+ to instantiate, and lastly a notation for the instance itself.
+
+ It then generates a semantic macro that takes as argument
+ the name of a declaration in the instantiated \stexcode"mathstructure"
+ and resolves it to the corresponding instance of that particular declaration.
+ \end{function}
+
+ \begin{mmtbox}
+ \stexcode"\instantiate" and \stexcode"mathstructure" make use of the
+ \emph{Theories-as-Types} paradigm (see \cite{MueRabKoh:tat18}):
+
+ \stexcode"mathstructure{<name>}" simply creates a nested theory with name
+ |<name>-structure|. The \emph{constant} |<name>| is defined as
+ |Mod(<name>-structure)| -- a \emph{dependent record type with manifest fields},
+ the fields of which are generated from (and correspond to) the constants in
+ |<name>-structure|.
+
+ \stexcode"\instantiate" generates a constant whose definiens is a record term of
+ type |Mod(<name>-structure)|, with the fields assigned based on the respective
+ key-value-list.
+ \end{mmtbox}
+
+ Notably, \stexcode"\instantiate" throws an error if not \emph{every}
+ declaration in the instantiated \stexcode"mathstructure" is being assigned.
+
+ You might consequently ask what the usefulness of \stexcode"mathstructure"
+ even is.
+
+ \begin{function}{\varinstantiate}
+ The answer is that we can also instantiate a
+ \stexcode"mathstructure" with a \emph{variable}.
+ The syntax of \stexcode"\varianstantiate" is equivalent
+ to that of \stexcode"\instantiate", but all of the key-value-pairs
+ are optional, and if not explicitly assigned (to a symbol \emph{or}
+ a variable declared with \stexcode"\vardef") inherit their notation
+ from the one in the \stexcode"mathstructure" environment.
+ \end{function}
+
+ This allows us to do things like:
+
+ \stexexample{%
+\varinstantiate{varM}{monoid}{M}
+
+A \symname{monoid} is a structure
+$\varM!:=\mathstruct{\varM{universe},\varM{op}!,\varM{unit}}$
+such that
+$\varM{op}!:\funtype{\varM{universe},\varM{universe}}{\varM{universe}}$ ...
+}
+
+and
+
+\stexexample{%
+ \varinstantiate{varMb}{monoid}{M_2}[universe = Int]
+
+ Let $\varMb!:=\mathstruct{\varMb{universe},\varMb{op}!,\varMb{unit}}$
+be a \symname{monoid} on $\Int$ ...
+ }
+
+ We will return to these two example later, when we also know
+ how to handle the \emph{axioms} of a monoid.
+\end{smodule}
+\end{sfragment}
+
+\begin{sfragment}{The \texttt{copymodule} Environment}
+
+ \textcolor{red}{TODO: explain}
+
Given modules:
-\stexexample{
- \begin{smodule}{magma}
- \symdef{universe}{\comp{\mathcal U}}
- \symdef{operation}[args=2,op=\circ]{#1 \comp\circ #2}
- \end{smodule}
- \begin{smodule}{monoid}
- \importmodule{magma}
- \symdef{unit}{\comp e}
- \end{smodule}
- \begin{smodule}{group}
- \importmodule{monoid}
- \symdef{inverse}[args=1]{{#1}^{\comp{-1}}}
- \end{smodule}
+\stexexample{%
+\begin{smodule}{magma}
+ \symdef{universe}{\comp{\mathcal U}}
+ \symdef{operation}[args=2,op=\circ]{#1 \comp\circ #2}
+\end{smodule}
+\begin{smodule}{monoid}
+ \importmodule{magma}
+ \symdef{unit}{\comp e}
+\end{smodule}
+\begin{smodule}{group}
+ \importmodule{monoid}
+ \symdef{inverse}[args=1]{{#1}^{\comp{-1}}}
+\end{smodule}
}
We can form a module for \emph{rings} by ``cloning''
@@ -20,48 +175,64 @@ an instance of |group| (for addition) and |monoid| (for multiplication),
respectively, and ``glueing them together'' to ensure they share the
same universe:
-\stexexample{
- \begin{smodule}{ring}
- \begin{copymodule}{group}{addition}
- \renamedecl[name=universe]{universe}{runiverse}
- \renamedecl[name=plus]{operation}{rplus}
- \renamedecl[name=zero]{unit}{rzero}
- \renamedecl[name=uminus]{inverse}{ruminus}
- \end{copymodule}
- \notation*{rplus}[plus,op=+,prec=60]{#1 \comp+ #2}
- %\setnotation{rplus}{plus}
- \notation*{rzero}[zero]{\comp0}
- %\setnotation{rzero}{zero}
- \notation*{ruminus}[uminus,op=-]{\comp- #1}
- %\setnotation{ruminus}{uminus}
- \begin{copymodule}{monoid}{multiplication}
- \assign{universe}{\runiverse}
- \renamedecl[name=times]{operation}{rtimes}
- \renamedecl[name=one]{unit}{rone}
- \end{copymodule}
- \notation*{rtimes}[cdot,op=\cdot,prec=50]{#1 \comp\cdot #2}
- %\setnotation{rtimes}{cdot}
- \notation*{rone}[one]{\comp1}
- %\setnotation{rone}{one}
- Test: $\rtimes a{\rplus c{\rtimes de}}$
- \end{smodule}
+\stexexample{%
+\begin{smodule}{ring}
+ \begin{copymodule}{group}{addition}
+ \renamedecl[name=universe]{universe}{runiverse}
+ \renamedecl[name=plus]{operation}{rplus}
+ \renamedecl[name=zero]{unit}{rzero}
+ \renamedecl[name=uminus]{inverse}{ruminus}
+ \end{copymodule}
+ \notation*{rplus}[plus,op=+,prec=60]{#1 \comp+ #2}
+%\setnotation{rplus}{plus}
+ \notation*{rzero}[zero]{\comp0}
+%\setnotation{rzero}{zero}
+ \notation*{ruminus}[uminus,op=-]{\comp- #1}
+%\setnotation{ruminus}{uminus}
+ \begin{copymodule}{monoid}{multiplication}
+ \assign{universe}{\runiverse}
+ \renamedecl[name=times]{operation}{rtimes}
+ \renamedecl[name=one]{unit}{rone}
+ \end{copymodule}
+ \notation*{rtimes}[cdot,op=\cdot,prec=50]{#1 \comp\cdot #2}
+%\setnotation{rtimes}{cdot}
+ \notation*{rone}[one]{\comp1}
+%\setnotation{rone}{one}
+ Test: $\rtimes a{\rplus c{\rtimes de}}$
+\end{smodule}
}
\textcolor{red}{TODO: explain donotclone}
+
+\end{sfragment}
+
+\begin{sfragment}{The \texttt{interpretmodule} Environment}
+
+ \textcolor{red}{TODO: explain}
+
+\stexexample{%
+\begin{smodule}{int}
+ \symdef{Integers}{\comp{\mathbb Z}}
+ \symdef{plus}[args=2,op=+]{#1 \comp+ #2}
+ \symdef{zero}{\comp0}
+ \symdef{uminus}[args=1,op=-]{\comp-#1}
+
+ \begin{interpretmodule}{group}{intisgroup}
+ \assign{universe}{\Integers}
+ \assign{operation}{\plus!}
+ \assign{unit}{\zero}
+ \assign{inverse}{\uminus!}
+ \end{interpretmodule}
+\end{smodule}
+}
+
+\end{sfragment}
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "../stex-manual"
+%%% End:
-\stexexample{
- \begin{smodule}{int}
- \symdef{Integers}{\comp{\mathbb Z}}
- \symdef{plus}[args=2,op=+]{#1 \comp+ #2}
- \symdef{zero}{\comp0}
- \symdef{uminus}[args=1,op=-]{\comp-#1}
-
- \begin{interpretmodule}{group}{intisgroup}
- \assign{universe}{\Integers}
- \assign{operation}{\plus!}
- \assign{unit}{\zero}
- \assign{inverse}{\uminus!}
- \end{interpretmodule}
- \end{smodule}
-} \ No newline at end of file
+% LocalWords: circ,e intmonoid MueRabKoh:tat18 varinstantiate 2,op runiverse rplus prec
+% LocalWords: rzero uminus ruminus plus,op uminus,op rtimes cdot,op cdot,prec 1,op
+% LocalWords: donotclone intisgroup