A Short Article for the Newsletter of the ALP (Appeared August 1991)
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.
(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.