Full LF

This page is part of the introduction to proving metatheorems with STELF.

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:

$$\begin{align*} K & ::= \mathtt{type} \mid \Pi x{:}A. K \\ A & ::= b \mid A \, M \mid \Pi x{:}A_1. A_2 \\ R & ::= c \mid x \mid R \, M \\ M & ::= R \mid \lambda x. M \end{align*}$$

In STELF’s concrete syntax, the type $\Pi x{:}A_1 .A_2$ is written {x:A1} A2, the kind $\Pi x{:}A .K$ is written {x:A} K, and the term $\lambda x.M$ is written [x] M. The terms are unchanged from the previous grammar. The type families now include both dependent function types and applications $A \, M$ of type families to terms. The kind level classifies type families. Type families of kind $\mathtt{type}$ 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:

$$R : \Pi x {:} A. B \qquad M : A \over R \; M : [M/x]B$$

In LF, this substitution $[M/x]B$ 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 $A\,M$ has a similar substitution into the result kind.

$$A : \Pi x {:} B. K \qquad M : B \over A \; M : [M/x]K$$

STELF conveniences

STELF 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 STELF, you can define an LF constant for later use. For example assuming the last section’s definition of natural numbers, we can write this:

nat : type.
z   : nat.
s   : nat -> nat.

even    : nat -> type.
even-z  : even z.
even-s  : {N:nat} even N -> even (s (s N)).

plus : nat -> nat -> nat -> type.

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. (STELF treats numeric identifiers the same as any other constants as long as no constraint domains are active, so naming a constant 2 is no different, from STELF’s perspective, than naming it two.)

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.

Definitions like this do not create any new numbers (i.e. any new canonical forms of type nat), they just name what can be formed with existing constants.

Non-canonical forms

STELF 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))). So we might expect STELF to automatically expand that definition in its output:

four = ss 2.

The expected expansion doesn’t actually happen! STELF works very hard not to expand definitions, while still always returning the same results as if those definitions had been expanded. For all purposes ss 2 should be thought of as another way of writing the s (s (s (s z))).

Eta-equivalence

The term s, which has type nat ->; nat can be used instead of its eta-expansion [x] s x. Eta expansions will always be performed in STELF’s output:

other-s = s.

We will discuss eta-equivalence more in the context of higher-order representations.

Implicit arguments

Writing out all of the parameters to a constant becomes tedious, so STELF 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, STELF reports an error. If a variable beginning with an upper-case letter is left unbound, STELF 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-explicit : {N1:nat} {N2:nat} {N3:nat} plus N1 N2 N3 -> plus (s N1) N2 (s N3).
%% implicit
plus-s-implicit : plus N1 N2 N3 -> plus (s N1) N2 (s N3).

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

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

In most circumstances, STELF 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-explicit (s z) (s z) (s (s z))
        (plus-s-explicit z (s z) (s z)
                (plus-z-explicit (s z))).

Using the implicit version, it is much shorter:

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

The type of this term is ambiguous, but STELF will attempt to use unification to infer the most general possible type. The fully general result has an additional parameter, X1:nat, and establishes not that $2 + 1 = 3$ but the more general fact $2 + \mathtt{X_1} = \mathsf{succ}(\mathsf{succ}(\mathtt{X_1}))$

Backwards arrow

STELF 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

STELF 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 saw before that the implicitly typed version of plus resulted in an ambiguous type:

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

If for some reason this was undesirable, and we really wanted this to be proof that $2 + 1 = 3$, one way to achieve this would be to use a type annotation to say that plus-z should be used specifically as a proof that $0 + 1 = 1$:

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

Type annotations on the arguments of lambda-terms [x:A] M are sometimes useful, even though they aren’t present in the formal definition of LF. Type annotations on Pi-types \{x:A2\} A can sometimes be elided when the type of the variable is determined by its use, even though they are required in the formal definition of LF.

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-explicit _ _ _
    (plus-s-explicit _ _ _
        (plus-z-explicit (s z))).