-
Object-language terms are written in \texttt{fixed-width}^[However, strings in fixed-width font beginning with a question mark like
$\ttt{?f}$ do not denote object language terms but "holes"; see below.] or special fonts (e.g.$\N$ ,$\mathcal{U}_0$ ), whereas meta-language terms are written in `normal', variable-width font. For example, in the sentence$$\text{If
$A,B : \mathcal{U}_0$ and$f : A \rightarrow B$ , then $f \equiv \lambda \texttt{x}.
f(\texttt{x})$}.$$the symbols '$t$', '$A$' and '$B$' denote meta-variables denoting arbitrary for object-language terms, whereas the symbols '$\mathcal{U}_0$' and '$\texttt{x}$' denote object-language terms.
-
When the context
$\Gamma$ of a sequent$$\Gamma \vdash J$$ is empty, we may drop the turnstile and simply denote it by
$J$ . Or, we might write it as$$\vdash J$$ or even use the book's convention and denote the empty context explicitly using a dot$$\emptyctx \vdash J.$$ -
When presenting deduction rules, we will usually drop the parentheses in contexts, e.g. we write
$$\inferrule{a : A \ b : B \ x : A, y : B \vdash f(x,y) : C}{a : A, b : B \vdash f(a,b) : C}$$ instead of
$$\inferrule{a : A \ b : B \ (x : A, y : B) \vdash f(x,y) : C}{(a : A, b : B) \vdash f(a,b) : C}.$$ In accordance with this convention, concatenation of contexts will be denoted using a comma.
For example, if
$$\Gamma = (x : X, y : Y)\quad \text{and}\quad \Gamma' = (a : A, b : B),$$ then$\Gamma, \Gamma'$ denotes$$(x : X, y : Y, a : A, b : B).$$ Similarly,$\Gamma, z : Z$ denotes$(x : X, y : Y, z : Z)$ . -
Holes are indicated using the symbol
$\Box$ , as in \begin{align*} \text{(0)} && \Gamma \vdash \labstt{x}{A}{\Box} : \prod_{x : A} B && \text{(-1),$\Pi$ -INTRO} \ \text{(-1)} && \Gamma, x : A \vdash \Box : B. && \end{align*} Named holes are indicated by a question mark followed by a meta-variable name, all written in fixed-width font, as in \begin{align*} \text{(0)} && \Gamma \vdash \labstt{x}{A}{\ttt{?f}} : \prod_{x : A} B && \text{(-1),$\Pi$ -INTRO} \ \text{(-1)} && \Gamma, x : A \vdash \ttt{?f} : B. && \end{align*} -
If
$f$ is a function symbol that's usually written in infix notation, we will write$(f)$ (following the Idris convention) when we want to indicate that it is written in postfix.For example, we might write
$$\labstt{\N}{n}{\labstt{\N}{m}{n+m}}$$ also as$$\labstt{\N}{n}{\labstt{\N}{m}{(+)(n,m).}}$$ -
When viewed as implicit, function arguments are suppressed in the notation.
For example, instead of
$$\happly(A,B, f, g, \funext(A, B, f, g, h))$$ we may write$$\happly(\funext(h))$$ instead.We might also---instead of completely suppressing it in the notation---replace an implicit argument with an underscore, especially if confusion might arise otherwise.
In the previous example, we might therefore also have written
$$\happly(_, _, _, _, \funext(_, _, _, _, h)).$$ -
To explicitly indicate that an argument to a function is normally treated as implicit, we surround it using curly braces
${$ ,$}$ in the type declaration.For example, to indicate that the arguments
$A$ and$B$ in$$\mathsf{ev}: \prod_{A : \UV} \prod_{B : A \rto UV} \prod_{a : A} \prod_{f : \prod_{x : A} B(x)} B(a)$$ are implicit, we would write
$$\mathsf{ev}: \prod_{{A : \UV}} \prod_{{B : A \rto UV}} \prod_{a : A} \prod_{f : \prod_{x : A} B(x)} B(a)$$ or even
$$\mathsf{ev}: \left{\prod_{A : \UV}\right} \left{\prod_{B : A \rto UV}\right} \prod_{a : A} \prod_{f : \prod_{x : A} B(x)} B(a)$$ if convenient.
The concept of a "hole" is crucial for the practicality of programming in depenently typed programming languages; for that same reason, we must talk about it here, since there is no difference between that activity and doing proofs in type theory.
If life would be easy^[Newsflash, it's not.], whenever we'd want to prove something in type theory,
i.e. find a term
For example, if
That's pretty obvious. However, a small problem arises if we are to write down such a "backwards" proof formally because a formal^[Our "formal proofs" aren't really formal, because we leave out intermediate, "obvious" steps in the linearized derivation tree.] proof ends with the goal, hence we need to know the complete proof in advance before the goal can even be written down.
Thus it becomes natural to write down the derivation tree in reverse order,
beginning with the end goal. However, that still doesn't solve the problem,
since the term
The solution is to simply leave this meta-variable uninstantiated, i.e. to leave a hole in derivation tree, which is to be filled in later.
This "hole" will be denoted by the symbol
\begin{align*}
\text{(0)} && \Gamma \vdash \labstt{x}{A}{\Box} : \prod_{x : A} B &&
\text{(-1),
holes are introduced by applying a derivation rule (scheme) containing a meta-variable ranging over terms but without supplying an actual term for one (or more) of those meta-variables.
In the rule (scheme)
$$\inferrule*[right=\text{$\Pi$-INTRO}]{\Gamma, x : A \vdash b : B}{\Gamma \vdash
\labstt{x}{A}{b} : \prod_{x : A} B},$$
there are three^[To be really precise,
The relation between the two "holes" in the judgements^[Since they contain
meta-variables/holes, they aren't judgements, strictly speaking.]
\begin{align*}
\text{(0)} && \Gamma \vdash \labstt{x}{A}{\Box} : \prod_{x : A} B &&
\text{(-1),
However, sometimes (especially when applying a rule scheme containing several meta-variables) it's helpful to make this relation more explicit by naming the holes, i.e. by inserting an actual meta-variable instead of the box symbol. Following a popular convention from dependently typed programming, these meta-variables will be written in fixed-width font with a question mark infront, to clearly mark them as such.
The example above could therefore have also been written as
\begin{align*}
\text{(0)} && \Gamma \vdash \labstt{x}{A}{\ttt{?f}} : \prod_{x : A} B &&
\text{(-1),
Once a hole has been created in a proof, you must eventually fill it in order to obtain a complete derivation. To fill a hole means to have a complete^[complete up to filled holes] derivation ending^[i.e. starting in it, if the derivation is written backwards] in it.
For instance, if in the above example we had
\begin{align*}
\text{(0)} && \Gamma \vdash \labstt{x}{A}{\ttt{?f}} : \prod_{x : A} A &&
\text{(-1),
Once all holes in a derivation with holes are "filled", we can derive a "normal" derivation (without holes), by substituting the filling terms into their corresponding holes, successively from bottom to top.
For example, removing the holes in the above three-step derivation results in
\begin{align*}
\text{(0)} && \Gamma \vdash \labstt{x}{A}{x} : \prod_{x : A} A &&
\text{(-1),
Since this is a completely mechanical operation that is obviously\texttrademark{} well-defined and correct, there is no need to actually carry it out. So, we won't.
Even though writing derivations backwards and using holes help in reconciling the interactive nature of dependently typed programming with the linear and immutable nature of written text, some tension remains.
It is therefore sometimes convenient to "update" a judgement, i.e. to first write down a preliminary version (e.g. in order to have something that can be referred to verbally) and then afterwards follow it by a more complete, or final version.
We adopt the convention that a judgement always supersedes any previous ones with the same number. Here we mean by "supersede" that a newer version replaces an older one in situ, i.e. even if more judgements (with lower numbers) are written down in between, judgements are to be read in order according to their numbering.
For instance, in the example below we want to derive the addition on natural numbers, so we might want to start by writing down \begin{align*} \text{(0)} && \vdash (\ttt{?+}) : \N \rto \N \rto \N && \end{align*} in order to fix the type of the sought-after term in the readers mind. Then, we might want to bring to the readers attention the convention regarding associativity of the arrow notation and rewrite the judgement as \begin{align*} \text{(0)} && \vdash (\ttt{?+}) : \N \rto (\N \rto \N), && \end{align*} so that it immediately suggests the application of the induction principle, which then leads us to rewrite it a second (and final) time as \begin{align*} \text{(0)} && \vdash (\ttt{?+}) : \N \rto (\N \rto \N) && \text{$\N$-ELIM on (-1),(-2)} \ \text{(-1)} && \vdash \ttt{?add}_0 : \N \rto \N && \ \text{(-2)} && n : \N, f : \N \rto \N \vdash \ttt{?add}s(n,f) : \N \rto \N. && \end{align*} Once again, stating that (0) is derived from (-1) and (-2) contains some implicit information, in this case the assumed judgemental equality $$(\ttt{?+}) \equiv \ind\N(\labst{n}{\N \rto \N}, \ttt{?add}_0, \ttt{?add}s).$$ If we want to make this explicit (which in this case we probably would), we could have done so by writing \begin{align*} \text{(0)} && \vdash \ind\N(\labst{n}{\N \rto \N}, \ttt{?add}_0, \ttt{?add}_s) : \N \rto (\N \rto \N) && \text{$\N$-ELIM on (-1),(-2)} \end{align*} instead (or even afterwards).
To fix ideas, let us look at a more complicated derivation, containing several holes.
First, let us define addition of natural numbers
\begin{align*}
\text{(0)} && \vdash (\ttt{?+}) : \N \rto \N \rto \N. && \
\intertext{Recalling that
Second, let's prove that addition is associative.
So we want to inhabit
\begin{align*}
\text{(0)} && n,m,k : \N \vdash \Box : (n+m) + k =\N n + (m + k). && \
\intertext{Of course we are going to use induction for this, so we somehow need
to get a function $\N \rto$ in there. Since we want to use induction on the
variable $n$, we produce this function by lambda abstracting on that variable:}
\text{(0)} && n,m,k : \N \vdash \ttt{?f}(n) : (n+m) + k =\N n + (m + k) && \text{$\Pi$-ELIM on (-1)} \
\text{(-1)} && m,k : \N \vdash \ttt{?f} : \prod_{n : \N} (n+m) + k =\N n + (m + k). && \
\intertext{Now we plug this hole using induction:}
\text{(-1)} && m,k : \N \vdash \ttt{?f} : \prod{n : \N} (n+m) + k =\N n + (m + k) && \text{$\N$-ELIM on (-2), (-3)} \
\text{(-2)} && m,k : \N \vdash \ttt{?f}0 : (0+m) + k =\N 0 + (m + k) && \
\text{(-3)} && m,k : \N, n : \N, p : (n+m) + k =\N n + (m + k) && \
&& \vdash \ttt{?f}s(n,p) : (\suc(n)+m) + k =\N \suc(n) + (m + k). && \
\intertext{Now by construction of