Proving metatheorems:Representing the judgements of the natural numbers

 Previous:Simply typed LF Proving metatheorems with Twelf Next:Full LF

Now that we've seen how to represent the syntax of a deductive system, we turn to representing judgements. Our first example is the judgement that a number is even.

Even numbers

Informal definition

The judgement  holds when  is even. It is inductively defined by the following inference rules:

  

LF representation

In the previous sections, we saw how to represent object-language syntax as the inhabitants of LF types. At a high level, the LF methodology for representing judgements is exactly analogous: we represent an object-language judgement with an LF type, where the inhabitants of this type correspond exactly to derivations of the judgement.

However, to adequately represent judgements, we must generalize from simply-typed LF to dependently-typed LF. A moment's thought reveals why a dependently-typed language is appropriate: Object-language judgements are parametrized by their subjects—for example  is parametrized by the number  being judged to be even. Consequently, to represent judgements themselves as LF types, we should consider LF types that are parametrized by the subjects of object-language judgements. But the judgement subjects—the syntax of the language—are represented as LF terms. Thus, to represent judgements themselves as LF types, it is natural to consider families of LF types parameterized by LF terms.

For example, we represent the judgement  using the following signature:

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

The first declaration says that even is a family of types indexed by a nat. This means that for every term N : nat, there is a type even N. Note that the syntax -> is overloaded: it is used to classify both type-level families and and term-level functions. We then use this type family to define the types of two term constants.

The first term constant, even-z, has type even z. This constant represents the derivation that consists of the first inference rule above, which concludes .

The second term constant even-s, corresponds to the second inference rule above, which, for any , constructs a derivation of  from a derivation of . To encode this inference rule, the constant even-s is given a dependent function type.

The syntax {x:A1} A2 represents a dependent function type, which is a generalization of the ordinary function type A1 -> A2 that allows the argument term x to appear in A2. We write the ordinary function type -> as a synonym when the argument is not free in the result type (i.e., A1 -> A2 means {_:A1} A2). Just as with the ordinary function type, LF terms of dependent function type can be applied to a term of the argument type to form a new term.

As an example, the constant even-s can be applied to a term N:nat and then a term of type even N for that N to create a term of type even (s (s N)) (again, for that N). The dependent function type is used to bind the variable N in the type (even N -> even (s (s N))), expressing that the inference rule is schematic in .

When a term of dependent function type is applied to an argument, the argument is substituted into the result type. For example, the term even-s z has type even z -> even (s (s z))—i.e., it is the specialization of the inference rule to . Thus, the term

```even-s z even-z
```

(where we adopt the usual convention that application is left-associative) represents the derivation



The term even-s (s (s z)) (even-s z even-z) represents a derivation that 4 is even, and so on.

To summarize, dependently-typed LF refines the type level of simply-typed LF with dependent function types and families of types parametrized by LF terms. The terms of LF remain unchanged from the grammar presented in the previous section. These changes are sufficient for representing judgements as LF type families and derivations as LF terms.

To check that this LF representation is correct (adequate), we must verify that there is a bijection between the derivations of  and the LF terms of type even N where . In particular, this LF signature adequately represents natural numbers and derivations of  when considered in the empty LF context. It would not be adequate in contexts containing assumptions of the form x : nat (which don't correspond to any natural number) or d : even N (which don't correspond to any of the rules for deriving .

Part of establishing this bijection requires reasoning by induction on the canonical forms of type even N, which corresponds to rule induction on the informal judgement. The definition of the encoding and the proof of adequacy are simple; interested readers are referred to the literature for examples.

Informal definition

Addition can be represented as a judgement relating two natural numbers to their sum:

  

This judgement defines addition by induction on the first argument.

LF representation

This judgement is represented by the following LF signature:

```plus   : nat -> nat -> nat -> type.
plus-z : {N2:nat} plus z N2 N2.
plus-s : {N1:nat} {N2:nat} {N3:nat} plus N1 N2 N3 -> plus (s N1) N2 (s N3).```

The type family plus is indexed by three terms of type nat because the informal judgement has three parameters. The constants correspond to the two inference rules, inhabiting the type family with terms representing derivations. For example, the term

```plus-s (s z) (s z) (s (s z))
(plus-s z (s z) (s z)
(plus-z (s z)))
```

which has type plus (s (s z)) (s z) (s (s (s z))), represents a derivation that 2 + 1 = 3.

To check correctness of this representation, we must verify that there is a bijection between derivations of  and LF terms of type plus N1 N2 N3 where . Once again, the definition of the encoding judgement and the adequacy proof are simple.