Syntactic redundancy in LF proofs

Kevin Watkins

November 8, 2001

1 Introduction

The LF logical framework is a language for writing down and manipulating the objects of a formal system. The language itself is a dependently typed lambda calculus. Objects of the formal system with certain properties are represented by LF terms of a certain type. Dependent types allow for parameterizing the representable properties over other objects. A simple example is a representation of proofs in natural deduction. The LF representation starts with a type o of propositions and constants of that type, such as the connective and.

o : type.
and : o → o → o.

The proofs themselves are represented by a type nd indexed by propositions.

nd : o → type.

An inference rule such as and-introduction is a constant mapping deductions of a couple of propositions to a deduction of their conjunction, indexed dependently by the propositions themselves.

and intro : ΠA:o. ΠB:o. nd A → nd B → nd (and A B).

Thus, the representation of a proof ending with an instance of and-introduction would look like an LF term (and intro A B D E) : (nd (and A B)) where D : (nd A) and E : (nd B). An interesting observation about this state of affairs is that if, given D and E, their types could be recovered without any further information, the indexing propositions A and B could be “read off” from the types. It would be redundant to supply the arguments A and B directly. The term could be written (and intro D E).

Conversely, if the type of the whole term were given, the propositions A and B could be “read off” from the type of the whole term. The arguments A and B could again be omitted. Also, there might be further gains representing D and E since they would be examined with their types already known.

This paper describes a system for writing down LF terms that exploits redundancy to omit parts of a term. A type checker for the system recovers this information in an unambiguous way by “reading it off” syntactically. The type checker is guided by annotations in the LF signature that describe which arguments are to be omitted and how they will be recovered. These annotations can be validated to ensure that the type checker will always enough information to operate correctly.

2 Directional type checking

The key to recovering the redundant arguments in the first example above was the ability, given the terms D and E, to generate their types. When the type checker operates in a mode where it accepts a term and generates its type (if the term is well-typed), it is ^{+}-checking. By contrast, the second example began with the type of the whole term already known, and then examined D and E with their types already known. When the type checker examines a term with a putative type already given, it is ^{−}-checking.

In this system, it is always possible to write an LF term of atomic type down in a canonical way such that ^{+}-checking it will succeed and yield its type. There will also be a (possibly different) canonical way to write the term such that given its type, ^{−}-checking will succeed. Conversely, whenever ^{+}-checking succeeds on a term, it is such a canonical representation of some fully explicit LF term, and similarly for ^{−}-checking. Further, the representations of distinct (canonical) LF terms are unique. These representations are called ^{+}-canonical and ^{−}-canonical forms.

In general, the ^{−}-canonical form of a term will be smaller than the ^{+}-canonical form, because it depends on more information from the context. On the other hand, ^{−}-canonical forms may take longer to typecheck because the information from the context might have to be reconciled with information already in the term itself.

Atomic types can be marked with ^{+} or ^{−} to indicate which mode the type checker is operating in. This leads to two judgements for checking terms of atomic type.

Γ ⊢ M : a^{+} Γ ⊢ M : a^{−}

While notionally the first judgement generates the type a^{+} , the presentation is simplified if a^{+} is taken to be a pattern supplied by the context which might contain variables. When ^{+}-checking generates the actual type of M , it will be matched against a^{+} to instantiate the variables. The type a^{−} in the second judgement is a ground type supplied by the context.

Checking a term at a function type is simple. Since terms are represented in eta-long, betanormal form, the term must be a lambda abstraction. The argument type A is an unannotated type. It is not written in the abstraction, and must be supplied as a ground type by the context. This ensures that the type checker only considers typing contexts Γ containing ground types.

Γ, x:A ⊢ M : N
Γ ⊢ λx. M : Πx:A. N

Here N is a metavariable representing an annotated type given by the following grammar.

N ::= a^{+} | a^{−} | Πx:A. N

(The letter N is chosen because these types will always occur negatively in an annotated signature.)

Beta-normal form also ensures that any term of atomic type must be a variable or a constant applied to some arguments. It turns out to be most natural to write applications in this system using spines. Spines essentially reassociate arguments to the right instead of to the left. In the case of a variable applied to arguments, this system makes no attempt to omit any of the arguments. This is why the types of variables introduced into Γ in the rule above are unannotated.

For a constant, annotations on the constant’s type indicate which arguments are to be omitted. The annotations also determine what mode each explicit argument will be checked in. The following grammar describes these types.

P ::= a | Πx:N. P | [Πx:A]_{q}. P

The grammar for unomitted argument types N is as above. An abstraction in brackets indicates that the argument is to be omitted. The qualifier q is a hint as to where the type checker should find the omitted argument.

The rules for ^{+}-checking terms of atomic type are as follows. (The ^{−}-checking rules will be given later.)

x:A ∈ Γ Γ ⊢ S : ⌜A⌝ > a_{0} Γ ⊢ a := a_{0}
Γ ⊢ x · S : a^{+}

c:P ∈ Σ Γ ⊢ S : P > a_{0} Γ ⊢ a := a_{0}
Γ ⊢ c · S : a^{+}

The little function ⌜·⌝ used in the first rule is a means of coercing an unannotated type into an annotated type that directs the type checker to omit no arguments. Each argument is ^{−}-checked, which minimizes the space the arguments occupy.

⌜a⌝ = a
⌜Πx:A. B⌝ = Πx:⌞A⌟. ⌜B⌝

⌞a⌟ = a^{−}
⌞Πx:A. B⌟ = Πx:A. ⌞B⌟

Note that ⌜A⌝ satisfies the P grammar above, while ⌞A⌟ satisfies the N grammar.

Both rules use a spine-checking judgement Γ ⊢ S : P > a_{0} to reduce the constant’s type P to the type a_{0} of the whole term. The type so determined is then matched against the pattern a provided by the context. This written as an assignment Γ ⊢ a := a_{0}.

The first few rules for checking spines are as follows.

Γ ⊢ nil : a > a

Γ ⊢ M : N Γ ⊢ S : [M/x]P > a

Γ ⊢ (M; S) : Πx:N. P > a

3 Reconstructing arguments using synthesized types

The first kind of omitted argument available in this system generalizes the first example from the introduction.

and intro : [ΠA:o]_{s}. [ΠB:o]_{s}. (nd A)^{+} → (nd B)^{+} → nd (and A B)

The terms representing the two premises of the and-introduction are examined by the ^{+}-checker. If it succeeds, it will synthesize types for them. Once their types are known, they can be matched against the patterns (nd A) and (nd B) to determine the omitted arguments A and B. The omitted arguments are said to be reconstructed by synthesis, and the qualifier on the omitted arguments is s. The spine-checking rule for this case merely creates a variable X that will be instantiated later by matching.

Γ ⊢ S : [X/x]P > a
Γ ⊢ S : [Πx:A]_{s}. P > a

Note that the following annotation of and intro is invalid because ^{−}-checking requires knowing the type of the term being checked ahead of time. Also, checking occurs from left to right, so the annotation for and intro_{1} is invalid as well.

and intro : [ΠA:o]_{s}. [ΠB:o]_{s}. (nd A)^{−} → (nd B)^{−} → nd (and A B)
and intro_{1} : [ΠA:o]_{s}. (nd A)^{−} → (nd A)^{+} → nd (and A A)

For the valid annotation of and intro above, it is easy to see that matching will unambiguously resolve the variables A and B. But there are cases where this does not occur because the matching problem is higher-order.

exists intro : [ΠA:(i → o)]_{s}. Πt:i^{−}. (nd (A t))^{+} → nd (exists A)

Here, even when the argument t is known (say it is t_{0}), and the type of the argument representing the premise is known (say it is (nd A_{0})), the matching problem ⊢ (A t_{0}) := A_{0} is insoluble. A similar problem occurs if the second argument is omitted. This demonstrates the need for a criterion that determines when a matching problem is guaranteed to instantiate a variable unambiguously. Such a criterion, strictness, has already been described in the context of notational definitions. Here it is used in the judgements that check the validity of annotated types.

4 Reconstructing arguments using inherited types

Another means of omitting the first two arguments of and intro uses ^{−}-checking.

and intro : [ΠA:o]_{i}. [ΠB:o]_{i}. (nd A)^{−} → (nd B)^{−} → nd (and A B)

Presuming the application of and intro is being ^{−}-checked, its result type will already be known. The arguments A and B can be read off the result type. The other two arguments can then be −-checked since their types are known. Arguments given by matching the result type against the type inherited from the context are marked with the i qualifier. These arguments are only omitted in ^{−}-canonical forms, since it is only during ^{−}-checking that an accurate type is supplied by the context.

The ^{−}-checker needs some way of getting a pattern for the result type before it even knows that all of the arguments are well typed. This leads to a two stage process. In the first stage the −-checker creates variables for all the omitted arguments marked with i and substitutes a wildcard for the other arguments. The result type is matched against the type from the context to instantiate the variables. At that point the variables can be inserted into the spine to create a ^{+}-canonical form and the usual spine-checking judgement is applied. The rules for the first stage are as follows.

Γ ⊢ a_{1} := a
Γ ⊢ nil : a_{1} :> a / nil

Γ ⊢ S : [X/x]P :> a / S′
Γ ⊢ S : [Πx:A]_{i}. P :> a / (X; S′)
Γ ⊢ S : [ /x]P :> a / S′

Γ ⊢ (M; S) : Πx:N. P :> a / (M; S′)

Γ ⊢ S : [ /x]P :> a / S′
Γ ⊢ S : [Πx:A]_{s}. P :> a / S′

The new rules for ^{−}-checking atomic types put the two stages together.

x:A ∈ Γ Γ ⊢ S : ⌜A⌝ :> a / S′ Γ ⊢ S′ : ⌜A⌝ >^{−} a_{0} Γ ⊢ a = a_{0}
Γ ⊢ x · S : a^{−}
c:P ∈ Σ Γ ⊢ S : P :> a / S′ Γ ⊢ S′ : P >^{−} a_{0} Γ ⊢ a = a_{0}
Γ ⊢ c · S : a^{−}

Note that the spine-checking judgment Γ ⊢ S : P > a has been annotated with the mode. All the rules for spine-checking presented so far apply in both modes. The new rules for i qualified implicit arguments are slightly different for the two modes.

Γ ⊢ M : ⌞A⌟ Γ ⊢ S : [M/x]P >^{+} a
Γ ⊢ (M; S) : [Πx:A]_{i}. P >^{+} a
Γ ⊢ S : [M/x]P >^{−} a
Γ ⊢ (M; S) : [Πx:A]_{i}. P >^{−} a

The reason is that for ^{+}-checking, such an argument was never omitted and needs to be typechecked, while for ^{−}-checking, the argument was generated by the prepass, so it is guaranteed to be well typed.

An optimization is possible when the result type of a constant depends only on inherited arguments. Then the matching performed by the prepass involves no wildcards, so it ensures that the term being checked is at least consistent with the type information given by the context (though some arguments may remain to be typechecked). This means the final equality test in the −-checking rule for the application involving the constant could be omitted. Similarly, the prepass itself can be omitted if the constant has no inherited arguments.

5 Second-level omitted arguments

An interesting phenomenon occurs when the only dependent occurrences of an argument are in the types of other omitted arguments. This happens for “two-level” signatures, of which the following is an example.

nd eq : [ΠA:o]_{s}. (nd A)^{+} → (nd A)^{−} → type.
nd refl : [ΠA:o]_{?}. [ΠD:nd A]_{i}. eq D D.

It is not clear what qualifier to attach to the first argument. It might be an inherited argument—in ordinary LF the result type would be written (eq A D D)—except that the occurrence of A in the result type has already been omitted. It might be a synthesized argument, since it occurs in the type of the second argument, but the second argument’s type is never constructed explicitly.

The truth is that it doesn’t really matter. So long as the argument has no explicit occurrences anywhere in a type actually constructed by the algorithm, and as long as it has at least one strict occurrence in one of the types never constructed, the argument is guaranteed to exist once the type checker succeeds. To describe this situation a different style of implicit argument is introduced. The grammar for positive types P is extended slightly.

P ::= a | Πx:N. P | [Πx:A]_{q}. P | [[Πx:A]]_{q}. P

The nd refl example can now be annotated as follows.

nd refl : [[ΠA:o]]_{i}. [ΠD:nd A]_{i}. eq D D.

The distinction between the s and i qualifiers is important for such arguments because the ^{+}-canonical form of an application of nd refl will contain the second argument explictly, and so for it to be checkable the first argument will also have to be present explicitly.