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.