Twelf is a tool for reasoning about deductive systems. Elegantly, each declaration in Twelf looks like an inference rule:
$${ \begin{align} &\text{premise}_1\\ &\ldots\\ &\text{premise}_n\\ \end{align} \over{\text{conclusion}} }(\text{name})$$name : premise-1 -> ... -> premise-n -> conclusion.
An inference rule without premises is called an axiom.
Let's get started with some Twelf code.
We can interpret an inference rule in two ways.
z inhabits the type nat. Each
premise is also a type. An inference rule with \(n\)
premises defines a function with parameter types defined by the
premises and return type defined by the conclusion. This function can
be applied to \(n\) terms of the premise types to yield a term of the
conclusion type. For example, the function s can be
applied to term z, to yield the term s z.
$${\text{}\over{\text{type}}}(\text{nat}) \quad {\text{}\over{\text{nat}}}(\text{z}) \quad {\text{nat}\over{\text{nat}}}(\text{s})$$
plus/s states that if you have
evidence of plus N1 N2 N3, then you can construct
evidence for plus (s N1) N2 (s N3) for
any nat terms N1, N2, N3.
$${\begin{align}
\text{nat}\\
\text{nat}\\
\text{nat}\\
\end{align}\over{\text{type}}}(\text{plus}) \quad {\text{}\over{\text{plus z N N}}}(\text{plus/z}) \quad {\text{plus N1 N2 N3}\over{\text{plus (s N1) N2 (s N3)}}}(\text{plus/s})$$
This dual interpretation, propositions-as-types, is known as the
Curry-Howard isomorphism. The type interpretation is more natural when
we care to distinguish terms of the same type: even
though z and s z are both of
type nat, we don't think of them as semantically
equivalent. The proposition interpretation is more natural when we
only care about inhabitation: whether it is true or false. For
example, plus (s z) z (s z) is inhabited (true),
while plus (s z) z z is not (false).
In Twelf, we can use the %query command to ask about
inhabitation. Click the play button, and also try queries of your
own by editing the box.
We can use the %solve command to actually construct a term of a certain type.
A term for the type plus (s (s z)) (s z) (s (s (s z)))
is plus/s (plus/s plus/z). Indeed,
the plus/z axiom gives us plus z (s z) (s
z), and applying plus/s twice constructs the
evidence for the desired proposition.
In our definition of plus/z, the N is an
implicit dependent type. We could also define the plus judgment with
all the dependent types made explicit. Now, we also would need to be
explicit in the applications of these new rules, as you can see with
the %solve query below.
Note that A -> B is just an abbreviation
for {_:A} B, where the name of the term of
type A is irrelevant, since the type B does
not depend on it.
We can think of a rule with conclusion type and \(n\)
premises as defining an \(n\)-place relation. Taken together, the
rules with conclusion whose head matches the relation name defines all
the way this relation may hold, i.e. all the possible derivations.
We can also define \(n\)-place relations, where some of the places are universally quantified (inputs), and some are existentially quantified (outputs). If we can show that the relation is total, i.e. we can always find outputs for all possible inputs, then we can interpret the relation as a theorem. The proof of a theorem also takes the form of inference rules, and proceeds by induction on the derivation rules of some (possibly none) of the inputs.
Let's get more concrete with some Twelf code.
We show that z is a neutral element on the right. The
induction is on the first term of type nat. Thus, we have
a case (itself, an inference rule) for each inference rule whose
conclusion is nat. In the s case, we make
use of the induction hypothesis: the term of type nat in
the premise (N) is smaller than the term of
type nat in the conclusion ((s N)).
We show that we can increment on the right. The induction is on the
first term of type plus N1 N2 N3. Thus, we need to
consider all possible inference rules
for plus: plus/z and plus/z. We
use the backwards arrow <-, so that we can start with
the conclusion and then construct how we reach it.
Now, let's prove that plus is commutative.
Exercise: Show that the plus relation is total, i.e. we can always add any two numbers.
Often, we need to reason about equality between terms. For a given type, we can define equality structurally or reflexively.
The recipe for structural equality has one case per derivation rule.
The recipe for reflexive equality always has just one case for identity.
Exercise: Show that the two definitions of equality for nat, reflexive and structural, are equivalent.
Armed with equality, we can show that the third place of
the plus relation is uniquely determined by the other two
places.