\begin{smodule}[ns=https://github.com/slatex/sTeX/doc]{SymbolsAndNotations} \begin{sfragment}{Declaring New Symbols and Notations} Inside an \stexcode"smodule" environment, we can declare new \sTeX symbols. \begin{function}{\symdecl} The most basic command for doing so is using \stexcode"\symdecl{symbolname}". This introduces a new symbol with name |symbolname|, arity $0$ and semantic macro \stexcode"\symbolname". The starred variant \stexcode"\symdecl*{symbolname}" will declare a symbol, but not introduce a semantic macro. If we don't want to supply a notation (for example to introduce concepts like ``abelian'', which is not something that has a notation), the starred variant is likely to be what we want. \end{function} \begin{mmtbox} \stexcode"\symdecl" introduces a new \omdoc/\mmt constant in the current module (=\omdoc/\mmt theory). Correspondingly, they get assigned the URI |?|. \end{mmtbox} Without a semantic macro or a notation, the only meaningful way to reference a symbol is via \stexcode"\symref",\stexcode"\symname" etc. \stexexample{% \symdecl*{foo} Given a \symname{foo}, we can... } Obviously, most semantic macros should take actual \emph{arguments}, implying that the symbol we introduce is an \emph{operator} or \emph{function}. We can let \stexcode"\symdecl" know the \emph{arity} (i.e. number of arguments) of a symbol like this: \stexexample{% \symdecl{binarysymbol}[args=2] \symref{binarysymbol}{this} is a symbol taking two arguments. } So far we have gained exactly \ldots nothing by adding the arity information: we cannot do anything with the arguments in the text. We will now see what we can gain with more machinery. \begin{function}{\notation} We probably want to supply a notation as well, in which case we can finally actually use the semantic macro in math mode. We can do so using the \stexcode"\notation" command, like this: \stexexample{% \notation{binarysymbol}{\text{First: }#1\text{; Second: }#2} $\binarysymbol{a}{b}$ } \end{function} \begin{mmtbox} Applications of semantic macros, such as \stexcode"\binarysymbol{a}{b}" are translated to \mmt/\omdoc as |OMA|-terms with head ||. Semantic macros with no arguments correspond to |OMS| directly. \end{mmtbox} \begin{function}{\comp} For many semantic services e.g. semantic highlighting or \defemph{wikification} (linking user-visible notation components to the definition of the respective symbol they come from), we need to specify the notation components. Unfortunately, there is currently no way the \sTeX engine can infer this by itself, so we have to specify it manually in the notation specification. We can do so with the \stexcode"\comp" command. \end{function} We can introduce a new notation |highlight| for \stexcode"\binarysymbol" that fixes this flaw, which we can subsequently use with \stexcode"\binarysymbol[highlight]": \stexexample{% \notation{binarysymbol}[highlight] {\comp{\text{First: }}#1\comp{\text{; Second: }}#2} $\binarysymbol[highlight]{a}{b}$ } \begin{dangerbox} Ideally, \stexcode"\comp" would not be necessary: Everything in a notation that is \emph{not} an argument should be a notation component. Unfortunately, it is computationally expensive to determine where an argument begins and ends, and the argument markers |#n| may themselves be nested in other macro applications or \TeX\xspace groups, making it ultimately almost impossible to determine them automatically while also remaining compatible with arbitrary highlighting customizations (such as tooltips, hyperlinks, colors) that users might employ, and that are ultimately invoked by \stexcode"\comp". \end{dangerbox} \begin{dangerbox} Note that it is required that \begin{enumerate} \item the argument markers |#n| never occur inside a \stexcode"\comp", and \item no semantic arguments may ever occur inside a notation. \end{enumerate} Both criteria are not just required for technical reasons, but conceptionally meaningful: The underlying principle is that the arguments to a semantic macro represent \emph{arguments to the mathematical operation} represented by a symbol. For example, a semantic macro \stexcode"\addition{a}{b}" taking two arguments would represent \emph{the actual addition of (mathematical objects) $a$ and $b$}. It should therefore be impossible for $a$ or $b$ to be part of a notation component of \stexcode"\addition". Similarly, a semantic macro can not conceptually be part of the notation of \stexcode"\addition", since a semantic macro represents a \emph{distinct mathematical concept} with \emph{its own semantics}, whereas notations are syntactic representations of the very symbol to which the notation belongs. If you want an argument to a semantic macro to be a purely syntactic parameter, then you are likely somewhat confused with respect to the distinction between the precise \emph{syntax} and \emph{semantics} of the symbol you are trying to declare (which happens quite often even to experienced \sTeX users), and might want to give those another thought - quite likely, the macro you aim to implement does not actually represent a semantically meaningful mathematical concept, and you will want to use \stexcode"\def" and similar native \LaTeX\xspace macro definitions rather than semantic macros. \end{dangerbox} \begin{function}{\symdef} In the vast majority of cases where a symbol declaration should come with a semantic macro, we will want to supply a notation immediately. For that reason, the \stexcode"\symdef" command combines the functionality of both \stexcode"\symdecl" and \stexcode"\notation" with the optional arguments of both: \end{function} \stexexample{% \symdef{newbinarysymbol}[hl,args=2] {\comp{\text{1.: }}#1\comp{\text{; 2.: }}#2} $\newbinarysymbol{a}{b}$ } We just declared a new symbol |newbinarysymbol| with |args=2| and immediately provided it with a notation with identifier |hl|. Since |hl| is the \emph{first} (and so far, only) notation supplied for |newbinarysymbol|, using \stexcode"\newbinarysymbol" without optional argument defaults to this notation.\bigskip But one man's meat is another man's poison: it is very subjective what the ``default notation'' of an operator should be. Different communities have different practices. For instance, the complex unit is written as $i$ in Mathematics and as $j$ in electrical engineering. So to allow modular specification and facilitate re-use of document fragments \sTeX allows to re-set notation defaults. \begin{function}{\setnotation} The first notation provided will stay the default notation unless explicitly changed -- this is enabled by the \stexcode"\setnotation" command: \stexcode"\setnotation{symbolname}{notation-id}" sets the default notation of \stexcode"\symbolname" to |notation-id|, i.e. henceforth, \stexcode"\symbolname" behaves like \stexcode"\symbolname[notation-id]" from now on. \end{function} Often, a default notation is set right after the corresponding notation is introduced -- the starred version \stexcode"\notation*" for that reason introduces a new notation and immediately sets it to be the new default notation. So expressed differently, the \emph{first} \stexcode"\notation" for a symbol behaves exactly like \stexcode"\notation*", and \stexcode"\notation*{foo}[bar]{...}" behaves exactly like \stexcode"\notation{foo}[bar]{...}\setnotation{foo}{bar}". \begin{function}{\textsymdecl} In the less mathematical settings where we want a symbol and semantic macro for some concept with a notation \emph{beyond} its mere name, but which should also be available in \TeX's text mode, the command \stexcode"\textsymdecl" is useful. For example, we can declare a symbol \stexcode"openmath" with the notation \stexcode"\textsc{OpenMath}" using \textsymdecl{openmath}[name=OpenMath]{\textsc{OpenMath}} \stexcode"\textsymdecl{openmath}[name=OpenMath]{\textsc{OpenMath}}". The \stexcode"\openmath" yields \openmath both in text and math mode. \end{function} \begin{sfragment}{Operator Notations} Once we have a semantic macro with arguments, such as \stexcode"\newbinarysymbol", the semantic macro represents the \emph{application} of the symbol to a list of arguments. What if we want to refer to the operator \emph{itself}, though? We can do so by supplying the \stexcode"\notation" (or \stexcode"\symdef") with an \emph{operator notation}, indicated with the optional argument |op=|. We can then invoke the operator notation using \stexcode"\symbolname![notation-identifier]". Since operator notations never take arguments, we do not need to use \stexcode"\comp" in it, the whole notation is wrapped in a \stexcode"\comp" automatically: \stexexample{% \notation{newbinarysymbol}[ab, op={\text{a:}\cdot\text{; b:}\cdot}] {\comp{\text{a:}}#1\comp{\text{; b:}}#2} \symname{newbinarysymbol} is also occasionally written $\newbinarysymbol![ab]$ } \begin{mmtbox} \stexcode"\symbolname!" is translated to \omdoc/\mmt as || directly. \end{mmtbox} \end{sfragment} \end{sfragment} \begin{sfragment}{Argument Modes} The notations so far used \emph{simple} arguments which we call \emph{mode}-|i| arguments. Declaring a new symbol with \stexcode"\symdecl{foo}[args=3]" is equivalent to writing \stexcode"\symdecl{foo}[args=iii]", indicating that the semantic macro takes three mode-|i| arguments. However, there are three more argument modes which we will investigate now, namely mode-|b|, mode-|a| and mode-|B| arguments. \begin{sfragment}{Mode-\texttt b Arguments} A mode-|b| argument represents a \emph{variable} that is \emph{bound} by the symbol in its application, making the symbol a \emph{binding operator}. Typical examples of binding operators are e.g. sums $\sum$, products $\prod$, integrals $\int$, quantifiers like $\forall$ and $\exists$, that $\lambda$-operator, etc. \begin{mmtbox} Mode-|b| arguments behave exactly like mode-|i| arguments within \TeX, but applications of binding operators, i.e. symbols with mode-|b| arguments, are translated to |OMBIND|-terms in \omdoc/\mmt, rather than |OMA|. \end{mmtbox} For example, we can implement a summation operator binding an index variable and taking lower and upper index bounds and the expression to sum over like this: \stexexample{% \symdef{summation}[args=biii] {\mathop{\comp{\sum}}_{#1\comp{=}#2}^{#3}#4} $\summation{\svar{x}}{1}{\svar{n}}{\svar{x}}^2$ } where the variable $\svar{x}$ is now \emph{bound} by the \stexcode"\summation"-symbol in the expression. \end{sfragment} \begin{sfragment}{Mode-\texttt a Arguments} Mode-|a| arguments represent a \emph{flexary argument sequence}, i.e. a sequence of arguments of arbitrary length. Formally, operators that take arbitrarily many arguments don't ``exist'', but in informal mathematics, they are ubiquitous. Mode-|a| arguments allow us to write e.g. \stexcode"\addition{a,b,c,d,e}" rather than having to write something like \stexcode"\addition{a}{\addition{b}{\addition{c}{\addition{d}{e}}}}"! \stexcode"\notation" (and consequently \stexcode"\symdef", too) take one additional argument for each mode-|a| argument that indicates how to ``accumulate'' a comma-separated sequence of arguments. This is best demonstrated on an example. Let's say we want an operator representing quantification over an ascending chain of elements in some set, i.e. \stexcode"\ascendingchain{S}{a,b,c,d,e}{t}" should yield $\forall a{<_S}b{<_S}c{<_S}d{<_S}e.\,t$. The ``base''-notation for this operator is simply\\ \stexcode"{\comp{\forall} #2\comp{.\,}#3}", where |#2| represents the full notation fragment \emph{accumulated} from |{a,b,c,d,e}|. The \emph{additional} argument to \stexcode"\notation" (or \stexcode"\symdef") takes the same arguments as the base notation and two \emph{additional} arguments |##1| and |##2| representing successive pairs in the mode-|a| argument, and accumulates them into |#2|, i.e. to produce $a<_Sb<_Sc<_Sd<_Se$, we do \stexcode"{##1 \comp{<}_{#1} ##2}": \stexexample{% \symdef{ascendingchain}[args=iai] {\comp{\forall} #2\comp{.\,}#3} {##1 \comp{<}_{#1} ##2} Tadaa: $\ascendingchain{S}{a,b,c,d,e}{t}$ } If this seems overkill, keep in mind that you will rarely need the single-hash arguments |#1|,|#2| etc. in the |a|-notation-argument. For a much more representative and simpler example, we can introduce flexary addition via: \stexexample{% \symdef{addition}[args=a]{#1}{##1 \comp{+} ##2} Tadaa: $\addition{a,b,c,d,e}$ } \begin{sfragment}{The \texttt{assoc}-key} We mentioned earlier that ``formally'', flexary arguments don't really ``exist''. Indeed, formally, addition is usually defined as a binary operation, quantifiers bind a single variable etc. Consequently, we can tell \sTeX (or, rather, \mmt/\omdoc) how to ``resolve'' flexary arguments by providing \stexcode"\symdecl" or \stexcode"\symdef" with an optional |assoc|-argument, as in \stexcode"\symdecl{addition}[args=a,assoc=bin]". The possible values for the |assoc|-key are: \begin{itemize} \item[|bin|:] A binary, associative argument, e.g. as in \stexcode"\addition" \item[|binl|:] A binary, left-associative argument, e.g. $a^{\scriptstyle b^{\scriptstyle c^d}}$, which stands for $((a^b)^c)^d$ \item[|binr|:] A binary, right-associative argument, e.g. as in $A\to B\to C\to D$, which stands for $A \to (B \to (C \to D))$ \item[|pre|:] Successively prefixed, e.g. as in $\forall x,y,z.\,P$, which stands for $\forall x.\, \forall y.\, \forall z.\,P$ \item[|conj|:] Conjunctive, e.g. as in $a=b=c=d$ or $a,b,c,d\in A$, which stand for $a=d\wedge b=d\wedge c=d$ and $a\in A\wedge b\in A \wedge c\in A\wedge d\in A$, respectively \item[|pwconj|:] Pairwise conjunctive, e.g. as in $a\neq b\neq c\neq d$, which stands for $a\neq b\wedge a\neq c\wedge a\neq d\wedge b\neq c\wedge b\neq d\wedge c\neq d$ \end{itemize} As before, at the PDF level, this annotation is invisible (and without effect), but at the level of the generated OMDoc/MMT this leads to more semantical expressions. \end{sfragment} \end{sfragment} \begin{sfragment}{Mode-\texttt B Arguments} Finally, mode-|B| arguments simply combine the functionality of both |a| and |b| - i.e. they represent an arbitrarily long sequence of variables to be bound, e.g. for implementing quantifiers: \stexexample{% \symdef{quantforall}[args=Bi] {\comp{\forall}#1\comp{.}#2} {##1\comp,##2} $\quantforall{\svar{x},\svar{y},\svar{z}}{P}$ } \end{sfragment} \end{sfragment} \begin{sfragment}{Type and Definiens Components} \stexcode"\symdecl" and \stexcode"\symdef" take two more optional arguments. \TeX\xspace largely ignores them (except for special situations we will talk about later), but \mmt can pick up on them for additional services. These are the |type| and |def| keys, which expect expressions in math-mode (ideally using semantic macros, of course!) \begin{mmtbox} The |type| and |def| keys correspond to the |type| and |definiens| components of \omdoc/\mmt constants. Correspondingly, the name ``type'' should be taken with a grain of salt, since \omdoc/\mmt -- being foundation-independent -- does not a priori implement a fixed typing system. \end{mmtbox} \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}}} The |type|-key allows us to provide additional information (given the necessary \sTeX symbols), e.g. for addition on natural numbers: \stexexample{% \symdef{Nat}[type=\set]{\comp{\mathbb N}} \symdef{addition}[ type=\funtype{\Nat,\Nat}{\Nat}, op=+, args=a ]{#1}{##1 \comp+ ##2} \symname{addition} is an operation $\funtype{\Nat,\Nat}{\Nat}$ } The |def|-key allows for declaring symbols as abbreviations: \stexexample{% \symdef{successor}[ type=\funtype{\Nat}{\Nat}, def=\fun{\svar{x}}{\addition{\svar{x},1}}, op=\mathtt{succ}, args=1 ]{\comp{\mathtt{succ(}#1\comp{)}}} The \symname{successor} operation $\funtype{\Nat}{\Nat}$ is defined as $\fun{\svar{x}}{\addition{\svar{x},1}}$ } \end{sfragment} \begin{sfragment}{Precedences and Automated Bracketing} Having done \stexcode"\addition", the obvious next thing to implement is \stexcode"\multiplication". This is straight-forward in theory: \stexexample{% \symdef{multiplication}[ type=\funtype{\Nat,\Nat}{\Nat}, op=\cdot, args=a ]{#1}{##1 \comp\cdot ##2} \symname{multiplication} is an operation $\funtype{\Nat,\Nat}{\Nat}$ } However, if we \emph{combine} \stexcode"\addition" and \stexcode"\multiplication", we notice a problem: \stexexample{% $\addition{a,\multiplication{b,\addition{c,\multiplication{d,e}}}}$ } We all know that $\multiplication!$ binds stronger than $\addition!$, so the output $\addition{a,\multiplication{b,\addition{c,\multiplication{d,e}}}}$ does not actually reflect the term we wrote. We can of course insert parentheses manually \stexexample{% $\addition{a,\multiplication{b,(\addition{c,\multiplication{d,e}})}}$ } but we can also do better by supplying \emph{precedences} and have \sTeX insert parentheses automatically. For that purpose, \stexcode"\notation" (and hence \stexcode"\symdef") take an optional argument |prec=;x...x|. We will investigate the precise meaning of || and the ||s shortly -- in the vast majority of cases, it is perfectly sufficient to think of |prec=| taking a single number and having that be \emph{the} precedence of the notation, where lower precedences (somewhat counterintuitively) bind stronger than higher precedences. So fixing our notations for \stexcode"\addition" and \stexcode"\multiplication", we get: \stexexample{% \notation{multiplication}[ op=\cdot, prec=50 ]{#1}{##1 \comp\cdot ##2} \notation{addition}[ op=+, prec=100 ]{#1}{##1 \comp+ ##2} $\addition{a,\multiplication{b,\addition{c,\multiplication{d,e}}}}$ } Note that the precise numbers used for precedences are pretty arbitrary - what matters is which precedences are higher than which other precedences when used in conjunction. \begin{variable}{\infprec,\neginfprec} It is occasionally useful to have ``infinitely'' high or low precedences to enforce or forbid automated bracketing entirely -- for those purposes, \stexcode"\infprec" and \stexcode"\neginfprec" exist (which are implemented as the maximal and minimal integer values accordingly). \end{variable} \begin{dangerbox} More precisely, each notation takes \begin{enumerate} \item One \emph{operator precedence} and \item one \emph{argument precedence} for each argument. \end{enumerate} By default, all precedences are $0$, unless the symbol takes no argument, in which case the operator precedence is \stexcode"\neginfprec" (negative infinity). If we only provide a single number, this is taken as both the operator precedence and all argument precedences. \sTeX decides whether to insert parentheses by comparing operator precedences to a \emph{downward precedence} $p_d$ with initial value \stexcode"\infprec". When encountering a semantic macro, \sTeX takes the operator precedence $p_{op}$ of the notation used and checks whether $p_{op}>p_d$. If so, \sTeX insert parentheses. When \sTeX steps into an argument of a semantic macro, it sets $p_d$ to the respective argument precedence of the notation used. In the example above: \begin{enumerate} \item \sTeX starts out with $p_d=$\stexcode"\infprec". \item \sTeX encounters \stexcode"\addition" with $p_{op}=100$. Since $100\not>$\stexcode"\infprec", it inserts no parentheses. \item Next, \sTeX encounters the two arguments for \stexcode"\addition". Both have no specifically provided argument precedence, so \sTeX uses $p_d=p_{op}=100$ for both and recurses. \item Next, \sTeX encounters \stexcode"\multiplication{b,...}", whose notation has $p_{op}=50$. \item We compare to the current downward precedence $p_d$ set by \stexcode"\addition", arriving at $p_{op}=50\not>100=p_d$, so \sTeX again inserts no parentheses. \item Since the notation of \stexcode"\multiplication" has no explicitly set argument precedences, \sTeX uses the operator precedence for all arguments of \stexcode"\multiplication", hence sets $p_d=p_{op}=50$ and recurses. \item Next, \sTeX encounters the inner \stexcode"\addition{c,...}" whose notation has $p_{op}=100$. \item We compare to the current downward precedence $p_d$ set by \stexcode"\multiplication", arriving at $p_{op}=100>50=p_d$ -- which finally prompts \sTeX to insert parentheses, and we proceed as before. \end{enumerate} \end{dangerbox} \end{sfragment} \begin{sfragment}{Variables} All symbol and notation declarations require a module with which they are associated, hence the commands \stexcode"\symdecl", \stexcode"\notation", \stexcode"\symdef" etc. are disabled outside of |smodule|-environments. Variables are different -- variables are allowed everywhere, are not exported when the current module (if one exists) is imported (via \stexcode"\importmodule" or \stexcode"\usemodule") and (also unlike symbol declarations) ``disappear'' at the end of the current \TeX\xspace group. \begin{function}{\svar} So far, we have always used variables using \stexcode"\svar{n}", which marks-up $n$ as a variable with name |n|. More generally, \stexcode"\svar[foo]{}" marks-up the arbitrary || as representing a variable with name |foo|. \end{function} Of course, this makes it difficult to reuse variables, or introduce ``functional'' variables with arities $>0$, or provide them with a type or definiens. \begin{function}{\vardef} For that, we can use the \stexcode"\vardef" command. Its syntax is largely the same as that of \stexcode"\symdef", but unlike symbols, variables have only one notation (\textcolor{red}{TODO: so far?}), hence there is only \stexcode"\vardef" and no \stexcode"\vardecl". \end{function} \stexexample{% \vardef{varf}[ name=f, type=\funtype{\Nat}{\Nat}, op=f, args=1, prec=0;\neginfprec ]{\comp{f}#1} \vardef{varn}[name=n,type=\Nat]{\comp{n}} \vardef{varx}[name=x,type=\Nat]{\comp{x}} Given a function $\varf!:\funtype{\Nat}{\Nat}$, by $\addition{\varf!,\varn}$ we mean the function $\fun{\varx}{\varf{\addition{\varx,\varn}}}$ } (of course, ``lifting'' addition in the way described in the previous example is an operation that deserves its own symbol rather than abusing \stexcode"\addition", but... well.) \textcolor{red}{TODO: bind=forall/exists} \end{sfragment} \begin{sfragment}{Variable Sequences} Variable \emph{sequences} occur quite frequently in informal mathematics, hence they deserve special support. Variable sequences behave like variables in that they disappear at the end of the current \TeX\xspace group and are not exported from modules, but their declaration is quite different. \begin{function}{\varseq} A variable sequence is introduced via the command \stexcode"\varseq", which takes the usual optional arguments |name| and |type|. It then takes a starting index, an end index and a \emph{notation} for the individual elements of the sequence parametric in an index. Note that both the starting as well as the ending index may be variables. \end{function} This is best shown by example: \stexexample{% \vardef{varn}[name=n,type=\Nat]{\comp{n}} \varseq{seqa}[name=a,type=\Nat]{1}{\varn}{\comp{a}_{#1}} The $i$th index of $\seqa!$ is $\seqa{i}$. } Note that the syntax |\seqa!| now automatically generates a presentation based on the starting and ending index. \textcolor{red}{TODO: more notations for invoking sequences}. \vardef{varn}[name=n,type=\Nat]{\comp{n}} \varseq{seqa}[name=a]{1}{\varn}{\comp{a}_{#1}} Notably, variable sequences are nicely compatible with |a|-type arguments, so we can do the following: \stexexample{% $\addition{\seqa}$ } Sequences can be \emph{multidimensional} using the |args|-key, in which case the notation's arity increases and starting and ending indices have to be provided as a comma-separated list: \stexexample{% \vardef{varm}[name=m,type=\Nat]{\comp{m}} \varseq{seqa}[ name=a, args=2, type=\Nat, ]{1,1}{\varn,\varm}{\comp{a}_{#1}^{#2}} $\seqa!$ and $\addition{\seqa}$ } \vardef{varm}[name=m,type=\Nat]{\comp{m}} We can also explicitly provide a ``middle'' segment to be used, like such: \stexexample{% \varseq{seqa}[ name=a, type=\Nat, args=2, mid={\comp{a}_{\varn}^1,\comp{a}_1^2,\ellipses,\comp{a}_{1}^{\varm}} ]{1,1}{\varn,\varm}{\comp{a}_{#1}^{#2}} $\seqa!$ and $\addition{\seqa}$ } \end{sfragment} \end{smodule} %%% Local Variables: %%% mode: latex %%% TeX-master: "../stex-manual" %%% End: % LocalWords: binarysymbol newbinarysymbol hl,args a,b,c,d,e ascendingchain assoc binl % LocalWords: a,assoc binr x,y,z conj a,b,c,d pwconj funtype succ prec opprec argprec1 % LocalWords: argprec texcode varf varn n,type varx x,type varseq seqa a,type th m,type