Processing math: 100%

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:

premise1…premisenconclusion(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.




    
 
  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.

type(nat)nat(z)natnat(s)

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

natnatnattype(plus)plus z N N(plus/z)plus N1 N2 N3plus (s N1) N2 (s N3)(plus/s)

 
    3. 




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.


 



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.


 



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.


 



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.


 










 





powered by io.livecode.ch