summaryrefslogtreecommitdiff
path: root/macros/latex209/contrib/zed/zmacros.tex
blob: 5e6f0b0d24b76a7363fa87d38bbaca75ec8309ac (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
% ZMACROS.TEX		Mike Spivey	July 1987
\documentstyle[palatino,11pt,zed]{article}
\begin{document}
\title{Printing Z with \LaTeX}
\author{Mike Spivey}
\date{15th September 1987}
\maketitle

\section{Introduction}

This note describes a small package of \LaTeX\ macros for printing
Z specifications.
I put these together specifically for printing my book on Z semantics,
so the package only provides features I needed for that, and your
favourite Z constructs may be missing.
On the other hand, I've put quite a lot of work into getting
the constructs which {\em are\/} there to look right, at
least to my eyes. If the package doesn't do what you want,
at least it gives you something to start from.
The package does several related things for you:
\begin{enumerate}
\item   It loads the two fonts of extra symbols from the American
        Mathematical Society and defines mnemonics for the Z symbols
        they contain.
\item   It defines macros to fudge some Z symbols (e.g. $\pinj$) which
        don't appear in any of our fonts.
\item   It fixes the way \TeX\ sets letters in mathematical formulas so
        that multi-character identifiers look better.
\item   It provides ways to set the various brands of `boxed mathematics'
        which appear in Z specifications.
\end{enumerate}

\section{Loading the macros}

The package is kept in a file {\tt zed.sty}, so to load it at
the start of a \LaTeX\ run, you just begin with
\begin{quote}
\begin{verbatim}
\documentstyle[11pt,zed]{article}
\end{verbatim}
\end{quote}
or something like it.
At PRG, the package only works with the eleven-point base size at
present: the extra-symbols fonts it loads are only available at
this size on the LBP--10.

\section{The care and feeding of schemas}

To print the schema
\begin{schema}{PhoneDB}
    known: \power NAME \\
    phone: NAME \pfun PHONE
\where
    known = \dom phone
\end{schema}
you just say
\begin{quote}
\begin{verbatim}
\begin{schema}{PhoneDB}
    known: \power NAME \\
    phone: NAME \pfun PHONE
\where
    known = \dom phone
\end{schema}
\end{verbatim}
\end{quote}
What could be simpler?
If you want a schema with no name, just a horizontal rule at the top,
use the \verb|schema*| environment instead.
In fact, here is an example:
% \begin{schema*}
%	known: \power NAME \\
%	phone: NAME \pfun PHONE
% \where
%	known = \dom phone
% \end{schema*}
If you like the name set flush left, you can use the \verb|\leftschemas|
declaration to get the following effect:
\begin{leftschemas}
\begin{schema}{PhoneDB}
    known: \power NAME \\
    phone: NAME \pfun PHONE
\where
    known = \dom phone
\end{schema}
\end{leftschemas}
As well as these, there's \verb|axdef|
for axiomatic definitions: to print
\begin{axdef}
    policy: \power_1 RESOURCE \fun RESOURCE
\where
    \forall S: \power_1 RESOURCE \spot \\
\t1         policy(S) \in S,
\end{axdef}
you say
\begin{quote}
\begin{verbatim}
\begin{axdef}
    policy: \power_1 RESOURCE \fun RESOURCE
\where
    \forall S: \power_1 RESOURCE \spot \\
\t1         policy(S) \in S,
\end{axdef}
\end{verbatim}
\end{quote}
The strange hint \verb|\t1| in this example makes the corresponding
line in the output have one helping of indentation.
As things get more nested, you can say \verb|\t2|, \verb|\t3|, and so on.
But if you should ever get beyond \verb|t9|, you'll need to use braces
around the argument: \verb|\t{10}|, and you'd better look for some way
to simplify your specification!
The syntax of these little tab marks is a bit strange, I'm afraid,
but I find them more convenient than other possibilities. They're short,
and they don't get longer as the tabbing gets deeper, within reason,
so they can be tucked in neatly on the left, well away from the
maths.
The size of `helping' you get with \verb|\t| is a parameter
\verb|\zedindent|, and the default is 2em.

Two other things to notice here are the little space between the
$\forall$ and the following $S$, and the use of \verb|\spot| for
the bullet $\spot$.
These macros produce symbols of the right type for \TeX's spacing
rules to insert spaces automatically.

For generic definitions, there's the \verb|gendef| environment:
you can get a neat double-topped box like
\begin{gendef}{I,X,Y}
    map: (X \pfun Y) \fun (I \pfun X) \fun (I \pfun Y)
\where
    map\,f = \lambda s: I \pfun X \mid
        \ran s \subseteq \dom f \spot f \circ s
\end{gendef}
by typing
\begin{quote}
\begin{verbatim}
\begin{gendef}{I,X,Y}
    map: (X \pfun Y) \fun (I \pfun X) \fun (I \pfun Y)
\where
    map\,f = \lambda s: I \pfun X \mid
        \ran s \subseteq \dom f \spot f \circ s
\end{gendef}
\end{verbatim}
\end{quote}
You should take note of the thin space I've inserted between $map$ and $f$
in this example: if this is omitted, the input \verb|map f| gives
$map f$, because \TeX\ ignores spaces in math mode.
There's also a \verb|gendef*| environment for generic definitions with no
parameters.

If a schema or other box contains more than one predicate below the
line, it often looks better to add a tiny vertical space between
them, as in this example:
\begin{schema}{AddPhone}
    \Delta PhoneDB \\
    name?: NAME \\
    number?: PHONE
\where
    name? \notin known
\also
    phone' = phone \oplus \{name? \mapsto number?\}
\end{schema}
This is done with the command \verb|\also|, which behaves syntactically
like \verb|\where|:
\begin{quote}
\begin{verbatim}
\begin{schema}{AddPhone}
    \Delta PhoneDB \\
    name?: NAME \\
    number?: PHONE
\where
    name? \notin known
\also
    phone' = phone \oplus \{name? \mapsto number?\}
\end{schema}
\end{verbatim}
\end{quote}
Note that \verb|\also| is provided {\em instead\/} of the
optional argument to \verb|\\|
which \LaTeX\ provides in other environments.

\section{Other mathematical displays}

The \verb|zed| environment can be used to set multi-line formulas without
an enclosing box: it is useful for given-set declarations, theorems, and the
miscellaneous bits of mathematics that don't come in a box:
\begin{zed}
    \forall n: \nat \spot \\
\t1         n+n \in even.
\end{zed}
is printed from the input
\pagebreak[3]
\begin{quote}
\begin{verbatim}
\begin{zed}
    \forall n: \nat \spot \\
\t1         n+n \in even.
\end{zed}
\end{verbatim}
\end{quote}
The formula \verb|\begin{zed} ... \end{zed}| may be abbreviated to
\verb|\[ ... \]|; the \verb|zed| environment is a generalization of the
\verb|displaymath| environment of \LaTeX, so this redefinition of
commands is fairly benign. Notice that the maths is set flush left on the
same indentation as schemas and their friends.
Here too you can use \verb|\also| for a little extra space
between lines.

For algebraic-style proofs, there is the \verb|argue| environment.
This is like the \verb|zed| environment, but the separation between
lines is increased a little, and page breaks may occur between lines.
The intended use is for arguments like this:
\begin{argue}
    rev(append(cons(x,s),t)) \\
\t1     = rev(cons(x,append(s,t))) \\
\t1     = append(rev(append(s,t)),cons(x,nil)) \\
\t1     = append(append(rev(t),rev(s)),cons(x,nil))
                \quad \hbox{by hypothesis} \\
\t1     = append(rev(t),append(rev(s),cons(x,nil))) \\
\t1     = append(rev(t),rev(cons(x,s))).
\end{argue}
Here, again, is the input:
\begin{quote}
\begin{verbatim}
\begin{argue}
    rev(append(cons(x,s),t)) \\
\t1     = rev(cons(x,append(s,t))) \\
\t1     = append(rev(append(s,t)),cons(x,nil)) \\
\t1     = append(append(rev(t),rev(s)),cons(x,nil))
                \quad \hbox{by hypothesis} \\
\t1     = append(rev(t),append(rev(s),cons(x,nil))) \\
\t1     = append(rev(t),rev(cons(x,s))).
\end{argue}
\end{verbatim}
\end{quote}
When the left-hand side is long, I find this style better than the
\LaTeX\ \verb|eqnarray| style, which wastes a lot of space.

Another brand of box is the inference rule; the rule
\begin{infrule}
    \Gamma \shows P
\derive[x \notin freevars(\Gamma)]
    \Gamma \shows \forall x \spot P
\end{infrule}
comes from the input
\begin{quote}
\begin{verbatim}
\begin{infrule}
    \Gamma \shows P
\derive[x \notin freevars(\Gamma)]
    \Gamma \shows \forall x \spot P
\end{infrule}
\end{verbatim}
\end{quote}
Note the optional argument to \verb|\derive|: it is a side-condition of
the rule.

Finally, there's the \verb|syntax| environment, used for
making displays like this:
\begin{syntax}
    EXPR & ::= & IDENT      & identifier \\
         &  |  & EXPR\;EXPR & application \\
         &  |  & \lambda IDENT \spot EXPR
                            & lambda-abstraction.
\end{syntax}
from input like this:
\begin{quote}
\begin{verbatim}
\begin{syntax}
    EXPR & ::= & IDENT      & identifier \\
         &  |  & EXPR\;EXPR & application \\
         &  |  & \lambda IDENT \spot EXPR
                            & lambda-abstraction.
\end{syntax}
\end{verbatim}
\end{quote}
This kind of thing is useful when you're describing a language,
and it can also be used for data-type definitions.
I've even---time for a confession---used it once for a fragment
of VDM\@.
The final column is optional:
just omit the third \verb|&| if you don't want it.

\section{Inside the boxes}

\makeatletter
\def\nota{\interzedlinepenalty=\interdisplaylinepenalty
        \@zed\halign\bgroup\strut\hbox to3em{$##$\hfil}\tabskip=0pt&##\hfil\cr}
\let\endnota=\endzed
\makeatother

Now for the details of what you can put inside the boxes.
The first thing to notice is that multi-letter identifiers look
better than they do with vanilla \LaTeX: instead of
$\mit specifications$, you get $specifications$.
The letters haven't been spread apart, and the ligature $fi$ has been
used.

Almost all of the mathematical symbols of \LaTeX\ can be used, plus
a few extra ones listed below.
The mnemonics I've chosen may seem a little mad, but that's life.
The \LaTeX\ symbols you can't use are the ones whose
names have been redefined:
mostly these are the same symbol, but with the spacing fixed for
use in Z specifications.
First, there are some new arrows, and some new names for old ones:
\begin{nota}
    \rel & \verb|\rel| \\
    \fun & \verb|\fun| \\
    \inj & \verb|\inj| \\
    \surj & \verb|\surj| \\
    \bij & \verb|\bij| \\
    \implies & \verb|\implies| \\
    \iff & \verb|\iff|
\end{nota}
There are also `accents' \verb|\p| and \verb|\f| which put one and two
crossings repectively over the following arrow.
So \verb|\p\fun| gives $\p\fun$ and (if you insist)
\verb|\f\bij| gives $\f\bij$.
There are also some new binary operations:
\begin{nota}
    \comp & \verb|\comp| \\
    \dres & \verb|\dres| \\
    \rres & \verb|\rres| \\
    \ndres & \verb|\ndres| \\
    \nrres & \verb|\nrres| \\
    \cross & \verb|\cross| \\
    \filter & \verb|\filter| \\
    \upto & \verb|\upto| \\
    \div & \verb|\div| \\
    \mod & \verb|\mod| \\
    \cat & \verb|\cat|
\end{nota}
and some new operators:
\begin{nota}
    \dom & \verb|\dom| \\
    \ran & \verb|\ran| \\
    \pre & \verb|\pre| \\
    \id & \verb|\id| \\
    \seq & \verb|\seq| \\
    \bag & \verb|\bag| \\
    \forall & \verb|\forall| \\
    \exists & \verb|\exists| \\
    \lambda & \verb|\lambda| \\
    \mu & \verb|\mu| \\
    \power & \verb|\power| \\
    \finset & \verb|\finset| \\
    \dcat & \verb|\dcat|
\end{nota}
The unique quantifier $\exists_1$ can be typeset as \verb|\exists_1|.
There are a couple of new ordinary symbols:
\begin{nota}
    \empty & \verb|\empty| \\
    \nat & \verb|\nat| \\
    \num & \verb|\num|
\end{nota}
as well as a few fancy brackets:
\begin{nota}
    \limg\;\rimg & \verb|\limg \rimg| \\
    \lbag\;\rbag & \verb|\lbag \rbag| \\
    \ldata\;\rdata & \verb|\ldata \rdata| \\
    \lblot\;\rblot & \verb|\lblot \rblot|
\end{nota}
Finally, the following bits and pieces come with the right spacing for Z:
\begin{nota}
    \land & \verb|\land| \\
    \lor & \verb|\lor| \\
    \lnot & \verb|\lnot| \\
    \widehat= & \verb|\defs| \\
    \hide & \verb|\hide| \\
    \project & \verb|\project| \\
    \semi & \verb|\semi| \\
    \vdash & \verb|\shows| \\
    \spot & \verb|\spot|
\end{nota}
Some of these are duplicates of binary operators listed above, but with
names more appropriate to their use in schema-expressions; there is
also a little more spacing in these variants.
And that's about it.

\section{Style parameters}

\begin{description}
\item[\tt\string\zedindent] The indentation for mathematical text.
	By default, this is the same as \verb|\leftmargini|, the indentation
	used for list environments.
\item[\tt\string\zedleftsep] The space between the vertical line on the left
	of schemas, etc., and the maths inside. The default is 1em.
\item[\tt\string\zedtab] The unit of indentation used by \verb|\t|. The default
	is 2em.
\item[\tt\string\zedbar] The length of the horizontal bar in the middle of a
	schema. The default is 6em.
\item[\tt\string\leftschemas] A declaration which makes schema names be
	set flush left. Use it in the document preamble.
\end{description}

\end{document}