Proofs, Search and Computation in General Logic

David Pym

Abstract: The Logical Framework (LF) is a formal system for the representation of logics and formal systems as theories within it, which was developed by Harper, Honsell and Plotkin. The LF consists of two components: the lambda Pi-calculus, the lambda-calculus with dependent function space (or product) types; and the principle of judgements as types in which judgements, the units of inference in logics and other formal systems, are identified with the types of the lambda Pi-calculus. This work is strongly influenced by the work of Martin-Löf on judgements in logic. The LF is suitable for mechanical implementation because the lambda Pi-calculus is decidable.

We present a theory of search and logic programming for the lambda Pi- calculus and consequently for logics which are adequately represented in the LF.

The presentation of the lambda Pi-calculus of Harper, Honsell and Plotkin is as a (linearized) natural deduction system. The search space induced by such a system is highly non-deterministic and so the first step is to define a Gentzenized system, in which the natural deduction style pi-elimination rule is replaced by a sequent calculus style Pi-elimination rule, which is sound and complete with respect to the system of Harper, Honsell and Plotkin.

The Gentzenized system thus provides the foundation for a metacalculus, possessing an important subformula property, for the inhabitation assertions of the lambda Pi-calculus which forms a suitable basis for proof-search in the lambda Pi-calculus. By exploiting the structure of a form of hypothetico-general judgement, we are able to obtain (complete) calculi based on certain forms of resolution rule, the search spaces of which are properly contained within that of our basic metacalculus. Furthermore, we are able to further constrain proof-search in these calculi by considering a certain uniform form for proofs.

We develop a unification algorithm for the lambda Pi-calculus by extending the work of Huet for the simply-typed lambda-calculus. We use this unification algorithm to allow us to eliminate non-deterministic choices of terms, when performing proof-search with the Pil) or resolution rules. This is done by the introduction of a class of universal variables which are later instantiated via the unification algorithm.

When unification is used to instantiate universal variables well-formedness may not be preserved. However, by extending the work of Bibel and Wallen (for first-order classical, modal and intuitionistic logics) to the lambda Pi-calculus we are able to obtain a theory which allows to accept as many such instantiations as possible by detecting when the derivation can be reordered in order to yield a well-formed proof.

We extend the theory described above to provide a notion of logic programming by admitting universal variables in endsequents: these are analogous to the logical variables of PROLOG . Finally, we provide a denotational semantics for our logic programs by performing a least fixed point construction in a collection of Herbrand interpretations - maps from \parallel C Sigma \parallel to (families of) sets of terms in \parallel \cal F \parallel, where C Sigma is the syntactic category constructed out of the lambda Pi-calculus with signature Sigma, and \cal F is the category of families of sets. This construction is similar to one of Miller, and exploits a Kripke-like satisfaction predicate. We characterize this construction in terms of the model theory of the lambda Pi-calculus using the Yoneda functor.
PhD thesis - price £10.00

LFCS report ECS-LFCS-90-125 (also published as CST-69-90)

Previous | Index | Next