summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/stex/doc/packages/stex-symbols.tex
blob: e7bafeda6b60f6e5b60c5393a78749f617a847a5 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
\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
  |<module-URI>?<constant-name>|.
\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 |<OMS name="...?binarysymbol"/>|.

  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 |<OMS name="...?symbolname"/>|
    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=<opprec>;<argprec1>x...x<argprec n>|.

We will investigate the precise meaning of |<opprec>| and the |<argprec>|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]{<texcode>}" marks-up
    the arbitrary |<texcode>| 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