# LaTeX Formal Methods Reference¶

The general idea of this reference is to provide a cheatsheet for writing math in LaTeX for someone who’s not particularily sure of either, such as myself. Each table contains a description of some symbol or concept, a rendering of the symbol, a LaTeX source, and, optionally, some odd notes on the concept or rendering. I hope to continue expanding this reference until I run out of Universe to fit it in. This is what I’v got so far though:

I lean heavily on Chapter 2 of Andrew Harry’s Formal Methods Fact File: VDM and Z for most of the theoretical contents of the tables. I also used Richard Hammack’s Book of Proof for some formulas and descriptions. Detexify and Wikibooks are invaluable reasorces for LaTeX stuff. Also, afor more complete reference of LaTeX symbols try The Comprehensive LaTeX Symbol List by Scott Pakin.

There are two sections related to transactional memory. One lists some of the symbols used by Guerraoui and Kapałka in Principles of Transactional Memory as well as from other work on that subject, which are used fairly commonly to describe various things pertaining to TM histories. The other lists symbols devised by Paweł T. Wojciechowski to render TM histories (or traces) without having to make drawings.

Please note that the symbols here are rendered via JavaScript by sphinx.ext.mathjax or sphinx.ext.jsmath and may therefore differ from what LaTeX will render. I am also not able to render some symbols at all here that will work perfectly fine in LaTeX, in which case I will note so by the relevant concept.

I provide (automatically generate) the source for the LaTeX for of all concepts, but not for the formulas sometimes found in notes. Their source can be viewed nevertheless by right-clicking them and selecting Show Source from the drop down menu (thanks to Sphinx and MathJax). This works for the second column just as well.

This is a (perpetual) work in progress, so comments etc. are especially welcome.

## Variable Names¶

Concept Math LaTeX Notes
Sets $$A,B,C$$ A,B,C upper-case letters
Indexed sets $$A_1, A_2, \ldots, A_n$$ A_1, A_2, \ldots, A_n the index may be of any type, not nec. an integer
Statements $$P, Q, R, S$$ P, Q, R, S fun fact: rearranged they stand for Senatus Populusque Romanus
Statements with variables $$P(x), Q(x), R(x), S(x)$$ P(x), Q(x), R(x), S(x)

## Set Theory¶

Concept Math LaTeX Notes
Set $$\{a,b,c\}$$ \{a,b,c\} set enumeration
Set $$\{\,x \mid P(x)\,\}$$ or $$\{\,x : P(X)\,\}$$ \{\,x \mid P(x)\,\} or \{\,x : P(X)\,\} set comprehension (described implicitly with the property $$P$$) aka set-builder notation
Infinite set $$\{1,2,3,\ldots\}$$ \{1,2,3,\ldots\} and so on
Infinite set $$\{\ldots,1,2,3,\ldots\}$$ \{\ldots,1,2,3,\ldots\} and so on
Empty set $$\varnothing$$ or $$\emptyset$$ or $$\{\}$$ \varnothing or \emptyset or \{\}
Powerset $$\mathbb{P}(S)$$ or $$\mathcal{P}(S)$$ \mathbb{P}(S) or \mathcal{P}(S) set of all possible subsets of set $$S$$, $$|\mathbb{P}(S)| = 2^{|S|}$$
Member $$x \in A$$ x \in A
Not member $$x \not\in A$$ x \not\in A
Subset $$A \subset B$$ or $$A \subseteq B$$ A \subset B or A \subseteq B
Not subset $$A \not\subset B$$ or $$A \nsubseteq B$$ A \not\subset B or A \nsubseteq B
Set equality $$A = B$$ A = B $$A \subseteq B \text{ and } B \subseteq A$$
Union $$A \cup B$$ A \cup B
Intersection $$A \cap B$$ A \cap B
Distributed or generalized union $$\bigcup SS$$ \bigcup SS over set of sets
Distributed or generalized intersection $$\bigcap SS$$ \bigcap SS over set of sets
Relative complement $$A - B$$ or $$A \setminus B$$ A - B or A \setminus B $$\{\,x \mid x \in A \text{ and } x \not\in B\,\}$$
Absolute complement $$A + B$$ A + B $$(A - B) \cup (B - A)$$
Disjoint sets     $$A \cap B = \varnothing$$
Set cardinality (aka size) $$\mathbf{card}(S)$$ or $$|S|$$ \mathbf{card}(S) or |S| number of members of $$S$$
Boolean set $$\mathbb{B}$$ or $$\{\mathrm{true}, \mathrm{false}\}$$ or $$\{tt, ff\}$$ or $$\{1, 0\}$$ \mathbb{B} or \{\mathrm{true}, \mathrm{false}\} or \{tt, ff\} or \{1, 0\}
Natural numbers set $$\mathbb{N}$$ or $$\mathbb{N}^+$$ \mathbb{N} or \mathbb{N}^+ $$\mathbb{N}^+ = \mathbb{N} \setminus \{0\}$$
Integer numbers set $$\mathbb{Z}$$ \mathbb{Z}
Rational numbers set $$\mathbb{Q}$$ \mathbb{Q} $$\frac{a}{b}$$, $$a$$ - numerator, $$b$$ - denominator, $$b \neq 0$$
Real numbers set $$\mathbb{R}$$ \mathbb{R}
Set of prime numbers $$\mathbb{N}$$ \mathbb{N}
Set of irrational numbers $$\mathbb{I}$$ \mathbb{I}
Set of complex numbers $$\mathbb{C}$$ \mathbb{C}

## Cartesian Products¶

Concept Math LaTeX Notes
Ordered Pair $$(a,b)$$ (a,b)
Triple $$(a,b,c)$$ (a,b,c)
N-tuple $$(e_1, \ldots, e_n)$$ (e_1, \ldots, e_n)
Cartesian product $$A \times B$$ A \times B $$\{\,(a,b) \mid a \in A, b \in B\,\}$$
Cartesian plane $$\mathbb{R} \times \mathbb{R}$$ \mathbb{R} \times \mathbb{R} $$\{\,(x,y) \mid x,y \in \mathbb{R}\,\}$$
Cartesian power $$A^n$$ A^n $$A \times A \times \ldots \times A = \{x_1,x_2,\ldots, x_n | x_1,x_2,\ldots,x_n \in A\}$$

## Types¶

Concept Math LaTeX Notes
User defined type $$\mathrm{DEFINEDTYPE} = \{2,4,8\}$$ \mathrm{DEFINEDTYPE} = \{2,4,8\} a set defined explicitly, or by set comprehension
Product type $$\mathbb{B} \times \mathbb{B}$$ \mathbb{B} \times \mathbb{B} a set of tuples (here, $$\{(tt,tt),(tt,ff),(ff,ff),(ff,tt)\}$$)
Two-argument function signature $$\textrm{func}:\mathbb{R} \times \mathbb{N} \rightarrow \mathbb{N}$$ \textrm{func}:\mathbb{R} \times \mathbb{N} \rightarrow \mathbb{N} type of arguments is product type
Enumerated type $$\textrm{signal} = \textrm{RED}~|~\textrm{ORANGE}~|~\textrm{GREEN}$$ \textrm{signal} = \textrm{RED}~|~\textrm{ORANGE}~|~\textrm{GREEN} type union of literals

## Mathematical Operators¶

Concept Math LaTeX Notes
Absolute operator $$\mathbf{abs}\ {-20} = 20$$ \mathbf{abs}\ {-20} = 20 unary
Floor/integer part operator $$\mathbf{floor}\ 2.5 = 2$$ \mathbf{floor}\ 2.5 = 2 unary
Integer division operator $$5\ \mathbf{div}\ 2 = 2$$ 5\ \mathbf{div}\ 2 = 2 binary
Remainder operator $$5\ \mathbf{rem}\ {-2} = 1$$ 5\ \mathbf{rem}\ {-2} = 1 binary
Modulus operator $$5\ \mathbf{mod}\ {-2} = -1$$ 5\ \mathbf{mod}\ {-2} = -1 binary
Equality $$a = b$$ a = b binary
Inequality $$a \neq b$$ a \neq b binary
Less than $$a > b$$ a > b binary
Less than or equal $$a \ge b$$ a \ge b binary
More than $$a < b$$ a < b binary
More than or equal $$a \le b$$ a \le b binary

## Bags¶

Concept Math LaTeX Notes
Bag $$[\![ a,b,b,c,d ]\!]$$ [\![ a,b,b,c,d ]\!] Members can repeat, unordered, also \llbracket and \rrbracket from package stmaryrd look better
Count operator $$\mathbf{count}[\![ a,b,b,c,d ]\!] b = 2$$ \mathbf{count}[\![ a,b,b,c,d ]\!] b = 2 How many times element $$b$$ occurs in bag
Bag cardinality $$\mathbf{card}(B)$$ \mathbf{card}(B) Number of members of $$B$$
Bag union (1) $$[\![ a,b,b,c,d ]\!] \cup [\![ a,b,c,c,d ]\!] = [\![ a,b,b,c,c,d ]\!]$$ [\![ a,b,b,c,d ]\!] \cup [\![ a,b,c,c,d ]\!] = [\![ a,b,b,c,c,d ]\!] Maximum number an element occurs
Bag union (2) $$[\![ a,b,b,c,d ]\!] \cup [\![ a,b,c,c,d ]\!] = [\![ a,a,b,b,b,c,c,c,d,c ]\!]$$ [\![ a,b,b,c,d ]\!] \cup [\![ a,b,c,c,d ]\!] = [\![ a,a,b,b,b,c,c,c,d,c ]\!] Sum of elements
Bag intersection $$[\![ a,b,b,c,d ]\!] \cap [\![ a,b,c,c,d ]\!] = [\![ a,b,c,d ]\!]$$ [\![ a,b,b,c,d ]\!] \cap [\![ a,b,c,c,d ]\!] = [\![ a,b,c,d ]\!] Minimum number an element occurs
Bag difference $$[\![ a,b,b,c,d ]\!] - [\![ a,b,c,c,d ]\!] = [\![ b,c ]\!]$$ [\![ a,b,b,c,d ]\!] - [\![ a,b,c,c,d ]\!] = [\![ b,c ]\!] Subtract the number of elements in the second bag from the first

## Sequences¶

Concept Math LaTeX Notes
Empty sequence [] []
Sequence (explicit declaration) $$[ a,b,b,d ]$$ [ a,b,b,d ] In that order. This is the typical representation.
Sequence (implicit declaration) $$[\,e \mid P(e)\,]$$ [\,e \mid P(e)\,] Set comprehension (described implicitly with the property $$P$$)
Head of a sequence $$\mathbf{hd}~A$$ \mathbf{hd}~A $$\mathbf{hd}~[ a,b,b,c ] = a$$
Tail of a sequence $$\mathbf{tl}~A$$ \mathbf{tl}~A $$\mathbf{tl}~[ a,b,b,c ] = [ b,b,c ]$$
Length of a sequence $$\mathbf{len}~A$$ \mathbf{len}~A $$\mathbf{len}~[ a,b,b,c ] = 4$$
Element selection (by application) $$A(n)$$ A(n) Select the $$n$$-th element of the sequence
Indices of a sequence $$\mathbf{inds}~A$$ \mathbf{inds}~A $$\mathbf{inds}~[ a,b,c ] = \{1,2,3\}$$
Elements of a sequence $$\mathbf{elems}~A$$ \mathbf{elems}~A $$\mathbf{elems}~[ a,b,b,c ] = \{a,b,c\}$$
Sequence concatenation     Symbol varies between notations
List $$<a,b,c>$$ or $$(a,b,c)$$ or $$abc$$ <a,b,c> or (a,b,c) or abc An alternative notation and naming used by some formal notations
Empty list $$()$$ ()

## Formal Logic¶

Concept Math LaTeX Notes
Conjunction (AND) $$\wedge$$ or $$\&$$ or $$.$$ \wedge or \& or . Alternatively \with from package cmll instead of \&.
Alternative (OR) $$\vee$$ or $$|$$ or $$+$$ \vee or | or +
Negation (NOT) $$\neg$$ or $$\sim$$ \neg or \sim
Implication $$\rightarrow$$ or $$\Rightarrow$$ or $$\supset$$ \rightarrow or \Rightarrow or \supset $$\text{premise} \rightarrow \text{conclussion}$$
Equivalence $$\leftrightarrow$$ or $$\Leftrightarrow$$ or $$\equiv$$ \leftrightarrow or \Leftrightarrow or \equiv

### Equivalence Laws¶

Concept Math LaTeX Notes
Commutation (conjunctions) $$(P \wedge Q) \equiv (Q \wedge P)$$ (P \wedge Q) \equiv (Q \wedge P)
Commutation (alternatives) $$(P \vee Q) \equiv (Q \vee P)$$ (P \vee Q) \equiv (Q \vee P)
Commutation (equivalences) $$(P \leftrightarrow Q) \equiv (Q \leftrightarrow P)$$ (P \leftrightarrow Q) \equiv (Q \leftrightarrow P)
Association (conjunctions) $$P \wedge (Q \wedge R) \equiv (P \wedge Q) \wedge R$$ P \wedge (Q \wedge R) \equiv (P \wedge Q) \wedge R
Association (alternatives) $$P \vee (Q \vee R) \equiv (P \vee Q) \vee R$$ P \vee (Q \vee R) \equiv (P \vee Q) \vee R
Distribution (1) $$P \vee (Q \wedge R) \equiv (P \vee Q) \wedge (P \vee R)$$ P \vee (Q \wedge R) \equiv (P \vee Q) \wedge (P \vee R)
Distribution (2) $$P \wedge (Q \vee R) \equiv (P \wedge Q) \vee (P \wedge R)$$ P \wedge (Q \vee R) \equiv (P \wedge Q) \vee (P \wedge R)
De Morgan’s Law (negation of conjunction) $$\neg(P \wedge Q) \equiv \neg P \vee \neg Q$$ \neg(P \wedge Q) \equiv \neg P \vee \neg Q
De Morgan’s Law (negation of alternative) $$\neg(P \vee Q) \equiv \neg P \wedge \neg Q$$ \neg(P \vee Q) \equiv \neg P \wedge \neg Q
Double Negation $$\neg\neg P \equiv P$$ \neg\neg P \equiv P
Excluded Middle $$P \vee \neg P \equiv tt$$ P \vee \neg P \equiv tt
Contradiction $$P \wedge \neg P \equiv ff$$ P \wedge \neg P \equiv ff
Material Implication $$P \rightarrow Q \equiv \neg P \vee Q$$ P \rightarrow Q \equiv \neg P \vee Q
Material Equivalence (1) $$(P \leftrightarrow Q) \equiv (P \rightarrow Q) \wedge (Q \rightarrow P)$$ (P \leftrightarrow Q) \equiv (P \rightarrow Q) \wedge (Q \rightarrow P)
Material Equivalence (2) $$(P \leftrightarrow Q) \equiv (P \wedge Q) \vee (\neg Q \wedge \neg P)$$ (P \leftrightarrow Q) \equiv (P \wedge Q) \vee (\neg Q \wedge \neg P)
Exportation $$(P \wedge Q) \rightarrow R \equiv P \rightarrow (Q \rightarrow R)$$ (P \wedge Q) \rightarrow R \equiv P \rightarrow (Q \rightarrow R)
Or-Simplification $$P \vee P \equiv P$$ P \vee P \equiv P
Or-Simplification (true) $$P \vee tt \equiv tt$$ P \vee tt \equiv tt
Or-Simplification (false) $$P \vee ff \equiv P$$ P \vee ff \equiv P
And-Simplification $$P \wedge P \equiv P$$ P \wedge P \equiv P
And-Simplification (true) $$P \wedge tt \equiv P$$ P \wedge tt \equiv P
And-Simplification (false) $$P \wedge ff \equiv ff$$ P \wedge ff \equiv ff

### Logic Forms¶

Concept Math LaTeX Notes
Modus Ponens $$P \rightarrow Q, P \vdash Q$$ P \rightarrow Q, P \vdash Q Andrew Harry uses \uptherefore from MnSymbol
Modus Tollens $$P \rightarrow Q, \neg Q \vdash \neg P$$ P \rightarrow Q, \neg Q \vdash \neg P
Hypothetical Syllogism $$P \rightarrow Q, Q \rightarrow R \vdash P \rightarrow R$$ P \rightarrow Q, Q \rightarrow R \vdash P \rightarrow R
Constructive Dillema $$P \rightarrow Q \wedge R \rightarrow S, P \vee R \vdash Q \vee S$$ P \rightarrow Q \wedge R \rightarrow S, P \vee R \vdash Q \vee S
Destructive Dillema $$P \rightarrow Q \wedge R \rightarrow S, \neg Q \vee \neg S \vdash \neg P \vee \neg R$$ P \rightarrow Q \wedge R \rightarrow S, \neg Q \vee \neg S \vdash \neg P \vee \neg R
Conjunction $$P, Q \vdash P \wedge Q$$ P, Q \vdash P \wedge Q
Addition $$P \vdash P \vee Q$$ P \vdash P \vee Q

### Predicate Logic¶

Concept Math LaTeX Notes
Universal qualifier (all) $$\forall_x$$ \forall_x
Universal specification $$\forall_x \bullet P_x$$ \forall_x \bullet P_x $$\forall_x \bullet \mathrm{man}(x) \rightarrow \mathrm{mortal}(x)$$
Existential qualifier (exists) $$\exists_x$$ \exists_x
Existential specification $$\exists_x \bullet P_x$$ \exists_x \bullet P_x $$\exists_x \bullet \mathrm{Socrates}(x) \wedge \mathrm{man}(x)$$
Ranging over types (1) $$\forall_x \in X$$ or $$\forall_x : X$$ \forall_x \in X or \forall_x : X The former suggests $$X$$ is a set, the latter that it is a type
Ranging over types (2) $$\exists_x \in X$$ or $$\exists_x : X$$ \exists_x \in X or \exists_x : X The former suggests $$X$$ is a set, the latter that it is a type
Covnersion between qualifiers (1) $$\forall_x \bullet P_x \equiv \neg\exists_x \bullet \neg P_x$$ \forall_x \bullet P_x \equiv \neg\exists_x \bullet \neg P_x Alternatively $$\nexists_x$$
Covnersion between qualifiers (2) $$\neg\forall_x \bullet P_x \equiv \exists_x \bullet \neg P_x$$ \neg\forall_x \bullet P_x \equiv \exists_x \bullet \neg P_x
Covnersion between qualifiers (3) $$\neg\forall_x \bullet \neg P_x \equiv \exists_x \bullet P_x$$ \neg\forall_x \bullet \neg P_x \equiv \exists_x \bullet P_x
Covnersion between qualifiers (4) $$\forall_x \bullet \neg P_x \equiv \neg\exists_x \bullet P_x$$ \forall_x \bullet \neg P_x \equiv \neg\exists_x \bullet P_x Alternatively $$\nexists_x$$

## Relationships and Functions¶

Concept Math LaTeX Notes
A mapping $$x \mapsto y$$ or $$(x, y)$$ x \mapsto y or (x, y)
Function signiature $$f:X \rightarrow Y$$ f:X \rightarrow Y Mapping from $$X$$ (domain) to $$Y$$ (co-domain). What is allowed to be in $$X$$, $$Y$$ is described by the precondition, postcondition.
Function definition $$\mathbf{square}(x) = x^2\ \text{where}\ 1 \le x \le 5$$ \mathbf{square}(x) = x^2\ \text{where}\ 1 \le x \le 5
Function defined as co-ordinates $$\mathbf{square} = \{(1,2), (2,4), (3,9), (4,16), (5,25)\}$$ \mathbf{square} = \{(1,2), (2,4), (3,9), (4,16), (5,25)\} The set of right coordinates (here $$\{2,4,9,16,25\}$$) is the range of a function
Range $$\mathrm{range}(f)$$ \mathrm{range}(f) $$\mathrm{range}(\{(1,a),(2,b),(3,c)\}) = \{a,b,c\}$$
Partial function signiature $$f:X \nrightarrow Y$$ f:X \nrightarrow Y Not all elements from $$X$$ are mapped to elements from $$Y$$

## Transactional Memory¶

Concept Math LaTeX Notes
History $$H$$ H
Sequential witness history $$S$$ or $$\hat{S}$$ S or \hat{S}
Completion
T-objects
Transaction $$T_i$$, $$T_j$$, $$T_k$$ T_i, T_j, T_k
Subhistory – transaction $$H|T_i$$ H|T_i A subhistory containing all operations in history $$H$$ that are executed within transaction $$T_i$$
Subhistory – t-object $$H|x$$ H|x A subhistory containing all operations in history $$H$$ that are executed on t-object $$x$$
History prefix $$H = H' \circ H''$$ H = H' \circ H'' $$H'$$ is a prefix of $$H''$$
Commit
Abort
Forced abort
Write
Operation $$\pi$$ \pi

### Notation for Presenting Histories¶

Concept Math LaTeX Notes
Variables $$x,y,z$$ x,y,z
Variable local copy or buffer $$\underline{x}$$ \underline{x} Transaction’s copy of $$x$$
Variable versioning $$\overset{n}{x}$$ \overset{n}{x} Variable $$x$$ with version $$n$$
Transaction identifiers $$T_i$$, $$T_j$$, $$T_k$$ T_i, T_j, T_k
Retried transaction identifiers $$T_i'$$, $$T_i''$$, $$T_i'''$$ T_i', T_i'', T_i''' Transaction $$T_i$$‘s first, second, etc. retry
Read operation $$r(x)v$$ r(x)v Reads value $$v$$ from variable $$x$$, can be used with specific values, e.g., $$r(x)1$$
Write operation $$w(x)v$$ w(x)v Writes value $$v$$ to variable $$x$$, can be used with specific values, e.g., $$w(x)1$$
Read-write operation $$\{x \xrightarrow{v} y\}$$ or $$\{y \xleftarrow{v} x\}$$ \{x \xrightarrow{v} y\} or \{y \xleftarrow{v} x\} Shorthand for the sequence $$r(x)v, w(y)v$$
Read operation with explicit membership $$r_i(x)v$$ r_i(x)v Read operation executed within $$T_i$$
Write operation with explicit membership $$w_i(x)v$$ w_i(x)v Write operation executed within $$T_i$$
Operation identifier $$\mathit{op}, \mathit{op}^r, \mathit{op}^w, \mathit{op}_i$$ \mathit{op}, \mathit{op}^r, \mathit{op}^w, \mathit{op}_i Operation, read operation, write operation, operation within $$T_i$$
Operation membership $$\mathit{op} \in T_i$$ \mathit{op} \in T_i Shorthand for $$\mathit{op} \in H|T_i$$
Transaction start $$[\![$$ or $$\llbracket$$ [\![ or \llbracket $$\llbracket$$ requires the stmaryrd package
Transaction commit $$]\!]$$ or $$\rrbracket$$ ]\!] or \rrbracket $$\rrbracket$$ requires the stmaryrd package
Transaction abort $$\circlearrowright$$ or $$\righttoleftarrow$$ or $$\curvearrowleft$$ \circlearrowright or \righttoleftarrow or \curvearrowleft in amsmath or mathabx or amssymb, respectively
Weak transaction start $$[$$ [ Used to indicate transactions with relaxed properties, e.g. eventually consistent transactions
Weak transaction commit $$]$$ ] Used to indicate transactions with relaxed properties, e.g. eventually consistent transactions
Irrevocable operation $$\mathit{irr}$$ or $$\mathit{ir}$$ \mathit{irr} or \mathit{ir}
Happens-before relation $$\searrow$$ \searrow Often rotated by about 22 degrees to be more visually appealing
Point in time $$\tau$$ \tau E.g. transaction $$T_i$$ starts at time $$\tau_i$$
State at point in time $$\{ x\!=\!1,y\!=\!2,z\!=\!3 \}$$ \{ x\!=\!1,y\!=\!2,z\!=\!3 \}
Examples     See examples in our papers, e.g. here or here

## Theorems¶

Concept Math LaTeX Notes
Proof $$\begin{proof} ... \end{proof}$$ \begin{proof} ... \end{proof}
Named proof $$\begin{proof}[name] ... \end{proof}$$ \begin{proof}[name] ... \end{proof}

## Various¶

Concept Math LaTeX Notes
Binominal coefficient $$\binom{n}{k} = \frac{n!}{k!(n-k)!}$$ \binom{n}{k} = \frac{n!}{k!(n-k)!} aka choose function (pl. symbol Newtona)
Divisor $$a | b$$ a | b $$ax=b$$ and $$a,b,x \in \mathbb{Z}$$