Proof terms for simply typed higher order logic

Stefan Berghofer^{⋆} and Tobias Nipkow

Technische Universität München, Institut für Informatik

                     http://www.in.tum.de/~berghofe/
                      http://www.in.tum.de/~nipkow/

Abstract. This paper presents proof terms for simply typed, intuitionistic higher order logic, a popular logical framework. Unification-based algorithms for the compression and reconstruction of proof terms are described and have been implemented in the theorem prover Isabelle. Experimental results confirm the effectiveness of the compression scheme.

1 Introduction

In theorem provers based on the LCF approach, theorems can only be constructed by a small set of primitive inference rules. Provided the implementation of these rules is correct, all theorems obtained in this way are sound. Hence it is often claimed that constructing an explicit proof term for each theorem is unnecessary. This is only partially true, however. If the core inference engine of a theorem prover is relatively large, correctness is difficult to ensure. Being able to verify proof terms by a small and independent proof checker helps to minimize the risks. Moreover, a precise notion of proof terms facilitates the exchange of proofs between different theorem proving systems. Finally, proof terms are a prerequisite for proof transformation and analysis or the extraction of computational content from proofs. Probably the most prominent application these days is proof-carrying code [5], a technique that can be used for safe execution of untrusted code. For these reasons we have extended Isabelle [9] with proof terms. However, apart from the actual implementation, our work is largely independent of Isabelle and most of this paper deals with the general topic of proof terms for simply typed, intuitionistic higher order logic (abbreviated to λHOL below), Isabelle’s meta logic. Because other logics (e.g. full HOL) can be encoded in this meta logic, this immediately yields proof terms for those logics as well.

We start with a disclaimer: the idea of proof terms based on typed λ-calculus has been around for some time now and is the basis of a number of proof assistants for type theory, for example Coq [2]. Even more, with the advent of “pure type systems” and the λ-cube [1], it became clear what proof terms for λHOL look like in principle (although this seems to have had little impact on the HOL world). What we have done is to re-introduce the strict syntactic separation between terms, types, and proofs to make it more amenable to readers from a simply typed background. Thus our presentation of proof terms can be seen as a

⋆ Supported by DFG Graduiertenkolleg Logic in Computer Science

partial evaluation of the corresponding pure type system, i.e. separating the layers. Things are in fact a bit more complicated due to the presence of schematic polymorphism in our term language.

The main original contribution of the paper is a detailed presentation of proof compression. A naive implementation of proof terms results in proofs of enormous size because with every occurrence of a proof rule the instantiations for its free variables are recorded. Thus it is natural to try and leave out some of those terms and to reconstruct them by unification during proof checking. Necula and Lee [6] have presented a scheme for proof compression in LF, another logical framework based on type theory. They analyze the proof rules of the object logic statically to determine what can be reconstructed by a weak form of unification. In contrast, we do a dynamic analysis of each proof term to determine what can be dropped. Reconstruction of missing information by unification is also available in other systems, e.g. Elf [12, 11], but none of them offers an automatic dynamic compression algorithm.

There has also been work on recording proofs in the HOL system [3, 14], but it is firmly based on a notion of proof that directly reflects the implementation of inferences as calls to ML functions. These proof objects lack the conciseness of λ-terms and it is less clear how to compress them other than textually.

We start by presenting the logical framework (§2) and its λ-calculus based proof terms (§3). In order to shrink the size of proofs we introduce partial proofs (§4), show how to collect equality constraints from a (partial) proof (§4.1), how to solve these constraints (§4.2) (to check that the proof is correct), and how to generate partial proofs from total ones, i.e. how to compress proofs (§4.3).

2 The logical framework

In a nutshell, Isabelle’s meta logic [9, 8] is the minimal higher order logic of implication and universal quantification over simply typed λ-terms including schematic polymorphism. Thus types are first order only, which makes type reconstruction decidable. A type τ is either a variable α or a compound type expression (τ_{1}, …, τ_{n})tc, where tc is a type constructor and n is its arity. The (infix) constructor → for function types has arity 2. We assume implicitly that all types are well-formed, i.e. every type constructor is applied to the correct number of arguments. The set t of terms is defined in the usual way by

t = x | c | λx :: τ. t | t t

Formulae are terms of the primitive type prop. The logical connectives are:

universal quantification ⋀ :: (α → prop) → prop
implication  ⟹ :: prop → prop → prop

Now we show how an object logic is formalized in this meta logic. As an example we have chosen a fragment of HOL. First we introduce new types and constants for representing the connectives of this logic:

Tr :: bool → prop  ∀ :: (α → bool) → bool
⟶ :: bool → bool → bool  ∃ :: (α → bool) → bool

Here, bool is the type of object level propositions. The function Tr establishes a connection between meta level and object level truth values: the expression Tr P should be read as “P is true”. The application of Tr is occasionally dropped when writing down formulae. The inference rules for the meta logic consist of the usual introduction and elimination rules and are shown in §3.1 below.

Inference rules of object logics are usually written like this:

\begin{aligned}ϕ_{1} & … & ϕ_{n} \\ & ψ \end{aligned}

In our meta logic they become nested implications:

ϕ_{1} ⟹ ⋯ ⟹ ϕ_{n} ⟹ ψ

Here are some examples:

impI : ⋀ A B. (Tr A ⟹ Tr B) ⟹ Tr (A ⟶ B)
impE : ⋀ P Q R. Tr (P ⟶ Q) ⟹ Tr P ⟹ (Tr Q ⟹ Tr R) ⟹ Tr R
allI : ⋀ P.  (⋀ x. Tr (P x)) ⟹ (Tr (∀x. P x))
allE : ⋀ P x R. Tr (∀x. P x) ⟹ (Tr (P x) ⟹ Tr R) ⟹ Tr R
exI : ⋀ P x.  Tr (P x) ⟹ Tr (∃x. P x)
exE : ⋀ P Q. Tr (∃x. P x) ⟹ (⋀ x. Tr (P x) ⟹ Tr Q) ⟹ Tr Q

Note that the introduction rules impI and allI are for object level implication and universal quantification are expressed by simply referring to the meta level counterpart of these connectives. The expression ⋀ x. ϕ is just an abbreviation for ⋀ (λx. ϕ), and similarly for ∀ and ∃.

3 Proof terms

3.1 Basic concepts

The set of proof terms p is defined as follows:

p = h | c_{[\overline{τ_{n}/α_{n}}]} | λh : ϕ. p | λx :: τ. p | p p | p t

The letters h, c, x, t, ϕ and τ denote proof variables, proof constants, term variables, terms of arbitrary type, terms of type prop and types, respectively. Note that terms, types and proof terms are considered as separate concepts. This is in contrast to type theoretic frameworks, where these concepts are identified. We will write Γ ⊢ p : ϕ for “p is a proof of ϕ in context Γ ”, where ϕ is a term of type prop, representing the logical proposition proved by p. The context Γ associates a proof variable with a term representing the proposition whose proof it denotes, and a term variable with its type. We require each context to be wellformed, i.e. every variable is associated with at most one term or type. Proof constants correspond to axioms or already proved theorems. The environment Σ maps proof constants to terms representing propositions. Our language of proof terms allows abstraction over proof and term variables, as well as application of proofs to proofs and terms. The abstractions correspond to the introduction of ⋀ and ⟹, while applications correspond to the elimination of these connectives. In contrast to polymorphic λ-calculi, no explicit application and abstraction is provided for types. To achieve a certain degree of polymorphism, we allow Σ(c) to contain free type variables and introduce the notation c_{[\overline{τ_{n}/α_{n}}]} to specify a suitable instantiation for them. The notion of provability can now be defined inductively as follows:

\begin{matrix}Γ, h : ϕ, Γ′ ⊢ h : ϕ & {Σ(c) = ϕ \atop Γ ⊢ c_{[\overline{τ_{n}/α_{n}}]} : ϕ[\overline{τ_{n}/α_{n}}]} \\ \begin{matrix}Γ, h : ϕ ⊢ p : ψ & Γ ⊢ ϕ :: prop \\ Γ ⊢ (λh : ϕ. p) : ϕ ⟹ ψ \end{matrix} & Γ, x :: τ ⊢ p : ϕ ; Γ ⊢ (λx :: τ. p) : ⋀ x :: τ. ϕ \\ \begin{matrix}Γ ⊢ p : ϕ ⟹ ψ & Γ ⊢ q : ϕ \\ Γ ⊢ (p q) : ψ \end{matrix} & \begin{matrix}Γ ⊢ p : ⋀ x :: τ. ϕ & Γ ⊢ t :: τ \\ Γ ⊢ (p t) : ϕ[t/x] \end{matrix} \end{matrix}

The judgement Γ ⊢ t :: τ used above expresses that the term t has type τ in context Γ. We will not give a formal definition of this judgement here, since it is well-known from simply typed lambda calculus.

3.2 Representing backward resolution proofs

This section explains how proof terms are constructed for proofs that are built up backwards by higher-order resolution as described by Paulson [8] and implemented in Isabelle. Although Isabelle also has LCF-like functions for forward proofs corresponding to the above inference rules, most proofs are constructed backwards without recourse to the forward rules. We now show how to augment these backward steps by proof terms. Thus the functions for backward resolution proofs need no longer be part of the trusted kernel of Isabelle.

In Isabelle, proof states are represented by theorems of the form

ψ_{1} ⟹ ⋯ ⟹ ψ_{n} ⟹ ϕ

where ϕ is the proposition to be proved and ψ_{1}, …, ψ_{n} are the remaining subgoals. Each subgoal is of the form ⋀ \overline{x}. \overline{A} ⟹ P, where \overline{x} and \overline{A} is a context of parameters and local assumptions.

Resolution A proof of a proposition ϕ starts with the trivial theorem ϕ ⟹ ϕ whose proof term is λv : ϕ. v. The initial proof state is then refined successively using the resolution rule

\begin{matrix}\begin{matrix}{P_{1} … P_{m} \atop C} & R \\ {P′_{1} … P′_{i} … P′_{m′} \atop C′} & R′ \end{matrix} ↦ θ \binom{P′_{1} … P′_{i−1} P_{1} … P_{m} P′_{i+1} … P′_{m′}}{C′} \\ where θ C = θ P′_{i} \end{matrix}

until a proof state with no more premises is reached. When refining a proof state having the proof term R′ using a rule having the proof term R, the proof term for the resulting proof state can be expressed by

θ (λ\overline{q_{i−1}} \overline{p_{m}}. R′ \overline{q_{i−1}} (R \overline{p_{m}}))

where θ is a unifier of C and P′_{i}. The first i − 1 abstractions are used to skip the first i − 1 premises of R′. The next m abstractions correspond to the new subgoals introduced by R.

Proof by assumption If the formula P_{j} in a subgoal ⋀ \overline{x_{k}}. \overline{P_{n}} ⟹ P_{j} of a proof state having the proof term R equals one of the assumptions in \overline{P_{n}}, this subgoal trivially holds and can therefore be removed from the proof state

\begin{aligned}Q_{1} … Q_{i−1} & ⋀ \overline{x_{k}}. \overline{P_{n}} ⟹ P_{j} & Q_{i+1} … Q_{m} \\ & C \end{aligned} ^{R} ↦ \begin{aligned}Q_{1} … Q_{i−1} & & Q_{i+1} … Q_{m} \\ & C \end{aligned}_{where 1 ≤ j ≤ n}

The proof term of the new proof state is obtained by supplying a suitable projection function as an argument to R:

λ\overline{q_{i−1}}. R \overline{q_{i−1}} (λ\overline{x_{k}} \overline{p_{n}}. p_{j})

Lifting rules into a context Before a subgoal of a proof state can be refined by resolution with a certain rule, the context of both the premises and the conclusion of this rule has to be augmented with additional parameters and assumptions in order to be compatible with the context of the subgoal. This process is called lifting. Isabelle distinguishes between two kinds of lifting: lifting over assumptions and lifting over parameters. The former simply adds a list of assumptions \overline{Q_{n}} to both the premises and the conclusion of a rule:

\begin{aligned}P_{1} & … & P_{m} \\ & C \end{aligned} ^{R} ↦ \begin{matrix}\overline{Q_{n}} ⟹ P_{1} & … & \overline{Q_{n}} ⟹ P_{m} \\ \overline{Q_{n}} ⟹ C \end{matrix}

The proof term for the lifted rule is

λ\overline{r_{m}} \overline{q_{n}}. R (\overline{r_{m} \overline{q_{n}}})

where the first m abstractions correspond to the new premises (with additional assumptions) and the next n abstractions correspond to the additional assumptions.

Lifting over parameters replaces all free variables a_{i} in a rule R [\overline{a_{k}}] by new variables a′_{i} of function type, which are applied to a list of new parameters \overline{x_{n}}. The new parameters are bound by universal quantifiers.

\begin{aligned}P_{1} [\overline{a_{k}}] & … & P_{m} [\overline{a_{k}}] \\ & C [\overline{a_{k}}] \end{aligned} ^{R [\overline{a_{k}}]} ↦ \begin{matrix}⋀ \overline{x_{n}}. P_{1} [\overline{a′_{k} \overline{x_{n}}}] & … & ⋀ \overline{x_{n}}. P_{m} [\overline{a′_{k} \overline{x_{n}}}] \\ ⋀ \overline{x_{n}}. C [\overline{a′_{k} \overline{x_{n}}}] \end{matrix}

The proof term for the lifted rule looks similar to the one in the previous case:

λ\overline{r_{m}} \overline{x_{n}}. R [\overline{a′_{k} \overline{x_{n}}}] (\overline{r_{m} \overline{x_{n}}})

3.3 Constructing an example proof

We will now demonstrate how a proof term can be synthesized incrementally while proving a theorem in backward style. A proof term corresponding to a proof state will have the general form

λ(g_{1} : ϕ_{1}) … (g_{n} : ϕ_{n})…. (g_{i} \overline{x^{i}} \overline{h^{i}}) …

where the bound variables g_{1}, …, g_{n} stand for proofs of the current subgoals which are still to be found. The \overline{x^{i}} and \overline{h^{i}} appearing in the proof term (g_{i} \overline{x^{i}} \overline{h^{i}}) are parameters and assumptions which may be used in the proof of subgoal i. As an example, the construction of a proof term for the theorem

(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)

will be shown by giving a proof term for each proof state. The parts of the proof terms, which are affected by the application of a rule will be underlined. Initially, the proof state is the trivial theorem:

step 0, remaining subgoal: (∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)

λg : ((∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)). g

We first apply rule impI. Applying a suitable instance of this rule to the trivial initial proof term yields

λg : (∃x. ∀y. P x y) ⟹ (∀y. ∃x. P x y).
(λg′ : ((∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)). g′)  } proof term from step 0
(\underbrace{impI (∃x. ∀y. P x y) (∀y. ∃x. P x y)}_{instance of impI} g)

and by βη reduction of this proof term we obtain

step 1, remaining subgoal: (∃x. ∀y. P x y) ⟹ (∀y. ∃x. P x y)

impI (∃x. ∀y. P x y) (∀y. ∃x. P x y)

We now apply allI to the above proof state. Before resolving allI with the proof state, its context has to be augmented with the assumption ∃x. ∀y. P x y of the current goal. The resulting proof term is

λg : (⋀ y. ∃x. ∀y. P x y ⟹ ∃x. P x y).
impI (∃x. ∀y. P x y) (∀y. ∃x. P x y)  } proof term from step 1
\begin{matrix}((λh_{2} : (∃x. ∀y. P x y ⟹ ⋀ y. ∃x. P x y). \\ λh_{1} : (∃x. ∀y. P x y). \\ allI (λy. ∃x. P x y) (h_{2} h_{1})) \end{matrix}  \} lifted instance of allI

\begin{matrix}(λh_{3} : (∃x. ∀y. P x y) \\ λy :: β. g y h_{3})) \end{matrix}  \} rearranging quantifiers

as before, we apply β reduction, which yields step 2, remaining subgoal: ⋀ y. ∃x. ∀y. P x y ⟹ ∃x. P x y

λg : (⋀ y. ∃x. ∀y. P x y ⟹ ∃x. P x y).

impI (∃x. ∀y. P x y) (∀y. ∃x. P x y)

(λh_{1} : (∃x. ∀y. P x y).

allI (λy. ∃x. P x y) (λy :: β. \underline{g y h_{1}}))

By eliminating the existence quantifier using exE we get step 3, remaining subgoal: ⋀ y x. ∀y. P x y ⟹ ∃x. P x y

λg : (⋀ y x. ∀y. P x y ⟹ ∃x. P x y).

impI (∃x. ∀y. P x y) (∀y. ∃x. P x y)

(λh_{1} : (∃x. ∀y. P x y).

allI (λy. ∃x. P x y)
(λy :: β. exE (λx. ∀y. P x y) (∃x. P x y) h_{1} (\underline{g y})))

Applying the introduction rule exI for the existential quantifier results in step 4, remaining subgoal: ⋀ y x. ∀y. P x y ⟹ P (?x y x) y

λg : (⋀ y x. ∀y. P x y ⟹ P (?x y x) y).

impI (∃x. ∀y. P x y) (∀y. ∃x. P x y)

(λh_{1} : (∃x. ∀y. P x y).

allI (λy. ∃x. P x y)
(λy :: β. exE (λx. ∀y. P x y) (∃x. P x y) h_{1}
(λx :: α.
λh_{2} : (∀y. P x y).
exI (λx. P x y) (?x y x) (\underline{g y x h_{2}}))))

We now eliminate the universal quantifier using allE, which yields step 5, remaining subgoal: ⋀ y x. P x (?y y x) ⟹ P (?x y x) y

λg : (⋀ y x. P x (?y y x) ⟹ P (?x y x) y).

impI (∃x. ∀y. P x y) (∀y. ∃x. P x y)

(λh_{1} : (∃x. ∀y. P x y).

allI (λy. ∃x. P x y)
(λy :: β. exE (λx. ∀y. P x y) (∃x. P x y) h_{1}
(λx :: α.
λh_{2} : (∀y. P x y).
exI (λx. P x y) (?x y x)
(allE (P x) (?y y x) (P (?x y x) y) h_{2} (\underline{g y x})))))

We can now prove the remaining subgoal by assumption, which is done by substituting the projection function λ(y :: β) (x :: α). λh_{3} : (P x y). h_{3} for g: step 6, no subgoals

impI (∃x. ∀y. P x y) (∀y. ∃x. P x y)

(λh_{1} : (∃x. ∀y. P x y).

allI (λy. ∃x. P x y)

(λy :: β. exE (λx. ∀y. P x y) (∃x. P x y) h_{1}

(λx :: α.
λh_{2} : (∀y. P x y).
exI (λx. P x y) x

(allE (P x) y (P x y) h_{2} (λh_{3} : (P x y). h_{3})))))

4 Partial proof terms

Proof terms are large, contain much redundant information, and need to be compressed. The solution is simple: leave out everything that can be reconstructed. But since we do not want to complicate reconstruction too much, it should not degenerate into proof search. Thus we have to keep the skeleton of the proof. What can often be left out are the ϕ, τ and t in λh:ϕ. p, λx::τ. p and (p t).

Since we will have to reconstruct the missing information later on, it is conceptually simpler to model the missing information by unification variables. These are simply a new class of free (term and type) variables, syntactically distinguished by a leading “?”, as in ?f and ?α. We will sometimes write ?f_{τ} to emphasize that ?f has type τ. Substitutions are functions that act on unification variables, e.g. θ = {?f ↦ λx.x,?α ↦ τ}.

In the remainder of this section we work with partial proofs, where terms and types may contain unification variables, as in (p ?f). Note that term unification variables that occur within the scope of a λ need to be “lifted” as in λx::τ. (p (?f x)). Because of this lifting, this partial information may take up more space than it saves. Therefore an actual implementation is bound to introduce separate new constructors for proof trees, e.g. λh: . p, λx:: . p and (p ), where represents the missing information. This is in fact what Necula and Lee describe [6]. However, it turns out that our partial proofs are easier to treat mathematically, not far from the “ ”-version, and also allow to drop only part of a term (although we will not make use of this feature).

Of course, we cannot check partial proofs with the rules of §3.1. In fact, we may not be able to check them at all, because too much information is missing. But we can collect equality constraints that need to hold in order for the proof to be correct. Such equality constraints are of the form T_{1} =^{?} T_{2}, where T_{1} and T_{2} are either both terms or both types. A substitution solves a constraint if the two terms become equal modulo βη-conversion, or if the two types become identical. Sets of such equality constraints are usually denoted by the letters C and D. To separate C into term and type constraints, let C_{t} denote the term and C_{τ} the type part. The subscripts t and τ do not refer to variable names but are simply keywords.

We will now show how to extract a set of constraints from a partial proof; how to solve those constraints is discussed later on.

4.1 Collecting constraints

The relation Γ ⊢ p ⊳ (ϕ, C) is a partial function taking Γ and a partial proof p and producing a formula ϕ (which may contain unification variables) and a set of constraints C. The function will be defined such that, if θ solves C, then θ(p) proves θ(ϕ). The notation \overline{V_{Γ}} denotes the list of all term variables declared in Γ, and \overline{τ_{Γ}} denotes the list of their types, i.e. \overline{V_{Γ}} = x_{1} … x_{n} and \overline{τ_{Γ}} = τ_{1} … τ_{n} for Γ = x_{1} :: τ_{1} … x_{n} :: τ_{n}.

Γ′, h : ϕ, Γ ⊢ h ⊳ (ϕ, ∅)  {Σ(c) = ϕ \atop Γ ⊢ c_{[\overline{τ_{n}/α_{n}}]} ⊳ (ϕ[\overline{τ_{n}/α_{n}}], ∅)}

\begin{matrix}Γ, h : ϕ ⊢ p ⊳ (ψ, C) & Γ ⊢ ϕ ⊳ (τ, D) \\ Γ ⊢ (λh:ϕ. p) ⊳ (ϕ ⟹ ψ, C ∪ D ∪ \{τ =^{?} prop\}) \end{matrix}

Γ, x :: τ ⊢ p ⊳ (ϕ, C) ; Γ ⊢ (λx::τ. p) ⊳ (⋀ x :: τ. ϕ, {λx :: τ. r =^{?} λx :: τ. s | (r =^{?} s) ∈ C_{t}} ∪ C_{τ})

Γ ⊢ p ⊳ (ϕ, C) Γ ⊢ q ⊳ (ψ, D)
Γ ⊢ (p q) ⊳ (?f_{\overline{τ_{Γ}} →prop} \overline{V_{Γ}} , \{ϕ =^{?} (ψ ⟹ ?f_{\overline{τ_{Γ}} →prop} \overline{V_{Γ}})\} ∪ C ∪ D)
Γ ⊢ p ⊳ (ϕ, C) Γ ⊢ t ⊳ (τ, D)

Γ ⊢ (p t) ⊳ (?f_{\overline{τ_{Γ}} →τ→prop} \overline{V_{Γ}} t, \{ϕ =^{?} ⋀ x :: τ. ?f_{\overline{τ_{Γ}} →τ→prop} \overline{V_{Γ}} x\} ∪ C ∪ D)

As usual, the unification variables ?f must be “new” in each case.

The above rules follow those in §3.1 very closely. For example, the intuition behind the rule for the application (p q) is the following: if p proves proposition ϕ, then ϕ must be some implication and the proposition ψ proved by q must be the premise of this implication. Moreover, the proposition proved by (p q) is the conclusion of the implication. The set of constraints for (p q) is the union of the constraints for p and q, plus one additional constraint expressing that ϕ is a suitable implication. One point to note is the judgement Γ ⊢ t ⊳ (τ, D) used in two premises of the constraint collection rules. It corresponds to Γ ⊢ t :: τ just like Γ ⊢ p ⊳ (ϕ, C) corresponds to Γ ⊢ p :: ϕ, i.e. D is a set of type constraints whose solvability implies that t has type τ. The rules for Γ ⊢ t ⊳ (τ, D) are not given because they are well-known: both from the literature about type inference for simply typed terms and because they closely resemble the rules above, just one level down. In a setting where types, terms and proofs are not syntactically distinguished, we would only have one judgement . ⊢ . ⊳ (., .).

We introduce the notation (ϕ, C) = collect(Γ, p) as a functional variant of Γ ⊢ p ⊳ (ϕ, C).

Example 1. Let p = λx :: ?α_{1}. λh_{1} : (?f_{?α_{2}} x). λy :: ?α_{3}. λh_{2} : (?f′_{?α_{4}} x y). h_{1} h_{2} y

Then

collect([], p) = (⋀ x :: ?α_{1}. ?f_{?α_{2}} x ⟹ ⋀ y :: ?α_{3}. ?f′_{?α_{4}} x y ⟹
?g′_{?α_{1}→?α_{3}→?α_{3}→prop} x y y,
{λx :: ?α_{1}.λy :: ?α_{3}. ?f_{?α_{2}} x =^{?}
λx :: ?α_{1}.λy :: ?α_{3}. ?f′_{?α_{4}} x y ⟹ ?g_{?α_{1}→?α_{3}→prop} x y,
λx :: ?α_{1}.λy :: ?α_{3}). ?g_{?α_{1}→?α_{3}→prop} x y =^{?}
λx :: ?α_{1}.λy :: ?α_{3}). ⋀ z :: ?α_{3}. ?g′_{?α_{1}→?α_{3}→?α_{3}→prop} x y z,
?α_{2} =^{?} ?α_{1} → ?β_{1}, ?β_{1} =^{?} prop
?α_{4} =^{?} ?α_{1} → ?α_{3} → ?β_{2}, ?β_{2} =^{?} prop})

where ?g, ?g′ and ?β_{i} are new variables generated during constraint collection.

Theorem 1. (Soundness and completeness)

1. If Γ ⊢ p ⊳ (ϕ′, C) and θ solves C then θ(Γ) ⊢ θ(p) : θ(ϕ′).

2. If Γ ⊢ p : ϕ and Γ ⊢ p ⊳ (ϕ′, C) then C ∪ {ϕ =^{?} ϕ′} is solvable.

This theorem shows the advantage of working with partial proofs as opposed to proofs containing “ ”: we can produce the full proof by instantiation from the partial one.

Thus there are two possible system architectures for checking partial proofs:

• either constraint collection Γ ⊢ p ⊳ (ϕ′, C) and constraint solving are part of the trusted kernel and θ(ϕ′) is accepted as the correct answer;

• or, for the security conscious, neither collecting nor solving is part of the trusted kernel and their result is checked by checking θ(Γ) ⊢ θ(p) : θ(ϕ′).

4.2 Solving constraints

Our constraints are a mixture of term and type constraints. Type constraints can be solved by first-order unification and thus do not need to be discussed here: they can be solved at any time in any order. Therefore we concentrate on term constraints in this subsection.

Since higher-order unification is undecidable, we restrict to unification of so called (higher-order) patterns [4], i.e. λ-terms where each occurrence of a unification variable is applied only to distinct bound variables. For example λxy.?F y x is a pattern, whereas λx.?F x x and ?F a are not patterns. The set of all patterns is denoted by Pat. For us, the key property of patterns is that their unification is decidable and that solvable pattern unification problems have most general unifiers [4, 12, 7, 13]. Thus we may assume a function mgu taking two patterns as arguments and either failing or returning the most general unifier of its arguments.

Since the constraints C generated by Γ ⊢ p ⊳ (ϕ, C) may contain nonpatterns, we have to delay solving those constraints until (hopefully) they are turned into patterns by the solution of other pattern constraints. Of course, in the worst case C may not contain any patterns at all, in which case we have to give up. Thus we have to take care when constructing partial proofs to make sure the complete proof can be reconstructed by pattern unification.

Example 2. The first constraint in {?f ?z =^{?} ?z, λxy.?f x =^{?} λxy.?f y} is not a pattern constraint, but if the second constraint is solved first, it yields the substitution ?f ↦ λx.?u, which turns the first constraint into the trivial ?u =^{?} ?z.

We say that a set of equality constraints C can be solved by pattern unification if C ⟶^{∗} ∅, where ⟶ is defined by the rewrite rule

C ∪ {s =^{?} t} ⟶ θ(C)

where s and t are patterns and mgu(s, t) returns the unifier θ. Note that the choice of which pair s =^{?} t to solve at which point is immaterial because ⟶ is confluent. This is well-known for first-order terms, and holds for patterns as well because of the existence of most general unifiers and the following easy results:

Lemma 1. 1. If s, t ∈ Pat and mgu(s, t) returns θ then Ran(θ) ⊆ Pat.

2. If Ran(θ) ⊆ Pat and u ∈ Pat then θ(u) ∈ Pat.

4.3 Compressing proof terms

The basic idea here is straightforward: given a proof term, remove all of the information that can be reconstructed by unification. If our meta logic were Prolog (i.e. proof terms contain no λs), we could drop all terms t in an application (p t), because first-order unification can reconstruct them. In our setting we require that pattern unification should be able to reconstruct the missing terms.

Compression is performed in three phases. First, all terms and types in the proof are replaced by suitably lifted unification variables. A substitution reversing the term abstractions is constructed as well.

varify(\overline{x}, \overline{τ}, λv:ϕ. p) = let (p′, θ) = varify(\overline{x}, \overline{τ}, p)
in (λv:(?f_{\overline{τ}→prop} \overline{x}). p′, θ ∪ \{?f ↦ λ\overline{x}.t\})
varify(\overline{x}, \overline{τ}, λy::τ. p) = let (p′, θ) = varify(\overline{x}y, \overline{τ} ?α, p)
in (λy::?α. p′, θ)
varify(\overline{x}, \overline{τ}, (p q)) = let (p′, θ) = varify(\overline{x}, \overline{τ}, p); (q′, θ′) = varify(\overline{x}, \overline{τ}, q)
in ((p′ q′), θ′)
varify(\overline{x}, \overline{τ}, (p t)) = let (p′, θ) = varify(\overline{x}, \overline{τ}, p)
in ((p′ (?f_{\overline{τ}→?β} \overline{x})), θ ∪ \{?f ↦ λ\overline{x}.t\})
varify(\overline{x}, \overline{τ}, c_{[\overline{τ_{n}/α_{n}}]}) = (c_{[\overline{?α_{n}/α_{n}}]}, ∅)

Thus varify(\overline{x}, \overline{τ}, p) = (p′, θ) does not quite imply θ(p′) = p because θ does not reverse the type abstractions: types are first-order and thus they can be reconstructed uniquely by unification.

Then the constraints are extracted from the resulting partial proof: (ϕ′, C) = collect(Γ, p′). Finally we compute (with the help of function solves) a minimal set of term variables V ⊆ Dom(θ) such that θ(C) can be solved by pattern unification. Thus the overall algorithm for compressing a proof p is

compress(p, ϕ) = let (p′, θ) = varify([], [], p) (ϕ′, C) = collect([], p′) V = solves(C ∪ {ϕ =^{?} ϕ′}, θ) in θ|_{V} (p′)

where θ|_{V} is the restriction of θ to V. Function solves(D, θ) returns V ⊆ Dom(θ) such that θ|_{V} (D) is solvable by pattern unification. The details are explained below.

The main correctness theorem expresses that compression does not lose any information in the following sense: the constraints collected from the compressed version of a valid proof are solvable by pattern unification and any solution yields a proof of the original formula.

Theorem 2. Let ϕ be ground. If ⊢ p : ϕ, q = compress(p, ϕ) and (ψ, C) = collect([], q) then 1. C ∪ {ϕ =^{?} ψ} is solvable by pattern unification and

2. if θ solves C ∪ {ϕ =^{?} ψ} then ⊢ θ(q) : ϕ.

The second part of the theorem follows directly from the soundness of collect (part 1 of Theorem 1) because ϕ is ground, i.e. θ(ϕ) = ϕ.

The fact that C ∪ {ϕ =^{?} ψ} is solvable by pattern unification is a bit more subtle. From q = compress(p, ϕ) it follows by definition of compress that there are p′, θ, ϕ′, C′ and V such that (p′, θ) = varify([], [], p), (ϕ′, C′) = collect([], p′), V = solves(C′ ∪ {ϕ =^{?} ϕ′}, θ) and q = θ|_{V} (p′). Because (ψ, C) = collect([], q) = collect([], θ|_{V} (p′)) and (ϕ′, C′) = collect([], p′) it can be shown that ψ = θ|_{V} (ϕ′) and C = θ|_{V} (C′). Thus C ∪ {ϕ =^{?} ψ} = θ|_{V} (C′ ∪ {ϕ =^{?} ϕ′}). It can be shown that θ(C′∪{ϕ =^{?} ϕ′}) is solvable by pattern unification. Appealing to Theorem 3 below, it follows that so is C ∪ {ϕ =^{?} ψ}.

Theorem 3. If θ(C) is solvable by pattern unification, then solves(C, θ) terminates successfully with a set of variables V such that θ|_{V} (C) is solvable by pattern unification.

This can be viewed as a specification of solves or as its main correctness theorem. Of course there are trivial implementations of solves that simply return Dom(θ). What we want is a minimal set V with the stated property. Note that in general there is no least such V:

Example 3. Let C = {λx.?f(?g(x)) =^{?} λx.f(x)} and θ = {?f ↦ f,?g ↦ λx.x}. Then θ(C), θ|_{{?f}}(C) and θ|_{{?g}}(C) are solvable by pattern unification.

Therefore solves nondeterministically computes a minimal set of variables by simulating the process of solving the constraints by pattern unification. Every time the process gets stuck, i.e. no more pattern constraints are left, a minimal set of additional variables is instantiated.

The main complication is that pattern unification may introduce new variables. Thus we need to keep track of where they came from, i.e. which original variable needs to be instantiated in order to ensure that the new variable becomes instantiated. Again, there may be a choice:

Example 4. Let C = {λxyz.?f z x =^{?} λxyz.?g x y} ∪ C′ and let θ = {?f ↦ λxy.f y,?g ↦ λxy.f x} ∪ θ′. Solving the first constraint in C yields the substitution σ = {?f ↦ λxy.?h y,?g ↦ λxy.?h x}. Now we need to compute the value of ?h (in case it is required later on in order to continue) and we need to record that ?h depends on either ?f or ?g, i.e. instantiating ?f or ?g will instantiate ?h. We can chose to record either dependency.

In the algorithm below, this dependency relation is stored in a partial function D mapping new variables to old ones they depend on.

Finally we introduce some terminology to select those variables that occur in non-pattern positions: given an equality constraint st, N PVars(st) is the set of variables ?f that occur in subterms of the form ?f \overline{u} in st, such that \overline{u} is not a list of distinct bound variables.

Now we can describe solves(C, θ) as an imperative algorithm. As long as there are pattern problems left in C, we solve them and propagate the solution. Once we are left only with non-pattern problems, we pick one such that values for all its non-pattern variables are known (via θ). All those variables are then instantiated and recorded in V. If there is no such non-pattern problem either, the algorithm fails. Luckily, Theorem 3 tells us that this will not happen in the cases we are interested in.

V := ∅; D := {?f ↦ ?f | ?f ∈ Var(C)}

   while C ≠ ∅ do

if there is a pattern problem (s =^{?} t) ∈ C then σ := mgu(s, t); C := σ(C − {s =^{?} t});

          forall (?f ↦ t) ∈ σ do

\begin{matrix}δ := mgu(θ(?f), θ(t)); \\ D := D ∪ \{?h ↦ D(?f) | ?h ∈ Dom(δ)\} \end{matrix}

          od

else pick some st ∈ C such that N PVars(st) ⊆ Dom(θ); V := V ∪ {D(?f) | ?f ∈ N PVars(st)}; C := θ|_{N PVars(st)}(C);

   od;
   return V

Note that the else-case does not necessarily compute a minimal V: if st = (λxy.?f x (?g y y) =^{?} λxy.x} and θ(?f) = λxy.x and θ(?g) = λxy.x then it suffices to instantiate either ?f or ?g, whereas above both are added to V. The above algorithm can be refined by instantiating st stepwise from the top and normalizing the result each time.

5 Implementation

The algorithms for compression and reconstruction of proofs have been implemented in ML as a part of the theorem prover Isabelle. During the proof of a theorem, the corresponding proof term is built up incrementally. Since this may slow down the execution of proof scripts, the generation of proof terms can be switched on and off as needed: during the interactive development of a proof this feature may be switched off. When the proof is completed, the proof script may be re-run with proof generation switched on and the resulting proof term could be exported.

We have tested the implementation on several proofs of theorems in Pelletier’s collection [10], which were generated by Isabelle’s tableau prover. The following table summarizes some results^{1}. It shows the number of terms (i.e. terms such as ϕ and t in λh:ϕ. p and (p t)) occurring in the uncompressed proof term, as well as the number of terms occurring in the compressed proof term (i.e. terms not replaced by placeholders “ ”, as explained in §4). In all cases, the compression

1 These measurements were done on a Pentium II with 400 MHz and 512 MB RAM

ratio was more than 90%. The compression rate reported by Necula and Lee [6] appears to be a little better, but that is probably because we counted only the number of terms, not their size: our dynamic compression scheme should drop at least as much as Necula and Lee’s static scheme.

number of terms  reconstruction
uncompressed compressed compression  time [s]
52  4  92.3%  0.030
116  6  94.8%  0.120
170  9  94.7%  0.190
316  16  94.9%  0.360
425  31  92.7%  0.710
1948  142  92.7%  5.220
2345  153  93.5%  5.950

The following diagram shows the correspondence between the number of terms in the uncompressed proof term and the time needed for reconstruction.

A crucial point is the efficient handling of large sets of constraints: when having computed a unifier for a constraint, one possibility is to apply this unifier to all the remaining constraints. Another possibility is to accumulate the unifiers and only apply them when needed. The first solution can be rather slow when having a large number of constraints, while the second solution—which has been chosen in our implementation—requires efficient data structures for storing substitutions. To speed up reconstruction, our implementation of function collect described in §4.1 tries to solve newly introduced constraints immediately, instead of collecting all constraints first and then solving them at the end.

6 Conclusion

We have given a first presentation of proof terms for simply typed intuitionistic higher-order logic, an important logical framework. We hope that by unfolding the underlying type theory and explicitly isolating the simply typed components familiar to users of Isabelle or HOL, this may popularize the λ-calculus view of proofs in those quarters as well. We have also presented what appears to be a novel compression scheme for proofs. Hence our work provides a new and promising basis for exchanging proofs in simply typed logics, in particular HOL, both among theorem provers (especially automatic and interactive) and in the realm of proof carrying code.

References

[1] H. P. Barendregt. Lambda calculi with types. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 118–309. Oxford University Press, 1992.

[2] B. Barras, S. Boutin, C. Cornes, J. Courant, Y. Coscoy, D. Delahaye, D. de Rauglaudre, J.-C. Filliâtre, E. Giménez, H. Herbelin, G. Huet, H. Laulhère, C. Muñoz, C. Murthy, C. Parent-Vigouroux, P. Loiseleur, C. Paulin-Mohring, A. Saïbi, and B. Werner. The Coq proof assistant reference manual – version 6.3.1. Technical report, INRIA, 1999.

[3] M. J. C. Gordon, J. M. J. Herbert, R. W. S. Hale, J. Harrison, W. Wong, and J. von Wright. Self-checking prover study – final report. Technical report, SRI, 1995.

Available at http://www.csl.sri.com/reports/postscript/proofchecker.ps.
gz.

[4] D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497–536, 1991.

[5] G. C. Necula. Proof-carrying code. In Conference Record of POPL ’97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 106–119. ACM Press, New York, 1997.

[6] G. C. Necula and P. Lee. Efficient representation and validation of proofs. In 13th IEEE Symp. Logic in Computer Science (LICS’98), pages 93–104. IEEE Computer Society Press, 1998.

[7] T. Nipkow. Functional unification of higher-order patterns. In 8th IEEE Symp. Logic in Computer Science, pages 64–74. IEEE Computer Society Press, 1993.

[8] L. C. Paulson. The foundation of a generic theorem prover. Journal of Automated Reasoning, 5:363–397, 1989.

[9] L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of LNCS. Springer, 1994.

[10] F. J. Pelletier. Seventy-five problems for testing automatic theorem provers. Journal of Automated Reasoning, 2:191–216, 1986.

[11] F. Pfenning. Logic programming in the LF Logical Framework. In G. Huet and G. Plotkin, editors, Logical Frameworks, pages 66–78. Cambridge University Press, 1991.

[12] F. Pfenning. Unification and anti-unification in the calculus of constructions. In 6th IEEE Symposium on Logic in Computer Science, pages 74–85. IEEE Computer Society Press, 1991.

[13] Z. Qian. Unification of higher-order patterns in linear time and space. Journal of Logic and Computation, 6:315–341, 1996.

[14] W. Wong. Recording and checking HOL proofs. In E. Schubert, P. Windley, and J. Alves-Foss, editors, Higher Order Logic Theorem Proving and Its Applications. 8th International Workshop, volume 971 of LNCS, pages 353–68. Springer-Verlag, Berlin, 1995.