Representing Judgements

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

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 $n \ \verb|even|$ holds when $n$ is even. It is inductively defined by the following inference rules:

$${ \over {\mathsf{zero} \ \verb|even|} } \qquad { {n \ \verb|even|} \over {(\verb|succ| (\verb|succ| n)) \ \verb|even|} }$$

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 $\mathsf{even}(n)$ is parametrized by the number $n$ 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.

We represent the judgement $n \verb|even|$ using the following signature:

%sort nat
%term z nat
%term s
  %-> nat
  %-> nat


%sort even nat
%scope even %{
  %term z even z
  %term s
    {N nat}
    %<- even (s (s N))
    %<- even 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.

Caution

The choice to have arrows have appear as a prefix (ie, %-> A %-> B rather than %-> A B) is chosen for this specific layout That is, each line in the chain is idented by an arrow

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 $\mathsf{even}(\mathsf{zero})$.

The second term constant even-s, corresponds to the second inference rule above, which, for any $n$, constructs a derivation of $\mathsf{even}(\mathsf{succ}(\mathsf{succ}(n)))$ from a derivation of $\mathsf{even}(n)$. To encode this inference rule, the constant even-s is given a dependent function type.

The syntax {x:A1} A2 is used to give a type to even-s (replacing the term variable x with N, the type A1 with nat, and the type A2 with even N -> even (s (s N))). This syntax 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). It looks like this:

test = even-s N D.

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 $n$.

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 $n = \mathsf{zero}$. That looks like this:

two-is-even = even-s z even-z.

This represents the derivation

$${\overline{\mathsf{even}(\mathsf{zero})}} \over {\mathsf{even}(\mathsf{succ}(\mathsf{succ}(\mathsf{zero})))}$$

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.

Adequacy

To check that this LF representation is correct (adequate), we must verify that there is a bijection between the derivations of $\mathsf{even}(n)$ and the LF terms of type even N where $n \gg N$. In particular, this LF signature adequately represents natural numbers and derivations of $\mathsf{even}(n)$ 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 $\mathsf{even}(n)$).

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.

Addition

Informal definition

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

$${ \over {\mathsf{plus}(\mathsf{zero},n_2,n_2)} } \qquad { {\mathsf{plus}(n_1,n_2,n_3)} \over {\mathsf{plus}(\mathsf{succ}(n_1), n_2, \mathsf{succ}(n_3))} }$$

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, this term represents a derivation that $2+1 = 3$.

test2 = plus-s (s z) (s z) (s (s z))
            (plus-s z (s z) (s z)
                (plus-z (s z))).

Adequacy

To check correctness of this representation, we must verify that there is a bijection between derivations of $\mathsf{plus}(n_1,n_2,n_3)$ and LF terms of type plus N1 N2 N3 where $n_i \gg N_i$. Once again, the definition of the encoding judgement and the adequacy proof are simple.

These adequacy theorems will be more precise after we review the full language of dependently typed LF in the next section.