A Short Article for the Newsletter of the ALP (Appeared August 1991)

Proof Theory as an Alternative to Model Theory

Dale Miller

LFCS, University of Edinburgh and CIS, University of Pennsylvania

The design and analysis of declarative programming languages require that computation be described in two separate ways: by an interpreter that extracts values from a program and by a declarative specification of what values should be attributed to a program. A soundness theorem for a programming language states that its interpreter computes only attributed values and a completeness theorem states that the interpreter extracts all such values. For example, in the logic programming literature, SLD-resolution is often used to define an interpreter that extracts values from a Horn clause program while minimal Herbrand models attribute values to programs. Since these two concepts -- resolution and model theory -- are very different, soundness and completeness theorems give us some confidence that Horn clause programming is not "hacky" and that they will have useful meta-level properties. Such meta-level properties can then be exploited in sophisticated program manipulations (e.g., partial evaluation, fold/unfold), in implementations on different models of computation (e.g., sequential, parallel), and in the proofs of program correctness. The separate descriptions of what values are extracted by an interpreter from a program and what values should be attributed to a program gives declarative programming languages their character.

A largely unquestioned assumption of the logic programming literature is that model theory is the appropriate tool for describing how values should be attributed to programs. Of course, Tarskian semantics has had a number of successful application in not only mathematical logic but also computer science. However, there are at least two reasons to worry about this "unquestioned" use of model theory. First, model theory itself does not seem to be devoid of ad hoc constructions. There now seems to be sufficient semantic muscle available to language designers that nearly any syntactic system can be given a sound and complete model theoretic semantics. Since some models are better than others, language designers cannot simply refer to soundness and completeness results as justifying a particular programming language design. Second, many aspects of model theory employ various forms of infinity that are rather remote from the study of the finite mechanisms employed within any computer system.

While model theory is very flexible and has been employed to characterize a great many phenomena, including many relevant to computation (e.g., denotational semantics), it seems natural to ask whether or not there are more direct and computationally oriented approaches to the semantics of declarative programming languages. One such approach has grown out of the "constructive" or "proof theoretic" approach to reducing mathematics to very weak logical principles. In such a setting, infinities are left as a last resort and properties of finite constructions are analyzed directly. Within this framework, proof normalization and cut-elimination have become central concepts in judging the declarative nature of formal systems. For example, it is possible to justify the concept of SLD-resolution by showing that it can be used to discover proofs in a particular sequent proof system. Since that proof system satisfies the cut-elimination property, many of the desirable meta-level properties of Horn clauses follow. Such an approach also permits direct analysis of logic programming in a wide range of logics, including intuitionistic and linear logics.

While there have been several recent papers in which proof-theoretic analysis has been used to analyze logic programming languages, the subject of proof theory and the related notions of intuitionistic logic and linear logic do not seem to be well known to the logic programming community. Below are listed some books and articles that provide introductions to these subjects.

(1) Handbook of mathematical logic, edited by Jon Barwise, New York: North-Holland Pub. Co. 1977. Part D is titled "Proof Theory and Constructive Mathematics." Particularly relevant is the article "Proof theory: Some applications of cut-elimination" by Helmut Schwichtenberg.

(2) Jean H. Gallier, Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row, 1986.

(3) Collected Papers of Gerhard Gentzen, edited by M. E. Szabo, North-Holland Publishing Co., Amsterdam, 1969. Of particular importance is the paper "Investigations into Logical Deductions" (1935) which is remarkably readable even after so many years.

(4) Jean-Yves Girard, Paul Taylor, and Yves Lafont, Proofs and Types. Cambridge University Press, 1989.

(5) Bengt Nordstrom, Kent Petersson and Jan M. Smith, Programming in Martin-Lof's type theory: An introduction. Oxford : Clarendon 1990.

(6) Dag Prawitz, Natural Deduction. Almqvist & Wiksell, Uppsala, 1965.

(7) To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, edited by J. P. Seldin and R. Hindley, Academic Press, 1980. The article by Howard titled ``The formulae-as-type notion of construction'' is elementary and readable.