Back to COMP3161

COMP3161 Glossary

Notation|Terms Alphabetically |Terms By Week

$\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.
$\multimap$ \multimap A linear implication in Linear Logic. $A \multimap B$ says that "$A$ can be transformed into $B$".
$\otimes$ \otimes A linear conjunction in Linear Logic. $A \otimes B$ says "you've got both $A$ and $B$".
$\oplus$ \oplus A type of linear disjunction in Linear Logic. $A \oplus B$ says "you've got either $A$ or $B$, you don't get to choose."
$\text{&}$ \text{\&} Another Linear Logic connective. $A\ \text{&}\ B$ says that "you can choose either $A$ or $B$."
$!$ ! In Linear Logic, indicates "an unlimited amount", e.g. $!A$ means an unlimited amount of $A$. In uniqueness types, can refer to an observer.
$\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.
$[\![ \cdot ]\!]_\mathcal{W}$ \llbracket \rrbracket_\mathcal{W} Notation for work cost.
$[\![ \cdot ]\!]_\mathcal{D}$ \llbracket \rrbracket_\mathcal{D} Notation for depth cost.
$\Vdash$ \Vdash Showing that an instance constraint is satsfiable from the set of known class instances.