twelf for minidot, an interactive tutorial

Fork me on GitHub

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.

nat : type. z : nat. s : nat -> nat.
plus : nat -> nat -> nat -> type. plus/z : plus z N N. plus/s : plus N1 N2 N3 -> plus (s N1) N2 (s N3).

We can interpret an inference rule in two ways.

  1. Each conclusion is a type. An axiom defines a term inhabiting the type of the conclusion. For example, the term 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})$$
  2. Each conclusion and premise is a proposition. An inference rule defines a recipe to construct a proof or evidence for the proposition in the conclusion. For example, the rule 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.

%query * 1 plus (s z) z (s z). %query 0 * plus (s z) z z. %query * 3 plus A B C.

We can use the %solve to actually construct a term of a certain type.

%solve a_nat : nat. %solve a_deriv : plus (s (s z)) (s z) N.

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.

plus : nat -> nat -> nat -> type. plus/z : {N:nat} plus z N N. plus/s : {N1:nat} {N2:nat} {N3:nat} plus N1 N2 N3 -> plus (s N1) N2 (s N3).
%solve a_deriv : plus (s (s z)) (s z) N.

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)).

plus-z-right-neutral : {N:nat} plus N z N -> type. %mode plus-z-right-neutral +N -D. -/z : plus-z-right-neutral z plus/z. -/s : plus-z-right-neutral N D -> plus-z-right-neutral (s N) (plus/s D). %worlds () (plus-z-right-neutral _ _). %total N (plus-z-right-neutral 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.

plus-s-right-inc : plus N1 N2 N3 -> plus N1 (s N2) (s N3) -> type. %mode plus-s-right-inc +D1 -D2. -/z : plus-s-right-inc plus/z plus/z. -/s : plus-s-right-inc (plus/s D1) (plus/s D2) <- plus-s-right-inc D1 D2. %worlds () (plus-s-right-inc _ _). %total D (plus-s-right-inc D _).

Now, let's prove that plus is commutative.

plus-comm : plus N1 N2 N3 -> plus N2 N1 N3 -> type. %mode plus-comm +D1 -D2. -/z : plus-comm plus/z D <- plus-z-right-neutral _ D. -/s : plus-comm (plus/s D1) D3 <- plus-comm D1 D2 <- plus-s-right-inc D2 D3. %worlds () (plus-comm _ _). %total D (plus-comm D _).

Exercise: Show that the plus relation is total, i.e. we can always add any two numbers.

% TODO .
plus-total : {N1:nat} {N2:nat} plus N1 N2 N3 -> type. %mode plus-total +N1 +N2 -D. -/z : plus-total z N2 plus/z. -/s : plus-total (s N1) N2 (plus/s D) <- plus-total N1 N2 D. %worlds () (plus-total _ _ _). %total N1 (plus-total N1 _ _).

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.

nat-eq-struct : nat -> nat -> type. nat-eq-struct/z : nat-eq-struct z z. nat-eq-struct/s : nat-eq-struct (s N1) (s N2) <- nat-eq-struct N1 N2.

The recipe for reflexive equality always has just one case for identity.

nat-eq : nat -> nat -> type. nat-eq/id : nat-eq N N.

Exercise: Show that the two definitions of equality for nat, reflexive and structural, are equivalent.

nat-eq-r2s : nat-eq N1 N2 -> nat-eq-struct N1 N2 -> type. %mode nat-eq-r2s +A -B. % TODO . %worlds () (nat-eq-r2s _ _). %total A (nat-eq-r2s A _). nat-eq-s2r : nat-eq-struct N1 N2 -> nat-eq N1 N2 -> type. %mode nat-eq-s2r +A -B. % TODO . %worlds () (nat-eq-s2r _ _). %total A (nat-eq-s2r A _).
nat-eq-struct-refl : {N:nat} nat-eq-struct N N -> type. %mode nat-eq-struct-refl +N -D. -/z : nat-eq-struct-refl z nat-eq-struct/z. -/s : nat-eq-struct-refl (s N) (nat-eq-struct/s D) <- nat-eq-struct-refl N D. %worlds () (nat-eq-struct-refl _ _). %total N (nat-eq-struct-refl N _). nat-eq-s : nat-eq N1 N2 -> nat-eq (s N1) (s N2) -> type. %mode nat-eq-s +A -B. -/id : nat-eq-s nat-eq/id nat-eq/id. %worlds () (nat-eq-s _ _). %total A (nat-eq-s A _). nat-eq-r2s : nat-eq N1 N2 -> nat-eq-struct N1 N2 -> type. %mode nat-eq-r2s +A -B. -/id : nat-eq-r2s nat-eq/id D <- nat-eq-struct-refl _ D. %worlds () (nat-eq-r2s _ _). %total A (nat-eq-r2s A _). nat-eq-s2r : nat-eq-struct N1 N2 -> nat-eq N1 N2 -> type. %mode nat-eq-s2r +A -B. -/z : nat-eq-s2r nat-eq-struct/z nat-eq/id. -/s : nat-eq-s2r (nat-eq-struct/s D) EQ' <- nat-eq-s2r D EQ <- nat-eq-s EQ EQ'. %worlds () (nat-eq-s2r _ _). %total A (nat-eq-s2r A _).

Armed with equality, we can show that the third place of the plus relation is uniquely determined by the other two places.

nat-eq-s : nat-eq N1 N2 -> nat-eq (s N1) (s N2) -> type. %mode nat-eq-s +A -B. -/id : nat-eq-s nat-eq/id nat-eq/id. %worlds () (nat-eq-s _ _). %total A (nat-eq-s A _). plus-unique : plus N1 N2 N3 -> plus N1 N2 N3' -> nat-eq N3 N3' -> type. %mode plus-unique +D1 +D2 -EQ. -/z : plus-unique plus/z plus/z nat-eq/id. -/s : plus-unique (plus/s D1) (plus/s D2) EQ' <- plus-unique D1 D2 EQ <- nat-eq-s EQ EQ'. %worlds () (plus-unique _ _ _). %total D (plus-unique D _ _).