Proving metatheorems:Full LF

From The Twelf Project
Jump to: navigation, search
Previous:
Representing judgements
Proving metatheorems with Twelf Next:
Proving totality assertions


In the previous section, we saw how dependently-typed LF can be used to represent object-language judgements. We now discuss dependently-typed LF in more detail.

Definition of LF

Full LF has the following syntax:

In Twelf's concrete syntax, the type is written {x:A1} A2, the kind is written {x:A} K, and the term is written [x] M. The terms are unchanged from the previous grammar. The type families now include both dependent function types and applications of type families to terms. The kind level classifies type families. Type families of kind classify terms. Type families that are not yet fully instantiated have kinds {x:A} K. In both types and kinds, we use -> as an abbreviation when the argument is not free in the result.

For example, in the previous section, we declared the type family plus to have kind nat -> nat -> nat -> type. This means that when plus is applied to three terms of type nat, it forms a type. This kind is syntactic sugar for the kind {_:nat} {_:nat} {_:nat} type. The partial application plus z has kind nat -> nat -> type. Below, we will see examples where the type of one index of a type family depends on a previous argument, which motivates permitting general {x:A} K kinds in the general case.

We do not present the typing rules for LF in detail here. However, we do call attention to the typing rule for application. In a dependently typed language, the application typing rules must substitute the argument into the body of the dependent function type:

In LF, this substitution is in fact a hereditary substitution, ensuring that the terms embedded in the result of the substitution are in canonical form.

This typing rule is how constants representing inference rules are specialized to particular instances. For example, constant even-s from the previous section has type {N:nat} even N -> even (s (s N)), so the application even-s z has type even z -> even (s (s z)).

The typing rule for family applications has a similar substitution into the result kind.

Twelf conveniences

Twelf permits several syntactic conveniences for writing LF signatures. The purpose of this list is to introduce you to these conveniences; we will see examples of them later in this introduction or elsewhere on the wiki.

Definitions

In Twelf, you can define an LF constant for later use. For example:

2 : nat = s (s z).
even-2 : even 2 = even-s z even-z.

The first constant names a natural number 2; the second names a derivation that 2 is even.

You can name terms of higher type as well:

ss : nat -> nat = [x:nat] s (s x).

This constant might be used as follows:

even-4 : even (ss 2) = even-s 2 even-2.

Note that defined constants do not contribute any new inhabitants to the canonical forms of the given types.

Non-canonical forms

Twelf permits non-canonical forms, which are treated as syntactic sugar for the associated canonical form. Here are some examples:

  • Beta-equivalence: the term ss 2, which, if we expand the definitions, reads ([x] (s (s x))) (s (s z)), has the canonical form s (s (s (s z))). As an optimization, Twelf tries not to expand definitions, but the defined form should be thought of as another way of writing the expanded canonical form.

Implicit arguments

Writing out all of the parameters to a constant becomes tedious, so Twelf permits these parameters to be left implicit. Specifically, if a variable starting with a lower-case letter is left unbound in a constant's type, Twelf reports an error. If a variable beginning with an upper-case letter is left unbound, Twelf implicitly binds it in a {N} at the outside of the type. For example, the following two ways of declaring the constant plus-s give it the same type:

%% explicit
plus-s : {N1:nat} {N2:nat} {N3:nat} plus N1 N2 N3 -> plus (s N1) N2 (s N3).
%% implicit
plus-s : plus N1 N2 N3 -> plus (s N1) N2 (s N3).

Similarly, we can make the parameter to plus-z implicit:

%%explicit
plus-z : {N2:nat} plus z N2 N2.
%%implicit
plus-z : plus z N2 N2.

In most circumstances, Twelf can infer the types of the implicit parameters from their use in the constant's type. If it cannot, it reports an error---the type of a constant must be fully determined when the constant is processed.

The application of a constant to its implicit parameters is then inferred from context. For example, using the fully explicit definition of plus, the derivation that 2 + 1 = 3 is written as follows:

d2+1e = plus-s (s z) (s z) (s (s z)) 
        (plus-s z (s z) (s z) 
                (plus-z (s z))).

Using the implicit version, it is much shorter:

d2+1i = plus-s (plus-s plus-z).

The type of this term is ambiguous, but Twelf will attempt to use unification to infer the most general possible type.

Backwards arrow

Twelf permits a type A -> B to be written B <- A. This makes it easier to see the result of applying a constant to all of its arguments. For example:

plus-s : plus (s N1) N2 (s N3)
           <- plus N1 N2 N3.

When we write C <- Pn <- ... P1, we will refer to C as the conclusion of the constant and each Pi as a premise, by analogy with the terminology for the inference rule that this constant represents.

The backwards-arrow also has implications on the logic programming operational semantics for LF, as we discuss below; the conclusion/premise terminology is consistent with the use of these words in logic programming as well.

Type and term inference

Twelf permits type annotations, which are written M:A, on all terms. Type annotations can be used for documentation. Additionally, in some cases they are necessary to help guide type inference. We can also use a type annotation to determine the type of an implicit parameter:

d2+1i' = plus-s (plus-s (plus-z : plus z (s z) (s z))).

This term unambiguously has type plus (s (s z)) (s z) (s (s (s z)))

Type annotations on the arguments of lambda-terms [x:A] M are sometimes necessary, but they can often be elided. Type annotations on Pi-types {x:A2} A can sometimes be elided when the type of the variable is determined by its use.

When they are determined from context, terms can be elided by writing an underscore. For example, if the constants defining plus were declared with explicit nat parameters, we could still write the derivation of 2+1=3 as follows:

d2+1e' = plus-s _ _ _ (plus-s _ _ _ (plus-z (s z))).
Previous:
Representing judgements
Proving metatheorems with Twelf Next:
Proving totality assertions