|
$\land$
|
\land
|
Logical conjunction.
|
|
$\lor$
|
\lor
|
Logical disjunction
|
|
$\Rightarrow$
|
\Rightarrow
|
Logical implication. Sometimes written with $\supset$ or $\rightarrow$.
|
|
$\neg$
|
\neg
|
Logical negation.
|
|
$\top$
|
\top
|
True, or the "top" element of a lattice or order.
|
|
$\bot$
|
\bot
|
False, or the "bottom" element of a lattice or order.
|
|
$\forall$
|
\forall
|
Universal quantifier
|
|
$\exists$
|
\exists
|
Existential quantifier
|
|
$\in$
|
\in
|
Read "is an element of", i.e. if the left hand side is in the set on the right hand side.
|
|
$\longleftrightarrow$
|
\longleftrightarrow
|
Parsing relation
|
|
$\Leftrightarrow$
|
\Leftrightarrow
|
If and only if
|
|
$::=$
|
::=
|
Definition of a non-terminal production in Backus-Naur Form.
|
|
$\vdash$
|
\vdash
|
Used for hypothetical derivations and contexts. $A \vdash B$ can be read as $\dfrac{A}{B}$.
|
|
$\dfrac{A}{B}$
|
\dfrac{A}{B}
|
An inference rule.
|
|
$\rightarrow$
|
\rightarrow
|
A function type. Sometimes denotes implication.
|
|
$:$
|
:
|
$e : \tau$ says that $e$ has type $\tau$. Written :: in Haskell, where : means cons.
|
|
$\mathbb{N}$
|
\mathbb{N}
|
The set of natural numbers.
|
|
$\mathbb{Z}$
|
\mathbb{Z}
|
The set of integers.
|
|
$\equiv_\alpha$
|
\equiv_\alpha
|
α-equivalence
|
|
$\equiv_{\alpha\beta}$
|
\equiv_{\alpha\beta}
|
αβ-equivalence
|
|
$\equiv_{\alpha\beta\eta}$
|
\equiv_{\alpha\beta\eta}
|
αβη-equivalence
|
|
$e[x := t]$
|
e[x := t]
|
A substitution, replacing $x$ with $t$ in $e$.
|
|
$e[{}^t/_x]$
|
e[{}^t/_x]
|
A substitution, replacing $x$ with $t$ in $e$.
|
|
$e_{\uparrow n}$
|
e_{\uparrow n}
|
The up-shifting operation, incrementing all de Bruijn indices greater or equal to $n$ in $e$.
|
|
$e_1\ e_2$
|
e_1\ e_2
|
Function application.
|
|
$x.\ t$
|
x.\ t
|
Binding or abstraction in higher-order abstract syntax.
|
|
$\lambda x.\ y$
|
\lambda x.\ y
|
A λ-abstraction taking the argument $x$ and returning $y$.
|
|
$[\![\cdot]\!]$
|
\llbracket\cdot\rrbracket
|
The function from syntax to semantics in denotational semantics.
|
|
$\mapsto$
|
\mapsto
|
The small-step semantics transition relation
|
|
$\Downarrow$
|
\Downarrow
|
The big-step semantics evaluation relation.
|
|
$\stackrel{\star}{\mapsto}$
|
\stackrel{\star}{\mapsto}
|
The reflexive transitive closure of $\mapsto$.
|
|
$\cup$
|
\cup
|
Set union.
|
|
$\cap$
|
\cap
|
Set intersection.
|
|
$\setminus$
|
\setminus
|
Set subtraction, i.e $A \setminus B$ is all the elements of $A$ which are not in $B$.
|
|
$\emptyset$
|
\emptyset
|
The empty set, the set with no elements.
|
|
$\times$
|
\times
|
Multiplication of numbers, cartesian product or a product type.
|
|
$\{ x \}$
|
\{ x \}
|
Brackets used to indicate construction of a set.
|
|
$\{ x\ |\ \psi \}$
|
\{ x\ |\ \psi \}
|
A set comprehension. The set of all $x$ where $\psi$ holds.
|
|
$\subset$
|
\subset
|
Used to denote strict subset.
|
|
$\subseteq$
|
\subseteq
|
Denotes subset.
|
|
$\supset$
|
\supset
|
Used for strict superset and sometimes implication.
|
|
$\supseteq$
|
\supseteq
|
Used for superset.
|
|
$\{ \varphi \}\ s\ \{ \psi \}$
|
\{ \phi \}\ s\ \{ \psi \}
|
A Hoare triple.
|
|
$\leadsto$
|
\leadsto
|
A useful symbol. Often used to indicate the output of an algorithmic judgement, such as in the TinyImp static semantics.
|
|
$\circ$
|
\circ
|
Used as an operator for function composition. Used as a symbol to denote the empty stack.
|
|
$\triangleright$
|
\triangleright
|
Used in the C-machine and similar to denote a frame on top of a stack.
|
|
$\succ$
|
\succ
|
The mode of the C-machine and E-machine that indicates the machine is evaluating an expression.
|
|
$\prec$
|
\prec
|
The mode of operation for the C-machine and E-machine that indicates that the machine is currently returning a value.
|
|
$\mathbb{R}$
|
\mathbb{R}
|
The set of real numbers.
|
|
$\mathcal{O}(f)$
|
\mathcal{O}(f)
|
The big-O notation.
|
|
$\bullet$
|
\bullet
|
A symbol sometimes used to denote the empty environment.
|
|
$\square$
|
\square
|
A blank square, used to indicate a hole in a one-hole context.
|
|
$\mapsto_M$
|
\mapsto_M
|
The transition relation for the M-machine.
|
|
$\mapsto_C$
|
\mapsto_C
|
The transition relation for the C-machine.
|
|
$\mapsto_E$
|
\mapsto_E
|
The transition relation for the E-machine.
|
|
$\langle\!\langle \eta, f.x.\ e \rangle\!\rangle$
|
\llangle \eta, f.x.\ e \rrangle
|
Notation for a closure.
|
|
$\Sigma^\omega$
|
\Sigma^\omega
|
The set of all behaviours.
|
|
$\mathbf{1}$
|
\mathbf{1}
|
The unit type.
|
|
$\texttt{()}$
|
\texttt{()}
|
Only inhabitant of the unit type.
|
|
$\simeq$
|
\simeq
|
Type isomorphism.
|
|
$+$
|
+
|
Addition or a sum type.
|
|
$\mathsf{fst}$
|
\mathsf{fst}
|
The first elimination form for a product type.
|
|
$\mathsf{snd}$
|
\mathsf{snd}
|
The second elimination form for a product type.
|
|
$\mathsf{InL}$
|
\mathsf{InL}
|
The first introduction form for a sum type.
|
|
$\mathsf{InR}$
|
\mathsf{InR}
|
The second introduction form for a sum type.
|
|
$\mathbf{0}$
|
\mathbf{0}
|
The empty type, the type with no inhabitants.
|
|
$\mathbf{rec}\ t.\ \tau$
|
\mathbf{rec}\ t.\ \tau
|
A recursive type.
|
|
$\mathbf{type}\ a.\ e$
|
\mathbf{type}\ a.\ e
|
Our notation for type abstraction.
|
|
$\mu a.\ e$
|
\mu a.\ e
|
The literature's notation for recursive types.
|
|
$\Lambda a.\ e$
|
\Lambda a.\ e
|
The literature's notation for type abstraction.
|
|
$@$
|
@
|
Our notation for type application
|
|
$\sqsubseteq$
|
\sqsubseteq
|
$\tau \sqsubseteq \rho$ iff $\rho$ is more general than $\tau$. Also can mean refinement.
|
|
$\sim$
|
\sim
|
Often used to denote unification problems.
|
|
$\tau \stackrel{U}{\sim} \rho$
|
\tau \stackrel{U}{\sim} \rho
|
The unification of $\tau$ and $\rho$, producing unifier $U$.
|
|
$\mathrm{FV}(t)$
|
\mathrm{FV}(t)
|
The set of free variables in a term.
|
|
$\mathsf{roll}$
|
\mathsf{roll}
|
The introduction form for a recursive type.
|
|
$\mathsf{unroll}$
|
\mathsf{unroll}
|
The elimination form for a recursive type.
|
|
$\mathsf{pack}$
|
\mathsf{pack}
|
The introduction form for an existential type.
|
|
$\mathsf{open}$
|
\mathsf{open}
|
The elimination form for an existential type.
|
|
$\leq$
|
\leq
|
A partial order. Often refers to subtyping.
|
|
$\Vdash$
|
\Vdash
|
Showing that an instance constraint is satsfiable from the set of known class instances.
|