16 pt

Printing Z and Object-Z L^{A}TEX documents

Paul King

Department of Computer Science University of Queensland Australia, 4072 king@batserver.cs.uq.oz.au

May 29, 1990

1 Introduction

This note describes a package of L^{A}TEX macros for printing Z and Object-Z specifications. The macros and this note are based originally on Mike Spivey’s zed.sty macros and documentation. The package does several related things for you:

• It loads extra fonts and defines mnemonics for the Z symbols they contain.

• It defines macros for some Z symbols (e.g. ↣) which don’t appear in any of our fonts.

• It fixes the way TEX sets letters in mathematical formulas so that multi-character identifiers look better.

• It provides various brands of ‘boxed mathematics’ which appear in Z and Object-Z specifications.

The package is kept in a file oz.sty in the directory /opt/local/lib/tex/lib/site-inputs. This directory should be mentioned in your TEXINPUTS shell variable. To use the macros you just begin your L^{A}TEX document with something like:

     \documentstyle[11pt,oz]{article}

2 Schema Boxes

The example below shows a schema on the left and what you need to say to get it on the right.

BirthdayBook known : ℙ NAME birthday : NAME \underrightarrow{}DATE

known = dom birthday

                                                      \begin{schema}{BirthdayBook}
                                                          known: \pset NAME \\
                                                          birthday: NAME \pfun DATE
                                                      \ST
                                                          known = \dom birthday
                                                      \end{schema}

The command \ST (read ‘Such That’) is the same as the previously used command \where which has been kept as an alias for upward compatibility. If you want a schema with no name, just a horizontal rule at the top, use the anonschema environment instead. You can set various parameters (see Section 7) to change the box style, for example:

BirthdayBook known : ℙ NAME birthday : NAME \underrightarrow{}DATE

known = dom birthday

In document preamble:

                                                      \leftschemas
                                                      \zedcornerheight=3ex
                                                      \zedlinethickness=0.9pt
                                                      \zedbar=10em\zedleftsep=3em

Schemas can also be defined using a horizontal notation, for example:

     BirthdayBook ˆ= [ . . .]  $BirthdayBook \sdef \lsch ... \rsch$

A generic schema is produced as follows.

Pool [RESOURCE] owner : RESOURCE \underrightarrow{}USER free : ℙ RESOURCE

(dom owner) ∪ free = RESOURCE (dom owner) ∩ free = ∅

                                                      \begin{genschema}{Pool}{RESOURCE}
                                                      owner : RESOURCE \pfun USER \\
                                                      free : \pset RESOURCE
                                                      \ST
                                                      (\dom owner) \uni free = RESOURCE \\
                                                      (\dom owner) \int free = \emptyset
                                                      \end{genschema}

3 Axiomatic definitions

A ‘liberal’ axiomatic definition is produced as follows.

limit : ℕ limit ≤ 65536

                                                      \begin{axdef}
                                                      limit : \nat
                                                      \ST
                                                      limit \leq 65536
                                                      \end{axdef}

A ‘generic’ axiomatic definition is produced as follows.

[X , Y ]

first : X × Y → X

∀ x : X ; y : Y • first(x, y) = x

                                                      \begin{gendef}{X,Y}
                                                      first : X \prod Y \tfun X
                                                      \ST
                                                      \all x : X; y : Y \dot first(x,y) = x
                                                      \end{gendef}

A ‘unique’ axiomatic definition is produced as follows.

π : ℝ π = 3.14159265 …

                                                      \begin{uniqdef}
                                                      \pi : \real
                                                      \ST
                                                      \pi = 3.14159265\ldots
                                                      \end{uniqdef}

4 Object-Z Class Boxes

Object-Z allows class types to be defined using a box very similar to the schema box previously described. It allows the previously described boxed environments (as well as nested sub-classes) to be placed within a class box. In addition, special names can be used for some of the boxed-environments when they appear within a class box. The following example illustrates a class definition.

Shape colour : Colour

perim : ℝ ; perim > 0

This class has 2 constants colour and perim.

x, y : ℝ

INIT x = y = 0

Translate ; Δ(x, y) ; dx?, dy? : ℝ ; x′ = x + dx? ; y′ = y + dy?

                                                      \begin{class}{Shape}
                                                      \also
                                                      colour : Colour \\
                                                      \begin{axdef}
                                                      perim : \real
                                                      \ST
                                                      perim > 0
                                                      \end{axdef} \\
                                                      \begin{classcom}
                                                      This class has 2 constants
                                                      $colour$ and $perim$.
                                                      \end{classcom} \\
                                                      \begin{state}
                                                      x, y : \real
                                                      \end{state} \\
                                                      \begin{init}
                                                      x = y = 0
                                                      \end{init} \\
                                                      \begin{op}{Translate}
                                                      \Delta (x,y) \\
                                                      dx?, dy? : \real
                                                      \ST
                                                      x' = x + dx? \\
                                                      y' = y + dy?
                                                      \end{op}
                                                      \end{class}

The classcom environment hasn’t been seen before. It creates a paragraph of text with the same margins as used for schemas and other Z environments. It uses a special font intended for use when placing comments inside classes. A similar environment, zpar, uses the same margins but with the normal roman font.

The \begin{init} command is an abbreviation for \begin{schema}{\Init}. Similarly \begin{state} is a

more meaningful synonym for \begin{anonschema}.

You will be given L^{A}TEX warning messages if you try to use a state environment outside of a class box or if you try to place an environment such as syntax inside a class. You can ask for additional help in these cases using the normal L^{A}TEX h or H help commands. If you proceed with L^{A}TEXing, the macros will attempt to do the best they can to do what you probably intend, even though you are violating the recommended nesting guidelines.

5 Controlling the Spacing within Equations and Boxes

Most of the special Z symbols are defined in a way that allows TEX to space them out correctly. Sometimes, however, you’ll need to give TEX a helping hand if you want it to get the spacing right. For example, to get map f you need to type map\,f. The \, gives you a thin space: if this is omitted, the input map f gives mapf , because TEX ignores spaces in math mode.

Sometimes it is useful to indent the left margin to emphasis the logical structure of the predicate. The command \t1 does this by making the corresponding line in the output have one helping of indentation. As things get more nested, you can say \t2, \t3, and so on. But if you should ever get beyond t9, you’ll need to use braces around the argument: \t{10}, and you’d better look for some way to simplify your specification! These little tab marks might look different to normal tabs but are never the less convenient. 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 \t is determined by the \zedtab parameter (see Section 7).

If you want a more powerful aligning mechanism than tabbing then you can use the margin stack as shown in the example below. The command \M sets the future left margin to the current horizontal position and pushes the old value onto a margin stack. The command \O resets the left margin to its previous value (which is popped off the stack).

Test

x, y : ℕ

x + 1/x = 0 ⇒ y + 1/y = 0

y = x

                                                      \begin{schema}{Test}
                                                      x, y : \nat
                                                      \ST
                                                      x + 1/x = 0 \imp \M y + 1/y = 0 \\
                                                      y = x \O \\
                                                      \end{schema}

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:

AddBirthday ΔBirthdayBook n? : NAME d? : DATE

n? ∉ known

birthday′ = birthday ∪ {n? ↦ d?}

                                                      \begin{schema}{AddBirthday}
                                                        \Delta BirthdayBook \\
                                                        n?: NAME \\
                                                        d?: DATE
                                                      \ST
                                                        n? \nem known
                                                      \also
                                                        birthday'=birthday \uni \{n? \map d?\}
                                                      \end{schema}

This is done with the command \also, which behaves syntactically like \ST. The command \also is provided instead of the optional argument to \\ which L^{A}TEX provides in other environments. If larger vertical spacing is required, the commands \Also and \ALSO may be used (giving 2 and 4 times as much space as \also respectively).

Normally, the contents of a schema box are kept on a single page. For large schemas it may be necessary to split the box across pages. You must specify which places are suitable for splitting using one of \zbreak, \Zbreak or \ZBREAK. If no split is performed at this point, a vertical space will be added as if the user had typed \also, \Also, or \ALSO respectively. You can also use the \znewpage command to force a page break within a box. (These breaking facilities will hopefully never be needed for schemas, but may become necessary for class specifications.)

6 Other Display Environments

The 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:

∀ n : ℕ • n + n ∈ even.

                                                      \begin{zed}
                                                          \all n: \nat \dot \\
                                                      \t1         n+n \mem even.
                                                      \end{zed}

The formula \begin{zed} ... \end{zed} may be abbreviated to \[ ... \]; the zed environment is a generalization of the displaymath environment of L^{A}TEX, 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 \also for a little extra space between lines.

For algebraic-style proofs, there is the argue environment. This is like the zed environment, but the separation between lines is increased a little, and page breaks may occur between lines. When the left-hand side is long this style wastes less space than the L^{A}TEX eqnarray style. The intended use is for arguments like this:

rev(append(cons(x, s), t)) = rev(cons(x, append(s, t))) = append(rev(append(s, t)), cons(x, nil)) = append(append(rev(t), rev(s)), cons(x, nil)) by hypothesis = append(rev(t), append(rev(s), cons(x, nil))) = append(rev(t), rev(cons(x, s))).

Here is the input:

\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}

The example below shows an inference rule (the optional argument to \derive gives a side-condition of the rule):

Γ ⊢ P

[ x ∉ freevars(Γ) ]

Γ ⊢ ∀ x • P

                                                \begin{infrule}
                                                    \Gamma \shows P
                                                \derive[x \nem freevars(\Gamma)]
                                                    \Gamma \shows \all x \dot P
                                                \end{infrule}

The syntax environment is used for making displays like this:

EXPR ::= IDENT  – identifier
| EXPR EXPR  – application
| λ IDENT • EXPR  – lambda-abstraction.

from input like this:

\begin{syntax}
  EXPR & \ddef & IDENT                   & identifier \\
       & \bbar & EXPR\;EXPR              & application \\
       & \bbar & \lambda IDENT \dot EXPR & lambda-abstraction.
\end{syntax}

This kind of thing is useful when you’re describing a language, and it can also be used for data-type definitions as shown below. The optional final column was omitted below by leaving out the third &.

TYPE ::= givenT ⟨⟨NAME⟩⟩
| powerT ⟨⟨TYPE⟩⟩
| tupleT ⟨⟨seq TYPE⟩⟩
| schemaT ⟨⟨IDENT \underrightarrow{}TYPE⟩⟩
| classT ⟨⟨IDENT \underrightarrow{}ClassAttr⟩⟩

                                                \begin{syntax}
                                                TYPE & \ddef & givenT  \lang NAME \rang \\
                                                & \bbar & powerT \lang TYPE \rang \\
                                                & \bbar & tupleT \lang \seq TYPE \rang \\
                                                & \bbar & schemaT \lang IDENT \ffun TYPE \rang \\
                                                & \bbar & classT \lang IDENT \ffun ClassAttr \rang
                                                \end{syntax}

This can be compared with the layout adopted by the UQ Z editor (version 1).

TYPE ::= givenT ⟨⟨NAME⟩⟩ | powerT ⟨⟨TYPE⟩⟩ | tupleT ⟨⟨seq TYPE⟩⟩ | schemaT ⟨⟨IDENT \underrightarrow{}TYPE⟩⟩ | classT ⟨⟨IDENT \underrightarrow{}ClassAttr⟩⟩

                                                \begin{zed}
                                                TYPE \ddef \M givenT  \lang NAME \rang \\
                                                \bbar powerT \lang TYPE \rang \\
                                                \bbar tupleT \lang \seq TYPE \rang \\
                                                \bbar schemaT \lang IDENT \ffun TYPE \rang \\
                                                \bbar classT \lang IDENT \ffun ClassAttr \rang \O
                                                \end{zed}

The sidebyside environment allows a display as shown in the first two columns below to be produced from the text of the third column. Note the use of the \comment command.

Schema [declarations] a < b  [pred-1] aaaaa < bbbbb [pred-2]  This is a paragraph which has the same margins as the stan- dard schemas do.

                                                      \begin{sidebyside}
                                                      \begin{schema}{Schema}
                                                      \comment*{declarations}
                                                      \ST
                                                      a < b \comment{pred-1} \\
                                                      aaaaa < bbbbb \comment{pred-2}
                                                      \end{schema}
                                                      \nextside
                                                      \begin{zpar}
                                                      This is a paragraph which has the same
                                                      margins as the standard schemas do.
                                                      \end{zpar}
                                                      \end{sidebyside}

In fact, this environment was used throughout this note to display the examples beside the required input text. Incidentally, the above example shows that sidebyside environments can be nested; so what the author of this note typed to get the above display was:

     \begin{sidebyside}
             \begin{sidebyside}
                     ...
             \nextside
                     ...
             \end{sidebyside}
     \nextside
             ...
     \end{sidebyside}

This resulted in the first two columns being equally spaced and together taking up as much space as the third column. You can have more than 2 columns without nesting by specifying an optional parameter to sidebyside. For example, the display below has three equally spaced columns obtained using \begin{sidebyside}[3].

BirthdayBook known : ℙ NAME birthday : NAME \underrightarrow{}DATE

known = dom birthday BirthdayBook known : ℙ NAME birthday : NAME \underrightarrow{}DATE

known = dom birthday Don’t get carried away with sidebyside like this example does.

7 Style Parameters

\zedindent The (horizontal) indentation for mathematical text. By default, this is the same as \leftmargini, the indentation used for list environments.

\zedleftsep The (horizontal) space between the vertical line on the left of schemas, etc., and the maths inside. The default is 1em.

\zedtab The unit of indentation used by \t. The default is 2em.

\zedbar The length of the horizontal bar in the middle of a schema. The default is 8em.

\leftschemas A declaration which makes schema names be set flush left. Use it in the document preamble.

\zedlinethickness The thickness of the lines that make up schema and class boxes. You can change the thickness with a command such as \zedlinethickness=0.1pt. This may be useful if you are creating overhead slides.

0.1pt

0.4pt (The default)

1pt

\baselinestretch The spacing for the text part of your document. It doesn’t change the spacing within Z environments. It’s default value is 1. A command such as \def\baselinestretch{2} will make your text double spaced, but not your Z environments.

\zedbaselinestretch The spacing for the Z environment part of your document. It’s default value is 1.

\zedsize The size of the material within the Z part of your document. It doesn’t affect the remainder of your document. For example, \zedsize{\large} will give you large Z symbols and equations but will not affect the size of the surrounding text.

\zedcornerheight The height of ‘corners’ that can be placed on the right hand side of the top and bottom lines of schema and class boxes. The default is 0em (i.e. no corners).

8 Symbols

Multi-letter identifiers have been changed to look better than they do with vanilla L^{A}TEX: instead of 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 L^{A}TEX can be used; some have been redefined—usually to fix the spacing so that it is suitable for Z specifications. The commands for obtaining additional symbols are listed below. Sometimes more than one command may produce a symbol you require. You should use the one that seems to be designed for the context you have in mind. This is because the spacing around (and size of) symbols has been chosen for their typical context.

Throughout the lifetime of these macros a number of alternate control sequences for any symbol may have existed. A list of aliases has been set up so that old commands may still be used. It is recommended however that you stick to the recommended command names for symbols as these names may be supported by other tools. Within the table below non-recommended aliases are surrounded by brackets, e.g., (\power).

8.1 Special Z Notation

Numbers

 ℕ  \nat
 ℕ_{1}  \natone (\nplus)

ℤ  \integer (\num)
ℝ  \real
div mod \div \mod
i^{n}  i^n i\expon n
succ  \succ
= ≠ = \neq
< ≤ ⩽ < \leq \leqslant
> ≥ ⩾ > \geq \geqslant
∗ / + − * / + -

Logic

¬  \lnot
∧  \land (\wedge)
∨  \lor (\vee)
∀  \all (\forall)
∃  \exi (\exists)
∃_{1}  \exione
∄  \nexi (\nexists)
•  @ \dot (\spot)
⇒  \imp (\implies)
⇔  \iff
true  \true
false \false
𝔹  \bool

Sets

{ | } \{ \cbar \}
∅  \emptyset
{ }  \varemptyset
∈  \mem (\in)
∉  \nem (\nmem \notin)
ℙ  \pset (\power)
𝔽  \fset (\finset)
ℙ_{1} 𝔽_{1} \fsetone \psetone
∪  \uni (\union)
∩  \int (\inter)
⊂  \psubs (\subset)
⊆  \subs (\subseteq)
⊃  \psups (\supset)
⊇  \sups (\supseteq)
×  \prod (\cross)
min max\min \max
#  \#
∪  \duni (\dunion)
∩  \dint (\dinter)
. .  \upto

Relations and Functions

λ μ \lambda \mu
dom \dom

ran  \ran
◁  \dres
− ◁  \dsub (\ndres)
▷  \rres
− ▷  \rsub (\nrres)
⊕  \fovr
∘  \cmp
o_{9}  \fcmp (\comp)
(| |) \limg \rimg
id  \id
R^{∼}  R^{-1}  R\inv
R^{+}  R^+     R\tcl
R^{∗}  R^*     R\rtcl
R^{k}  R^k     R\iter k
iter 0 R iter \, 0 \, R
↦  \map
↔  \rel
→  \tfun (\fun)
↣  \tinj (\inj)
\overrightarrow{→}  \tsur (\surj)
\underrightarrow{}\pfun
↣  \pinj
\underrightarrow{}\psur (\psurj)
\underrightarrow{}\ffun
\begin{matrix} \\ ↣ \end{matrix}  \finj
\underrightarrow{↣}  \bij

Sequences

seq  \seq
seq_{1}  \seqone
⟨ ⟩  \emptyseq
⟨ ⟩  \lseq \rseq
head tail \head \tail
front last \front \last
rev  \rev
next  \next
in  \inseq
⊆  \prefix
suffix  \suffix
squash  \squash
⌢  \cat
⌢/  \dcat
o_{9}/  \dcmp
⊕/  \dovr
↿  \ires
↾  \sres \filter
partitions \partitions
disjoint  \disjoint

Schemas

Δ  \Delta

≡ Ξ \equiv \Xi
pred \pred
pre  \pre
post \post
↾  \zproject \project
∧  \zand
∨  \zor
o_{9}  \zcmp (\semi)
∃  \zexi
∀  \zall
¬  \znot
\  \zhide (\hide)
/  \zfor
⇒  \zimp
⇔  \zeq
⊕  \zovr
>>  \zpipe
θ  \theta
[ | ] \lsch \zbar \rsch
.  .

Bags

[[ ]]  \lbag \rbag
bag  \bag
[[ ]]  \emptybag
items \items
count \bagcount
⊎  \buni
in  \inbag

Definitions and Declarations

::=  \ddef
|  \bbar
==  \defs
ˆ=  \sdef
≜  \varsdef
, ; : , ; :
⟨⟨ ⟩⟩ \lang \rang

Miscellaneous

[ ]  [ ]
( )  ( )
! ?  ! ?
let  \zlet
where \zwhere
in  \zin
⟨| |⟩ \lblot \rblot
iBump \intern Bump
INIT \Init
EXIT \Exit

8.2 Other Special Notation

Temporal Logic

□ − □ \always \uptilnow

       (\henceforth)

◯ ◯ ◯ ◯ ◯ − ◯ \atnext \atlast
◇  \eventually
− ◇  \previously

Proofs

Theorem \TH
Proof  \PR
Lemma \LE

□ □  \qed (\ETH) \Qed
□ ■  \QED \BLACKQED
⊢  \shows (\thrm)
⊨  \vDash
⊒  \refines
⊐ ∼  \weakrefine

Object-Z

𝕆  \oid
self  \self
contained \contained
INIT  \Init
A ∪ B  A \classuni B
↓A  \poly A
↾  \visibility
↾ ×  \invisibility
T_{◯ C}  T_\cid
T_{◯ S}  T_\sid
T_{◯ E}  T_\eid
 ∧  \cnj
 ∥  \pll
 ∥_{!}  \plo
 []  \gch
 o_{9}  \sqc
 •  \enh
∧  \dcnj
[]  \dgch
 o 9  \dsqc

Object Theory

≻  \subclass \isa
≿  \weaksubclass \islikea
≺  \supclass
≾  \weaksupclass
≻≻  \hasa \instantiates
≺≺  \instancein
⊏ ⊑ \subtype \subtypeeq
⊐ ⊒ \suptype \suptypeeq

Orders

monotonic  \mono
total order  \torder
partial order \porder

Word Styles

word \word{word}
word \keyword{word}
word \boldword{word}
\underline{word} \underword\{word\}
\underline{word} \underkeyword\{word\}
\underline{word} \underboldword\{word\}
‘word’ \String{word}
“word” \STRING{word}
a \underline{rel} b a \infix\{rel\} b

8.3 Special Letter Fonts

Greek

α  \alpha
β  \beta
γ Γ  \gamma \Gamma
δ Δ  \delta \Delta
ϵ ε  \epsilon \varepsilon
ζ  \zeta
η  \eta
θ ϑ Θ \theta \vartheta \Theta
ι  \iota
κ κ  \kappa \varkappa
λ Λ  \lambda \Lambda
μ  \mu
ν  \nu
ξ Ξ  \xi \Xi
π ϖ Π \pi \varpi \Pi
ρ ϱ  \rho \varrho
σ ς Σ \sigma \varsigma \Sigma
τ  \tau
υ Υ  \upsilon \Upsilon
ϕ φ Φ \phi \varphi \Phi
χ  \chi
ψ Ψ  \psi \Psi
ω Ω  \omega \Omega

Caligraphic

A  \cal A
B  \cal B
C  \cal C
D  \cal D
E  \cal E

F  \cal F
G  \cal G
H  \cal H
I  \cal I
J  \cal J
K  \cal K
L  \cal L
M  \cal M
N  \cal N
O  \cal O
P  \cal P
Q  \cal Q
R  \cal R
S  \cal S
T  \cal T
U  \cal U
V  \cal V
W  \cal W
X  \cal X
Y  \cal Y
Z  \cal Z

BlackBoard Bold

𝔸  \bbold A
𝔹  \bbold B
ℂ  \bbold C
𝔻  \bbold D
𝔼  \bbold E
𝔽  \bbold F
𝔾  \bbold G
ℍ  \bbold H
𝕀  \bbold I
𝕁  \bbold J
𝕂  \bbold K
𝕃  \bbold L
𝕄  \bbold M
ℕ  \bbold N
𝕆  \bbold O
ℙ  \bbold P
ℚ  \bbold Q
ℝ  \bbold R
𝕊  \bbold S
𝕋  \bbold T
𝕌  \bbold U
𝕍  \bbold V
𝕎  \bbold W
𝕏  \bbold X
𝕐  \bbold Y
ℤ  \bbold Z

Miscellaneous

ℏ  \hslash

ℏ  \hbar
϶  \backepsilon
ð  \eth
ℶ  \beth
ℷ  \gimel
ℸ  \daleth
∁  \complement
⊺  \intercal
ℵ  \aleph
∇  \nabla
ℏ  \hbar
ı  \imath
ȷ  \jmath
ℓ  \ell
℘  \wp
ℜ  \Re
ℑ  \Im
℧  \mho
𝟋  \digamma

8.4 Shapes

□  \Box
□  \square
■  \blacksquare
⋄  \diamond
◇  \Diamond
♢  \lozenge
♦  \blacklozenge
▷  \vartriangleright
◁  \vartriangleleft
▼  \blacktriangledown
▶  \blacktriangleright
◀  \blacktriangleleft
△  \vartriangle
▲  \blacktriangle
▽  \triangledown
△  \triangle
◁  \triangleleft
▷  \triangleright
△  \bigtriangleup
▽  \bigtriangledown
♣  \clubsuit
♢  \diamondsuit
♡  \heartsuit
♠  \spadesuit
∗  \ast
⋆  \star
✠  \maltese
⋆  \bigstar
◯  \bigcirc
∘  \circ
•  \bullet

▪  \centerdot
·  \cdot
· · ·  \cdots
. . .  \ldots
⋮  \vdots
...  \ddots

Circled Operations

Ⓢ  \circledS
⊚  \circledcirc
⊛  \circledast
⊝  \circleddash
®  \circledR
\begin{matrix}c \\ ◯ \end{matrix}  \copyright
⊕  \fovr
⊖  \ominus
⊗  \otimes
⊘  \oslash
⊙  \odot

Boxed operators

⊡  \boxdot
⊞  \boxplus
⊠  \boxtimes
⊟  \boxminus

8.5 Arrow Symbols

Left Arrows

←  \leftarrow \gets
⇐  \Leftarrow
↩  \hookleftarrow
↼  \leftharpoonup
↽  \leftharpoondown
⟵  \longleftarrow
⟸  \Longleftarrow
↞  \twoheadleftarrow
⇇  \leftleftarrows
↢  \leftarrowtail
⇚  \Lleftarrow
↚  \nleftarrow
⇍  \nLeftarrow

Right Arrows

→  \rightarrow \to
⇒  \Rightarrow

↦  \map
⟼  \longmapsto
↪  \hookrightarrow
⇀  \rightharpoonup
⇁  \rightharpoondown
⇝  \leadsto
⟶  \longrightarrow
⟹  \Longrightarrow
↠  \twoheadrightarrow
⇉  \rightrightarrows
↣  \rightarrowtail
⇝  \rightsquigarrow
⇛  \Rrightarrow
↛  \nrightarrow
⇏  \nRightarrow

Left Right Arrows

↔  \leftrightarrow
⇔  \Leftrightarrow
⇌  \rightleftharpoons
⟷ \longleftrightarrow
⟺ \Longleftrightarrow
⇌  \rightleftharpoons
⇋  \leftrightharpoons
⇆  \leftrightarrows
⇄  \rightleftarrows
↭  \leftrightsquigarrow
⇎  \nLeftrightarrow
↮  \nleftrightarrow

Up Down Arrows

↑  \uparrow
⇑  \Uparrow
↓  \downarrow
⇓  \Downarrow
↕  \updownarrow
⇕  \Updownarrow
⇈  \upuparrows
⇊  \downdownarrows
↾  \upharpoonright
⇂  \downharpoonright
↿  \upharpoonleft
⇃  \downharpoonleft

Miscellaneous

↗  \nearrow
↘  \searrow
↙  \swarrow
↖  \nwarrow
⟳  \circlearrowright
⟲  \circlearrowleft
↰  \Lsh
↱  \Rsh
↫  \looparrowleft
↬  \looparrowright
↶  \curvearrowleft
↷  \curvearrowright

8.6 Relations

≪  \ll
≫  \gg
≪  \lll \llless
≫  \ggg \gggtr
⊏  \sqsubset
⊐  \sqsupset
⊑  \sqsubseteq
⊒  \sqsupseteq
∋  \owns
⊢  \vdash
⊩  \Vdash
⊨  \vDash
⊣  \dashv
⊪  \Vvdash
⊧  \models
⊬  \nvdash
⊮  \nVdash
⊭  \nvDash
⊯  \nVDash
⊥  \perp
∼  \sim
≃  \simeq
≂  \eqsim
∽  \backsim
⋍  \backsimeq
∼  \thicksim
≁  \nsim
≈  \approx

≉  \napprox
≈  \thickapprox
≊  \approxeq
≍  \asymp
≅  \cong
≇  \ncong
≐  \doteq
≑  \Doteq \doteqdot
≓  \risingdotseq
≒  \fallingdotseq
⋖  \lessdot
⋗  \gtrdot
≖  \eqcirc
≗  \circeq
≏  \bumpeq
≎  \Bumpeq
≜  \triangleq
⊸  \multimap
∝  \propto
∝  \varpropto
≲  \lesssim
≳  \gtrsim
⪅  \lessapprox
⪆  \gtrapprox
≺  \xprec
≻  \xsucc
⪯  \preceq
⪰  \succeq
≾  \precsim
≿  \succsim
≾  \precapprox
≿  \succapprox
⪕  \eqslantless
⪖  \eqslantgtr
⋞  \curlyeqprec
⋟  \curlyeqsucc
≼  \preccurlyeq
≽  \succcurlyeq
≦  \leqq
≧  \geqq
⩽  \leqslant
⩾  \geqslant
≶  \lessgtr
≷  \gtrless
⋚  \lesseqgtr

⋛  \gtreqless
⪋  \lesseqqgtr
⪌  \gtreqqless
≨  \lvertneqq
≩  \gvertneqq
≰  \nleq
≱  \ngeq
≮  \nless
≯  \ngtr
⊀  \nprec
⊁  \nsucc
≨  \lneqq
≩  \gneqq
⩽̸  \nleqslant
⩾̸  \ngeqslant
⪇  \lneq
⪈  \gneq
⪯̸  \npreceq
⪰̸  \nsucceq
⋨  \precnsim
⋩  \succnsim
⋦  \lnsim
⋧  \gnsim
≦̸  \nleqq
≧̸  \ngeqq
⪵  \precneqq
⪶  \succneqq
⪹  \precnapprox
⪺  \succnapprox
⪉  \lnapprox
⪊  \gnapprox
⋐  \Subset
⋑  \Supset
⫅  \subseteqq
⫆  \supseteqq
⫅̸  \nsubseteqq
⫆̸  \nsupseteqq
⫋  \subsetneqq
⫌  \supsetneqq
⊊  \subsetneq
⊋  \supsetneq
⊈  \nsubseteq
⊉  \nsupseteq

⊵  \trianglerighteq
⊴  \trianglelefteq
⋭  \ntrianglerighteq
⋬  \ntrianglelefteq
⋪  \ntriangleleft
⋫  \ntriangleright
≬  \between
|  | \vert \mid
∥  \| \Vert \parallel
∥|  \interleave
∣  \shortmid
∥  \shortparallel
∣∥  \shortinterleave
∦  \nparallel
∤  \nmid
∤  \nshortmid
∦  \nshortparallel

8.7 Binary Operations

⋏  \curlywedge
⋎  \curlyvee
⊻  \veebar
⊼  \barwedge
⩞  \doublebarwedge
±  \pm
∓  \mp
×  \times
⋉  \ltimes
⋊  \rtimes
⋋  \leftthreetimes
⋌  \rightthreetimes
⋇  \divideontimes
÷  \divides
⊎  \uplus
⊓  \sqcap
⊔  \sqcup
⋓  \Cup \doublecup
⋒  \Cap \doublecap
\  \backslash
\  \setminus
∖  \smallsetminus
≀  \wr

⊲  \lhd
⊳  \rhd
⊴  \unlhd
⊵  \unrhd
↾  \restriction
⨿  \amalg
⊤  \top
⊥  \bot
⌣  \smallsmile
⌢  \smallfrown
⌣  \smile
⌢  \frown
⋔  \pitchfork
∔  \dotplus
⋈  \Join
▷◁  \bowtie

8.8 Miscellaneous Symbols

†  \dagger
‡  \ddagger
§  \sectionsymbol
¶  \P
∠  \angle
∡  \measuredangle
∢  \sphericalangle
′  \prime
‵  \backprime
√  \surd
∫  \smallint
♭  \flat
♮  \natural
♯  \sharp
∂  \partial
∞  \infty
¥  \yen
∴  \therefore
∵  \because
✓  \checkmark

8.9 Variable-sized Symbols

These symbols come in two sizes which do not vary with the point size of your font. The big size can be obtained by preceding the symbol command with the command \displaystyle.

∑ ∑ \sum
∏ ∏ \product

∐ ∐ \coprod
∫ ∫  \integral
∮ ∮  \oint
⋂ ⋂ \bigcap
⋃ ⋃ \bigcup
⨆ ⨆ \bigsqcup
⋁ ⋁ \bigvee
⋀ ⋀ \bigwedge
⨀ ⨀ \bigodot
⨂ ⨂ \bigotimes
⨁ ⨁ \bigoplus
⨄ ⨄ \biguplus

8.10 Delimiters

These symbols can be made large to surround large formula. E.g.,

⌊∑_{i=1}^{n} x^{i}⌋

was generated using

\left\lfloor...\right\rfloor

( )  ( )
{ } \{ \}
⌊ ⌋ \lfloor \rfloor
⌈ ⌉ \lceil \rceil
⟨ ⟩  \langle \rangle
⌜ ⌝ \ulcorner \urcorner
⌞ ⌟ \llcorner \lrcorner
↑  \uparrow
↓  \downarrow
↕  \updownarrow
⇑  \Uparrow
⇓  \Downarrow
⇕  \Updownarrow

8.11 Math Accents

â  \hat{a}
â  \widehat{a}
âa  \widehat{aa}
âaa  \widehat{aaa}
ã  \tilde{a}

ã  \widetilde{a}
ãa  \widetilde{aa}
ãaa  \widetilde{aaa}
ǎ  \check{a}
ă  \breve{a}
á  \acute{a}
à  \grave{a}
ā  \bar{a}
a⃗  \vec{a}
ȧ  \dotaccent{a}
ä  \ddot{a}

8.12 Size Commands

μ μ μ \mu \zsmall\mu \zSmall\mu
μ μ μ \zbig\mu \zBig\mu \zBIG\mu