|
antisymmetric
|
A property of a relation $R$ where $a\ R\ b$ and $b\ R\ a$ implies $a = b$.
|
|
|
bijection
|
An injective and surjective mapping between two sets.
|
|
|
binary operator
|
A function on a set $A$ that takes two elements of $A$ and produces an element of $A$. Examples: addition, multiplication, subtraction, division, implication, conjunction, disjunction.
|
|
|
boolean
|
The set containing $\{ \top, \bot \}$.
|
|
|
cartesian product
|
The set $A \times B$ contains sets of pairs $\{ (a, b)\ |\ a \in A \land b \in B \}$.
|
|
|
codomain
|
The output set of a function.
|
|
|
commutativity
|
A property of an operator (here written $\cdot$) where $A \cdot B = B \cdot A$. Allows us to move terms around at will. Examples: addition, multiplication.
|
|
|
conjunction
|
The "and" operator $A \land B$.
|
|
|
constructive
|
A property of a logic or proof that indicates it does not make use of the law of the excluded middle.
|
|
|
contradiction
|
The simultaneous derivation of both $A$ and $\neg A$.
|
|
|
de Morgan's law
|
The laws that $\neg (A \lor B) = \neg A \land \neg B$ and that $\neg (A \land B) = \neg A \lor \neg B$.
|
|
|
disjunction
|
The "or" operator $A \lor B$.
|
|
|
domain
|
The input set of a function.
|
|
|
double-negation elimination
|
The logical principle that $\neg \neg A \Rightarrow A$ for all $A$. Equivalent to excluded middle.
|
|
|
excluded middle
|
The logical principle that $A \lor \neg A$ for all $A$.
|
|
|
expression
|
A term in a recursively-defined object language.
|
|
|
first-order logic
|
A form of logic with quantifiers over some arbitrary set of individuals.
|
|
|
function
|
A mapping $A \rightarrow B$ from a domain set $A$ to a codomain or range set $B$. For each element of $A$ there should be one corresponding element of $B$. Functions that may not have a $B$ for each $A$ are called partial functions.
|
|
|
halting problem
|
The famous problem that cannot be computed by any Turing-complete system: To determine if a given program will halt.
|
|
|
hardware transactional memory
|
A hardware-supported implementation of transactional memory.
|
|
|
if and only if
|
$A$ if and only if $B$ is the same as $(A \Rightarrow B) \land (B \Rightarrow A)$.
|
|
|
implication
|
The "if-then" operator $A \Rightarrow B$. Sometimes written $A \supset B$. It holds unless $A$ is true and $B$ is false.
|
|
|
inconsistent
|
A logic that allows both $P$ and $\neg P$ to be proven for some $P$.
|
|
|
injective
|
A mapping from set $A$ to set $B$ is injective if each different element in $A$ has a different corresponding element in $B$.
|
|
|
inlining
|
The optimisation that removes costly jumps by copying the code from a function into its call sites.
|
|
|
integer
|
A whole number: positive, zero or negative.
|
|
|
intersection
|
The intersection of sets $A \cap B$ is the set of elements common to both $A$ and $B$.
|
|
|
Java
|
A programming language you may have used.
|
|
|
left-identity
|
A property of a binary operator (here written $\cdot$) and an identity element $X$ where $X \cdot A = A$ for all $A$.
|
|
|
modus ponens
|
The argument that if $A \Rightarrow B$ and $A$, then $B$. Also called implication elimination.
|
|
|
modus tollens
|
The argument that if $A \Rightarrow B$ and $\neg B$, then $\neg A$.
|
|
|
natural numbers
|
Whole numbers starting at 0 and going up.
|
|
|
negation
|
The "not" operator $\neg A$.
|
|
|
partial function
|
A function that is not defined for its whole domain.
|
|
|
partial order
|
A relation that is reflexive, transitive, and antisymmetric.
|
|
|
predicate
|
A logical property that is parameterised by a mathematical object. Equivalently a function from some set to booleans.
|
|
|
proof assistant
|
A tool for interactively proving theorems in a formal logic, such as Isabelle, Coq, or Agda.
|
|
|
proof by contradiction
|
The process of proof whereby the proof obligation is assumed to be false, and a contradiction is derived. Depends on excluded middle.
|
|
|
proof obligation
|
A judgement that we wish to prove, or must prove in order to establish our ultimate proof goal.
|
|
|
proposition
|
A logical statement. See judgement.
|
|
|
quantifier
|
The operators $\forall$ and $\exists$.
|
|
|
range
|
See codomain.
|
|
|
reflexive
|
A property of a relation $R$ that $a\ R\ a$ for all $a$.
|
|
|
relation
|
A judgement that operates on more than one object, i.e. its arity is greater than 1.
|
|
|
right-identity
|
A property of a binary operator (here written $\cdot$) and an identity element $X$ where $A \cdot X = A$ for all $A$
|
|
|
specification
|
A mathematical description of the desired properties of a program or software system.
|
|
|
strict subset
|
A set $A$ is a strict subset of a set $B$, written $A \subset B$, if $A$ is a subset of $B$ which is also not equal to $B$.
|
|
|
strict superset
|
A set $A$ is a strict superset of another set $B$ if $B$ is a strict subset of $A$.
|
|
|
subset
|
A set $A$ is a subset of a set $B$, written $A \subseteq B$ if every element of $A$ is also an element of $B$.
|
|
|
superset
|
$A$ is a superset of $B$ if and only if $B$ is a subset of $A$.
|
|
|
surjective
|
A mapping from set $A$ to set $B$ is surjective if each element of $B$ has some element of $A$ that maps to it.
|
|
|
symmetric
|
A property of a relation $R$ where $a\ R\ b$ implies $b\ R\ a$ for all $a$ and $b$.
|
|
|
tautology
|
A logical property that is self-evidently true, for example $A \Rightarrow A$.
|
|
|
transitive
|
A property of a relation $R$ where $a\ R\ b$ and $b\ R\ c$ implies $a\ R\ c$ for all $a$, $b$, and $c$.
|
|
|
Turing-complete
|
A property of a language that means that it is capable of performing any decidable computation in finite time.
|
|
|
union
|
The union of a set $A \cup B$ is the set containing all elements of $A$ and all the elements of $B$.
|
|
|
abstract syntax
|
A representation of a language's syntax with no ambiguity, and with superfluous information removed. Usually represented as a tree data structure rather than a list of characters or tokens.
|
1
2
|
|
Backus-Naur Form
|
A compact recursive notation used to describe a language's grammar. For example, $M ::= \epsilon\ \vert\ \texttt{(} M \texttt{)}\ \vert\ M M$ is the language of matching parentheses.
|
1
|
|
code generator
|
The final phase of a compiler, which produces appropriate code in a lower-level language such as machine code.
|
1
|
|
compiler
|
A program which, given program source code, translates the program into a lower-level language, usually machine code. Consists of a lexer, parser, semantic analyser, code generator and sometimes an optimiser.
|
1
|
|
cons
|
The non-empty list, consisting of a head element and a tail list
|
1
|
|
cost model
|
A type of dynamic semantics where the goal is not to describe the actual run-time behaviour (e.g. results returned) but instead to mathematically describe the computational resources used (e.g. for computational complexity) .
|
1
5
|
|
data constructor
|
The function provided by a data definition in Haskell that creates a new value of a particular type.
|
1
|
|
domain-specific language
|
A language designed for a particular purpose, may not be Turing-complete.
|
1
|
|
dynamic
|
Refers to run-time properties or behaviour, as opposed to static properties or behaviour.
|
1
|
|
dynamic semantics
|
Mathematical description of a language's run-time behaviour. Cost models are also considered a type of dynamic semantics.
|
1
3
|
|
grammar
|
The rules that describe how the parser may recognize a language's syntax. Consists of a family of recursive productions, often specified in Backus-Naur Form
|
1
2
|
|
Haskell
|
A neat programming language.
|
1
|
|
head
|
The element at the start of a non-empty list.
|
1
|
|
identifier
|
An alphabetical (or alphanumeric) lexeme in a language's syntax, which could stand for e.g. a variable, function or type name.
|
1
|
|
intermediate representation
|
A language used internally within a compiler or interpreter to make certain manipulations or optimisations simpler.
|
1
|
|
interpreter
|
A program which directly executes a program from source code given as input.
|
1
|
|
keyword
|
Reserved words used in a language to represent built in constructs, e.g. if, then, let etc. in Haskell.
|
1
|
|
lexeme
|
See token.
|
1
|
|
lexer
|
The first phase of a compiler or interpreter which converts source code to a sequence of tokens.
|
1
|
|
literal
|
A lexeme in a language's syntax that represents a single value, e.g. 3 or True or "Hello" in Haskell.
|
1
|
|
nil
|
The empty list.
|
1
|
|
non-terminal
|
A class of expressions that denotes a subset of a language, which is itself defined by a production elsewhere in a grammar.
|
1
|
|
optimiser
|
The fourth phase of a compiler or interpreter that will transform the abstract syntax, optionally using intermediate representations, to improve performance of a piece of code.
|
1
|
|
parse tree
|
A tree that contains a representation of the grammatical structure recognized for a particular program by the parser. Often this is the same as the abstract syntax tree.
|
1
2
|
|
parser
|
The second phase of a compiler or interpreter which converts the sequence of tokens from the lexer to a parse tree according to the grammar rules of the language's syntax.
|
1
2
|
|
production
|
A syntax production describes how to recognize a non-terminal as a sequence of terminals and other non-terminals.
|
1
|
|
scope checking
|
See scope resolution.
|
1
2
|
|
scope resolution
|
The process by which variables and other references in a program are checked to see if they refer to objects that have been defined previously. Finds the correct binding occurrence for each usage occurrence of a variable.
|
1
2
|
|
semantic analyser
|
The third phase of a compiler or interpreter which performs analysis on the abstract syntax tree to determine the static semantics of the input program.
|
1
|
|
semantics
|
The mathematical meaning of a program, in the form of dynamic semantics or static semantics.
|
1
3
|
|
source code
|
The code written by the programmer in their text editor.
|
1
|
|
static
|
Refers to properties or behaviour of programs that can be determined without running them, for example at compile-time.
|
1
|
|
static semantics
|
Mathematical description of the aspects of a program that can be determined statically.
|
1
3
|
|
syntax
|
The rules of the language that describe how the language is written (e.g. according to a grammar), rather than what it means (semantics).
|
1
2
2
|
|
tail
|
The rest of a non-empty list after the head.
|
1
|
|
terminal
|
A raw lexeme that is is recognised as-is in a language's grammar.
|
1
|
|
token
|
A single "word" in a programming language's syntax, e.g. a keyword, an identifier, or a literal. Also called a lexeme.
|
1
|
|
type
|
A type is a static tag that classifies expressions according to the sort of values they will evaluate to.
|
1
7
|
|
type checking
|
The process by which the semantic analyser of a compiler establishes that a program is well-typed (or not!).
|
1
7
|
|
virtual machine
|
In a programming languages context, a virtual machine refers to an interpreter for a fairly high-level abstract machine architecture that allows for cross-platform language implementation.
|
1
|
|
abstract syntax
|
A representation of a language's syntax with no ambiguity, and with superfluous information removed. Usually represented as a tree data structure rather than a list of characters or tokens.
|
1
2
|
|
abstraction
|
A form of term that introduces a new bound variable in higher-order abstract syntax, see λ-abstraction. Also can refer to the general notion of removing detail from a specification of a program.
|
2
|
|
admissible
|
An inference rule is admissible to a language $L$ if adding the rule to the language definition does not change $L$.
|
2
|
|
ambiguity
|
A language $L$ is ambiguous if there exists a string $s$ that can be proven to be part of $L$ in two or more ways.
|
2
|
|
associativity
|
A property of an operator (here written $\cdot$) where $A \cdot B \cdot C = A \cdot (B \cdot C) = (A \cdot B) \cdot C$. Allows us to rearrange parentheses at will. Examples: addition, multiplication.
|
2
|
|
axiom
|
An inference rule with no premises. Always holds.
|
2
|
|
base case
|
An elementary proof case that is derived from an axiom in an inductive proof.
|
2
|
|
binder
|
An expression that contains the binding occurrence of a variable, for example let expressions.
|
2
|
|
binding occurrence
|
The use of a variable name that defines it, or gives it its value. For example, in λ-abstractions or let expressions.
|
2
|
|
bound
|
A variable is bound in an expression $e$ if it is defined or introduced in the expression $e$, i.e. its binding occurrence is in $e$.
|
2
|
|
capture
|
The problem that arises in a substitution $e[x:=t]$ whenever a variable that appears in $t$ is also bound in $e$. For example let x = 5 in y + 1 applying the substitution $[y := x]$.
|
2
|
|
conclusion
|
The judgement that is proven by a particular inference rule.
|
2
|
|
concrete syntax
|
A representation of a language's syntax that corresponds closely to what the programmer would write in their editor, as opposed to abstract syntax which is an unambiguous tree representation.
|
2
|
|
de Bruijn indices
|
The means of representing abstract syntax where variable names are replaced with numbers that indicate how many binders to skip over, radiating out from the usage of the variable. For example let x = 3 in let y = 2 in x + y becomes let 3 in let 2 in (Var 1) + (Var 0).
|
2
|
|
declaration
|
See binding occurrence.
|
2
|
|
derivable
|
An inference rule is derivable from a language $L$ if the rule can be expressed as the composition of the existing rules for $L$. That is, starting from the premises of the rule, if the other rules in $L$ can be used to derive the conclusion of the rule, then the rule is derivable.
|
2
|
|
elimination
|
The inference rule in a logic that allows an assumption to be broken down into its component assumptions. Also the corresponding expression in a programming language that allows the components of a structure to be accessed.
|
2
|
|
equivalence
|
A type of relation that is reflexive, transitive, and symmetric.
|
2
|
|
ex falso quodlibet
|
The logical principle that $\bot \Rightarrow A$ for any $A$ --- from false, you can derive anything.
|
2
|
|
first-order abstract syntax
|
A means of representing abstract syntax which does not identify α-equivalent terms, as opposed to higher-order abstract syntax.
|
2
|
|
formalisation
|
The act of giving a mathematical description to something.
|
2
|
|
free
|
A variable is free in an expression if it is not bound in that expression.
|
2
|
|
grammar
|
The rules that describe how the parser may recognize a language's syntax. Consists of a family of recursive productions, often specified in Backus-Naur Form
|
1
2
|
|
higher-order abstract syntax
|
The means of representing abstract syntax by re-using the binding and variable mechanisms of the meta-language.
|
2
|
|
holds
|
A judgement is said to hold if a proof for it can be established.
|
2
|
|
hypothetical derivation
|
An inference rule which occurs as a premise to another inference rule.
|
2
|
|
induction
|
A process of proof whereby a property is shown for elemental base cases, and then, assuming premises called inductive hypotheses, the property is shown for inductive cases, thereby proving the property for all of an inductive set.
|
2
|
|
inductive case
|
A proof case that is derived from a (non-axiom) inference rule in an inductive proof, with one or more inductive hypotheses taken as assumptions.
|
2
|
|
inductive definition
|
A set of inference rules that is describes a language or judgement completely. That is, the rules prove the judgement, and if the judgement holds then it must be via one of those rules.
|
2
|
|
inductive hypothesis
|
An assumption derived from a premise of the inference rule for a particular inductive cases of an inductive proof.
|
2
|
|
inference rule
|
A rule, written $\frac{J_1 \quad J_2 \quad \dots \quad J_n}{J}$, which states that in order to prove judgement $J$,
it suffices to prove judgements $J_1$ through to $J_n$.
|
2
|
|
introduction
|
The inference rule in a logic that allows a logical operator to be introduced to the proven formula. Analogous
to a data constructor in a programming language.
|
2
|
|
judgement
|
A mathematical statement. To prove a judgement, we may derive it using inference rules.
|
2
|
|
left-associativity
|
A property of a binary operator (here written $\cdot$) where $A \cdot B \cdot C = (A \cdot B) \cdot C$. Examples: subtraction, division.
|
2
|
|
lemma
|
An intermediate theorem that is proven in order to prove a larger theorem.
|
2
|
|
logic
|
A formalised system of reasoning. Typically described using a meta-logic.
|
2
|
|
meta-language
|
The language within which another language is described. In this course, we use Haskell as a meta-language in the assignments, and a meta-logic as our meta-language in the mathematical work.
|
2
|
|
meta-logic
|
A bare-bones logical system designed to specify another logic or programming language. In this course we use Natural Deduction.
|
2
|
|
Natural Deduction
|
A system of reasoning whereby proofs are established by the formal use of inference rules, terminating in axioms.
|
2
|
|
out of scope
|
An error that is raised when a variable is encountered in a usage occurrence without a matching binding occurrence.
|
2
|
|
parse tree
|
A tree that contains a representation of the grammatical structure recognized for a particular program by the parser. Often this is the same as the abstract syntax tree.
|
1
2
|
|
parser
|
The second phase of a compiler or interpreter which converts the sequence of tokens from the lexer to a parse tree according to the grammar rules of the language's syntax.
|
1
2
|
|
parsing
|
The relation $\longleftrightarrow$ that relates concrete to abstract syntax.
|
2
|
|
premise
|
A judgement that must be proven in order to prove the conclusion of an inference rule.
|
2
|
|
pretty-printing
|
A process to transform abstract syntax back into concrete syntax by going right to left on the parsing relation.
|
2
|
|
proof calculus
|
A set of inference rules to describe a logic or reasoning system.
|
2
4
|
|
right-associativity
|
A property of a binary operator (here written $\cdot$) where $A \cdot B \cdot C = A \cdot (B \cdot C)$. Examples: implication, the function arrow in Haskell.
|
2
|
|
rule induction
|
The process whereby induction is performed according to the set of inference rules that form an inductive definition for a particular judgement that occurs as a premise of the desired proof obligation.
|
2
|
|
s-expressions
|
A particular type of term language where terms are either identifiers or parenthesised compounds consisting of one or more subterms.
|
2
|
|
scope
|
The (sub)-expressions in which a variable is bound.
|
2
|
|
scope checking
|
See scope resolution.
|
1
2
|
|
scope resolution
|
The process by which variables and other references in a program are checked to see if they refer to objects that have been defined previously. Finds the correct binding occurrence for each usage occurrence of a variable.
|
1
2
|
|
shadowing
|
The situation where a variable that is already in scope is bound. For example let x = 5 in let x = 2 in x + x end end.
|
2
|
|
simultaneous induction
|
The process of treating multiple judgements as part of one large inductive definition for the purposes of induction.
|
2
3
|
|
stack
|
A list-like data structure which consists of an operation to push on items, and pop items off, in Last-In-First-Out order.
|
2
5
|
|
structural induction
|
A form of rule induction where the rules being used define the structure (type) of a particular variable.
|
2
|
|
substitution
|
Written $e[x:=t]$ or $e[{}^t/_x]$, means the replacement of all free usage occurrences of $x$ with $t$ in $e$.
|
2
|
|
syntax
|
The rules of the language that describe how the language is written (e.g. according to a grammar), rather than what it means (semantics).
|
1
2
2
|
|
syntax
|
The rules of the language that describe how the language is written (e.g. according to a grammar), rather than what it means (semantics).
|
1
2
2
|
|
term
|
An expression in a minimal language used in the meta-logic to describe syntax trees. Can also be used
in general to mean expression.
|
2
|
|
theorem
|
A judgement or proposition that has been proven.
|
2
|
|
unambiguous
|
The absence of ambiguity.
|
2
3
|
|
unparsing
|
See pretty-printing.
|
2
|
|
up-shifting
|
The process of incrementing de Bruijn indices to accommodate new variables introduced into scope.
|
2
|
|
usage occurrence
|
The mention of a variable name where it is being used. Its binder will occur elsewhere.
|
2
|
|
variable
|
A symbol or name that stands for a value, either in a programming language or mathematical formula.
|
2
|
|
well-scoped
|
A program is well-scoped if it does not contain any out of scope errors.
|
2
|
|
α-equivalence
|
Two terms are α-equivalent if they differ only in bound variable names. An equivalence relation.
|
2
|
|
α-rename
|
The process of changing variable names that preserves α-equivalence.
|
2
|
|
application
|
A function being "called", i.e. given arguments to produce its result. An application is written $e_1\ e_2$, where the expression $e_1$ denotes a function and $e_2$ denotes the argument being passed to that function.
|
3
|
|
arity
|
Number of objects on which a function, relation or judgement operates.
|
3
|
|
axiomatic semantics
|
The specification of a language's dynamic semantics via the construction of a proof calculus to
allow correctness of a program to be verified.
|
3
|
|
big-step semantics
|
The specification of evaluation in dynamic semantics according to a relation $\Downarrow \subseteq E \times V$ where $E$ is the set of evaluable expressions and $V$ is the set of values.
|
3
|
|
call-by-name
|
The evaluation strategy where β-reduction is evaluated before function arguments. Can be computationally expensive.
|
3
|
|
call-by-need
|
An evaluation strategy that depends on graph reduction that effectively optimises call-by-name execution to be computationally inexpensive.
|
3
|
|
call-by-value
|
An evaluation strategy where function arguments are evaluated before β-reduction. Also called strict evaluation.
|
3
|
|
complete execution
|
An execution that is maximal and ends in a final state.
|
3
|
|
completed trace
|
See complete execution.
|
3
|
|
compositional
|
A general mathematical adjective that says that a mathematical object can be constructed by the combination of other objects, regardless of those objects' particular characteristics.
|
3
|
|
confluence
|
Property of a reduction that states that a term $A$ can be reduced in one way to $B$ and in another way to $C$, then $B$ and $C$ must both be reducible to a common term $D$.
|
3
|
|
congruence
|
Property of a reduction that states that the reduction can be applied to any reducible subexpression of a larger overall expression.
|
3
|
|
context
|
Usually written $\Gamma$, indicates a set of judgements that are assumed in a derivation. In type systems, usually is a mapping from variable name to type. Also can refer to an environment in dynamic semantics. Can be viewed as hypothetical derivation.
|
3
|
|
denotational semantics
|
The compositional construction of a language's dynamic semantics by mapping each form of syntax to a mathematical object. Usually written with $[\![\cdot]\!]$ brackets.
|
3
|
|
dynamic semantics
|
Mathematical description of a language's run-time behaviour. Cost models are also considered a type of dynamic semantics.
|
1
3
|
|
effects
|
Observable phenomena from a program, for example input/output, or reading from and writing to memory.
|
3
9
|
|
environment
|
A mapping from variables to their values.
|
3
5
|
|
evaluation
|
To determine the result of a particular expression. See big-step semantics.
|
3
|
|
evaluation semantics
|
See big-step semantics.
|
3
|
|
evaluation strategy
|
The order in which reductions are chosen in a dynamic semantics.
|
3
|
|
execution
|
The sequence of states arising from the repeated application of the transition relation from an initial state in a small-step semantics. May or may not end in a final state.
|
3
|
|
final state
|
The states in a state machine that are considered successful termination.
|
3
|
|
higher-order logic
|
A logic based on λ-calculus used as the foundation for various proof assistants.
|
3
|
|
initial state
|
The states in which a state machine may begin execution.
|
3
|
|
irreducible
|
A term is irreducible if no reduction may be applied to it.
|
3
|
|
lazy evaluation
|
See call-by-need evaluation.
|
3
|
|
maximal
|
A trace or execution $\sigma_1 \dots \sigma_n$ is maximal if and only if there is no $\sigma_{n+1}$ such that the $\sigma_n \mapsto \sigma_{n+1}$ according to the transition relation.
|
3
|
|
n-ary
|
A term indicating that the arity of a relation or other object goes up to an arbitrary $n$.
|
3
|
|
natural semantics
|
See big-step semantics.
|
3
|
|
non-deterministic
|
A property of an algorithm where multiple results or states are possible from a given input or starting state.
|
3
|
|
normal form
|
A form of expression that is irreducible. Opposite of a redex.
|
3
|
|
operational semantics
|
The specification of a language's dynamic semantics by constructing a program-evaluating state machine or transition system.
|
3
|
|
redex
|
An expression that is reducible.
|
3
|
|
reducible
|
A property of an expression that says that a reduction may be applied.
|
3
|
|
reduction
|
A rule that states that an expression can be rewritten to another (usually simpler) expression. See β-reduction for an example.
|
3
|
|
reflexive transitive closure
|
The minimal extension to a relation such that it becomes reflexive and transitive. For $\mapsto$, often written as $\stackrel{\star}{\mapsto}$.
|
3
|
|
semantics
|
The mathematical meaning of a program, in the form of dynamic semantics or static semantics.
|
1
3
|
|
simultaneous induction
|
The process of treating multiple judgements as part of one large inductive definition for the purposes of induction.
|
2
3
|
|
small-step semantics
|
A means of specifying a language's dynamic semantics as the execution of a state machine, consisting of a set of initial states $I \subseteq \Sigma$, a set of final states $F \subseteq \Sigma$, and a transition relation $\mapsto \subseteq \Sigma \times \Sigma$ from state to state.
|
3
|
|
state
|
All the information required to evaluate a program at one step in its execution. For example, would include the values of all variables.
|
3
|
|
state machine
|
A mathematical formalism consisting of a set of states $\Sigma$, sets of initial and final states $I$ and $F$, and a transition relation $\mapsto \subseteq \Sigma \times \Sigma$.
|
3
|
|
static semantics
|
Mathematical description of the aspects of a program that can be determined statically.
|
1
3
|
|
strict evaluation
|
See call-by-value.
|
3
|
|
structural operational semantics
|
See small-step semantics.
|
3
|
|
termination
|
A property that states that a program halts in a final state after a finite amount of steps, i.e. that all maximal traces are finite completed traces.
|
3
|
|
trace
|
See execution.
|
3
|
|
transition relation
|
The relation $\mapsto$ in small-step semantics.
|
3
|
|
transition system
|
See state machine.
|
3
|
|
type theory
|
A logic based on typed λ-calculus and the Curry-Howard correspondence, used as the foundation for many constructive proof assistants.
|
3
7
|
|
unambiguous
|
The absence of ambiguity.
|
2
3
|
|
value
|
The result of evaluation.
|
3
|
|
αβ-equivalence
|
The equivalence relation that equates any terms that have α-equivalent normal forms using only β-reduction.
|
3
|
|
αβη-equivalence
|
The equivalence relation that equates any terms that have α-equivalent normal forms using both β-reduction and η-conversion.
|
3
|
|
β-reduction
|
The reduction that states that a λ-term like $(\lambda x.\ t)\ s$ can be rewritten to $t[x := s]$.
|
3
|
|
η-conversion
|
The reduction that states that a λ-term like $\lambda x.\ f\ x$ can be rewritten to just $f$.
|
3
|
|
λ-abstraction
|
Written $\lambda x.\ t$, denotes a function from an argument $x$ to a body $t$.
|
3
|
|
λ-calculus
|
A language containing only λ-abstractions, application and variables, that is Turing-complete.
|
3
|
|
λ-term
|
A term in λ-calculus.
|
3
|
|
assembly language
|
A type of imperative language where each command corresponds to exactly one machine instruction.
|
4
|
|
assertion
|
A logical proposition that may involve variables from a program's mutable state.
|
4
|
|
assignment
|
A statement $x := e$ that updates the mutable variable $x$ to have the value resulting from $e$.
|
4
|
|
control structure
|
A syntactic construct to encapsulate some common pattern of control flow in an imperative language, such as a while loop or an if statement.
|
4
|
|
Dijkstra
|
A famous computer scientist.
|
4
|
|
formal verification
|
The process of proving that a program is correct by appeal to its semantics, usually axiomatic semantics.
|
4
|
|
functional programming
|
A functional programming language is a programming language
derived from or inspired by the λ-calculus, or derived from or
inspired by another functional programming language.
|
4
|
|
Hoare logic
|
An axiomatic semantics, or proof calculus for establishing partial correctness of a program by proving Hoare triple judgements.
|
4
|
|
Hoare triple
|
A judgement written $\{ \phi \} s \{ \psi \}$ which states that if the program $s$ starts in a state where the precondition $\phi$ holds, then if $s$ evaluates to a final state, the postcondition $\psi$ will hold for that state.
|
4
|
|
imperative programming
|
Where programs are described as a
series of statements or commands which manipulate mutable state or
cause externally observable effects
|
4
|
|
initialized
|
A property of a mutable variable that indicates it has been assigned a value after being declared.
|
4
|
|
loop invariant
|
An assertion that must be maintained by a loop in order to apply the rule in Hoare logic for loops.
|
4
|
|
MinHS
|
A minimal functional programming language (that is purely functional) we specified in Week 5.
|
4
|
|
mutable
|
An adjective that indicates that it may change over time, e.g. in the course of an execution.
|
4
9
|
|
partial correctness
|
The property that says if a program evaluates from an initial state which satisfies the precondition, then any final state it reaches will satisfy the postcondition. As opposed to total correctness which requires that a final state is reached.
|
4
|
|
postcondition
|
An assertion that will be satisfied by a program's final state if the precondition held for the initial state.
|
4
|
|
precondition
|
An assertion that must be satisfied by the initial state in order for the program's specification to apply.
|
4
|
|
proof calculus
|
A set of inference rules to describe a logic or reasoning system.
|
2
4
|
|
purely functional
|
A programming language is purely functional if β-reduction (or
evaluation in general) is actually a confluence.
In other words, functions have to be mathematical functions, and
free of side effects.
|
4
|
|
rule of consequence
|
The rule in Hoare logic that allows us to use logical implication to simplify assertions.
|
4
|
|
sequential composition
|
A fancy term for the semicolon operator in TinyImp, i.e. $s_1 ; s_2$ which runs $s_2$ after $s_1$.
|
4
|
|
side effects
|
Side effects refers to effects that are not tracked by the type system.
|
4
|
|
structured programming
|
A movement in the 1970s, headed by Edsger Dijkstra, to promote the use of control structures to aid in formal reasoning, in particular things like Hoare logic.
|
4
|
|
TinyImp
|
An imperative programming language we specify in Week 5.
|
4
|
|
total correctness
|
The combination of partial correctness and termination.
|
4
|
|
uninitialized
|
The opposite of initialized.
|
4
|
|
algebraic data type
|
A type comprised of sum types and product types.
|
7
|
|
behaviour
|
An infinite sequence of states, a generalised notion of a trace.
|
7
|
|
checked exceptions
|
A form of exceptions where the possibility of a raise is tracked in the type system.
|
7
|
|
commutative semiring
|
An algebraic structure consisting of a set $U$ and two operators $+$ and $\times$, with two identity elements $0 \in U$ and $1 \in U$ that behave analogously to the natural numbers in terms of associativity, commutativity, left and right-identity.
|
7
|
|
Curry-Howard correspondence
|
The correspondence between programs and proofs, types and propositions, and evaluation to proof simplification.
|
7
|
|
dynamic types
|
See unityped.
|
7
|
|
exception
|
A value that is passed to an exception handler when control flow is interrupted by a raise invocation.
|
7
|
|
exception handler
|
An expression that is evaluated in the event that an exception is raised.
|
7
|
|
inhabitant
|
A value $v$ is an inhabitant of a type $\tau$ if $v : \tau$.
|
7
|
|
isomorphic
|
Two types are isomorphic, written $\tau_1 \simeq \tau_2$, if and only if there exists a bijection between them. Typically, this is if they have the same number of inhabitants.
|
7
|
|
liveness
|
A type of property that states that something good will happen eventually. Cannot be refuted by a finite prefix of a
behaviour, as the good thing could always happen later. For example: confluence, termination.
|
7
|
|
monad
|
A convenient abstraction in Haskell, allows for the simulation of mutable state, exceptions and much more.
|
7
9
|
|
preservation
|
A lemma needed to prove type safety which states that if a program $e$ has type $\tau$, i.e. $e : \tau$, and $e$ takes a step to $e'$, then $e' : \tau$.
|
7
|
|
product type
|
A product type, written $\tau_1 \times \tau_2$, denotes the type of pairs or tuples of values of type $\tau_1$ and of $\tau_2$ respectively. Analogous to the cartesian product in set theory, and to conjunction via the Curry-Howard correspondence.
|
7
|
|
progress
|
The lemma that if an expression $e$ has type $\tau$, i.e. $e : \tau$ then either $e$ is a final state or $e$ can take a step to some state $e'$. Proves type safety along with preservation.
|
7
|
|
property
|
A set of a program's behaviours. Often informally described as an English statement about a program's behaviour.
|
7
|
|
raise
|
An expression that interrupts control flow, passing an exception to an exception handler. Also sometimes called a throw.
|
7
|
|
recursive type
|
A type that includes a recursive reference to itself, for example the type of linked lists.
|
7
|
|
safety
|
A type of property that states that something bad will not happen. Can be refuted by a finite prefix of a behaviour. For example, type safety, partial correctness.
|
7
|
|
strong normalisation
|
A property of typed λ-calculus that states that any expression will reduce to a normal form in finite time. This makes typed λ-calculus not Turing-complete, but suitable for a foundation for logic.
|
7
|
|
stuck state
|
A state that is not a final state but has no outgoing transitions in the transition relation.
|
7
|
|
subject reduction
|
A property of typed λ-calculus that states that the normal form of a term will have the same type as that term.
|
7
|
|
sum type
|
The sum type, written $\tau_1 + \tau_2$, denotes either a value of type $\tau_1$ or a value of type $\tau_2$, distinguished by a data constructor. Analogous to disjunction in logic via the Curry-Howard correspondence, the disjoint union in set theory, or the Either type in Haskell.
|
7
|
|
throw
|
See raise.
|
7
|
|
type
|
A type is a static tag that classifies expressions according to the sort of values they will evaluate to.
|
1
7
|
|
type checking
|
The process by which the semantic analyser of a compiler establishes that a program is well-typed (or not!).
|
1
7
|
|
type safety
|
The safety property that states that well-typed programs do not reach a stuck state. Usually proven via progress and preservation.
|
7
|
|
type system
|
A formal scheme of assigning types to expressions.
|
7
|
|
type theory
|
A logic based on typed λ-calculus and the Curry-Howard correspondence, used as the foundation for many constructive proof assistants.
|
3
7
|
|
typed λ-calculus
|
A variant of λ-calculus with a type system. Is not Turing-complete but enjoys strong normalisation and subject reduction.
|
7
|
|
unit type
|
The type with one inhabitant. Often written as () or $\mathbf{1}$.
|
7
|
|
unityped
|
A minimal type system which consists of only one type but ensures type safety through use of exceptions.
|
7
|
|
well-typed
|
Indicates that an expression $e$ can be proven to have some type $\tau$, i.e. $e : \tau$.
|
7
|
|
boxing
|
A means of implementing parametric polymorphism where all objects are stored on the stack uniformly as a pointer to a heap object.
|
8
|
|
constraint-based type inference
|
A method of type inference that casts the problem in constraint-satisfaction terms.
|
8
|
|
generalisation
|
The process of taking a type involving schematic variables and explicitly quantifying them with $\forall$.
|
8
|
|
generics
|
See parametric polymorphism.
|
8
|
|
Hindley-Milner restriction
|
Only allows type abstraction on the top level, not nested inside a function's definition or inside a data structure, and disallows polymorphic recursion. Makes type inference tractable.
|
8
|
|
implicitly-typed
|
Describes a language with no type annotations.
|
8
|
|
instantiation
|
The substitution of a type variable to a concrete type.
|
8
|
|
mgu
|
most general unifier.
|
8
|
|
monomorphic
|
Refers to something that is not polymorphic.
|
8
|
|
more general
|
A type $\tau$ is more general than a type $\rho$, written $\rho \sqsubset \tau$, if a substitution can be made to polymorphic type variables in $\tau$ to give $\rho$.
|
8
|
|
most general unifier
|
A unifier $S$ is most general for types $\tau$ and $\rho$ iff $S(\tau) = S(\rho)$ is the most general type that could result from unification.
|
8
|
|
parametric polymorphism
|
A feature of a language which allows functions to be defined operating on arbitrary types using type abstraction and type application. Sometimes called generics in Java.
|
8
|
|
parametricity
|
See relational parametricity.
|
8
|
|
polymorphic recursion
|
A recursive, polymorphic program that calls itself with different type arguments on each recursive call.
|
8
|
|
polymorphism
|
Usually refers to parametric polymorphism, unless otherwise indicated.
|
8
9
|
|
relational parametricity
|
The theorem scheme developed by John C. Reynolds that allows us to infer properties from polymorphic type signatures.
|
8
|
|
schematic variable
|
See unification variable.
|
8
|
|
second-order logic
|
A form of logic where quantifiers range over propositions that can themselves include quantifiers.
|
8
|
|
syntax-directed
|
When a set of inference rules can correspond to an algorithm by following the structure of abstract syntax.
|
8
|
|
template instantiation
|
A means of compiling polymorphic programs by statically generating a monomorphic copy of each polymorphic function.
|
8
|
|
type abstraction
|
Written $\textbf{type}\ a. e$, indicates that the expression $e$ is parameterised by a type variable $a$.
|
8
|
|
type annotation
|
Some means of syntax for the programmer to specify types.
|
8
|
|
type application
|
Written $e@\tau$, instantiates the type variable in the type of $e$ to $\tau$.
|
8
|
|
type inference
|
The process of determining what type would make an expression well-typed, given an implicitly-typed language.
|
8
|
|
type variable
|
A variable that stands for a type, usually in the context of parametric polymorphism.
|
8
|
|
unification
|
A process whereby a substitution $S$ is found for two types involving unification variables, $\tau$ and $\rho$, such that $S(\tau) = S(\rho)$.
|
8
|
|
unification variable
|
A type variable that stands for an unknown type in type inference.
|
8
|
|
unifier
|
The substitution that results from unification.
|
8
|
|
universal quantification
|
The use of the $\forall x.\ P(x)$ "for all" operator. Used in logic and types for parametric polymorphism.
|
8
9
|
|
unknowns
|
Can refer to schematic variables in the context of type inference.
|
8
|
|
abstract data type
|
A type defined not by its internal representation but by the operations
that can be performed on it. Type-theoretically encoded as an existential type.
|
9
|
|
ad-hoc polymorphism
|
Referring to multiple different values by the same name, with the exact implementation chosen during type checking. Common implementations are based on type classes.
|
9
|
|
ADT
|
An abstract data type. Never refers to an algebraic data type.
|
9
|
|
class instance
|
A set of implementations of methods for a particular type class and type.
|
9
|
|
coercion
|
An injective mapping from a subtype to a supertype.
|
9
|
|
concurrency
|
An abstraction for the programmer, allowing programs to be structured as
multiple threads of control, called processes. They may communicate
in various ways.
|
9
10
|
|
contravariant
|
For a type constructor $C$, the variance where $\tau \leq \rho$ implies that $C\ \tau \geq C\ \rho$.
|
9
|
|
covariant
|
For a type constructor $C$, the variance where $\tau \leq \rho$ implies $C \tau \leq C \rho$.
|
9
|
|
dictionary
|
A value that contains all the implementations for a class instance of a type class. Typically class instances are compiled to these.
|
9
|
|
effects
|
Observable phenomena from a program, for example input/output, or reading from and writing to memory.
|
3
9
|
|
existential quantification
|
The use of the $\exists x.\ P(x)$ "there exists" operator. Can denote an existential type.
|
9
|
|
existential type
|
Written $\exists a.\ \tau$, denotes a type $\tau$, which may involve
some unknown type $a$. An abstract data type with operations $\tau$ on some type $a$.
|
9
|
|
heisenbug
|
A result of non-deterministic programs where adding instrumentation to debug a problem makes the problem go away.
|
9
|
|
instance constraint
|
A constraint on a type that a type class must have a class instance.
|
9
|
|
invariant
|
A variance which is neither covariant nor contravariant.
|
9
|
|
Liskov Substitution Principle
|
The principle that states: Let $\phi(x)$ be a property provable about objects $x$ of type $\rho$. Then $\phi(y)$ should be true for objects $y$ of type $\tau$ where $\tau \leq \rho$.
|
9
|
|
method
|
An overloaded variable name that must be implemented to create a class instance of a type class.
|
9
|
|
module
|
A value encapsulating an abstract data type, i.e. an existential type.
|
9
|
|
monad
|
A convenient abstraction in Haskell, allows for the simulation of mutable state, exceptions and much more.
|
7
9
|
|
mutable
|
An adjective that indicates that it may change over time, e.g. in the course of an execution.
|
4
9
|
|
orphan
|
A class instance that is defined separately to both the type class and the type.
|
9
|
|
overloading
|
See ad-hoc polymorphism.
|
9
|
|
parallelism
|
The simultaneous execution of code on multiple processors or cores for the purposes of improved performance.
|
9
|
|
polymorphism
|
Usually refers to parametric polymorphism, unless otherwise indicated.
|
8
9
|
|
process
|
A sequence of statements to execute that forms one thread of control in a concurrent application.
|
9
10
|
|
rule of subsumption
|
The rule that states any expression $e : \tau$ also has type $\rho$ if $\tau$ is a subtype of $\rho$.
|
9
|
|
signature
|
The type of a module.
|
9
|
|
subtyping
|
A partial order on types, written $\tau \leq \rho$. Always includes a
rule of subsumption in the type system.
|
9
|
|
synchronisation
|
Where multiple processes co-ordinate or communicate to give predictable outcomes.
|
9
10
|
|
thread
|
See process.
|
9
10
|
|
type class
|
A set of types that have provided implementations (class instances) for a set of overloaded functions (methods).
|
9
|
|
type constructor
|
A type with a hole in it for a parameter. For example, $\mathtt{Maybe}\ \square$ or $\square \rightarrow \mathtt{Int}$.
|
9
|
|
universal quantification
|
The use of the $\forall x.\ P(x)$ "for all" operator. Used in logic and types for parametric polymorphism.
|
8
9
|
|
upcast
|
If $\tau$ is a subtype of $\rho$, then treating values of type $\tau$ as a value of type $\rho$. Uses the rule of subsumption.
|
9
|
|
variance
|
The way a type constructor interacts with subtyping.
|
9
|
|
atomic
|
A sequence of steps are atomic if they cannot be interrupted, and can be viewed as effectively one step by any external observer. For example, a critical section.
|
10
|
|
commit phase
|
The phase of transaction execution in transactional memory where all changes to transactional variables are saved to the shared variables.
|
10
|
|
concurrency
|
An abstraction for the programmer, allowing programs to be structured as
multiple threads of control, called processes. They may communicate
in various ways.
|
9
10
|
|
critical section
|
A sequence of steps guaranteed to execute atomically due to various means of synchronisation.
|
10
|
|
deadlock
|
The stuck state that results from two (or more) processes are each waiting for the other to perform an action before proceeding.
|
10
|
|
eventual entry
|
The liveness property that states that once a process desires to enter its critical section, it will eventually do so.
|
10
|
|
fairness
|
The assumption of a scheduler that if a process can always make progress, it will eventually be allowed to do so.
|
10
|
|
interference
|
The actions of one process altering the results or execution of another process.
|
10
|
|
isolation
|
A property of a process in a concurrent application where it is as though the process is executed in isolation --- its effects should not be themselves affected by other threads.
|
10
|
|
limited critical reference
|
A property we require of statements in concurrent programs to ensure that each statement can be executed as one atomic step. Requires that each statement access at most one shared variable, at most once.
|
10
|
|
livelock
|
The scenario where two (or more) processes loop repeatedly, waiting for the other process to make progress.
|
10
|
|
lock
|
An abstraction for synchronisation in concurrent programs.
|
10
|
|
mutual exclusion
|
The safety property that says that no two processes are in their critical section simultaneously.
|
10
|
|
optimistic
|
A model of synchronisation where transactions are executed, and only afterwards checking for interference. As opposed to pessimistic models like locks.
|
10
|
|
pessimistic
|
A property of a synchronisation model where interference is pre-emptively prevented before transactions are executed, such as locks. As opposed to optimistic models like transactional memory.
|
10
|
|
process
|
A sequence of statements to execute that forms one thread of control in a concurrent application.
|
9
10
|
|
scheduler
|
The operating system component that chooses which processes get to run.
|
10
|
|
shared variable
|
A mutable variable that may be accessed by multiple processes.
|
10
|
|
software transactional memory
|
A software-only implementation of transactional memory.
|
10
|
|
starvation
|
The scenario where a process is repeatedly denied entry into its critical section because of the scheduler's favouritism to other processes.
|
10
|
|
starvation-freedom
|
The property that starvation cannot occur. Used synonymously with eventual entry.
|
10
|
|
synchronisation
|
Where multiple processes co-ordinate or communicate to give predictable outcomes.
|
9
10
|
|
thread
|
See process.
|
9
10
|
|
transaction
|
See critical section. Used in the context of transactional memory.
|
10
|
|
transactional memory
|
An optimistic means of synchronisation where transactional variables are modified locally in a log, and then commited to shared variables only after validating to ensure the results are not inconsistent due to interference.
|
10
|
|
transactional variable
|
A special type of mutable variable where modifications are tracked using transactional memory.
|
10
|
|
validate phase
|
The phase of transaction execution in transactional memory where we check for interference, and restart the transaction if it has occured.
|
10
|