Representing constructive theories in high-level programming languages (logic)
Ryan D. Stansifer · 1985
This thesis concerns certain constructive theories we call programming logics. A programming logic is a strongly typed, functional programming language. Its semantics can be defined by a set of rewrite rules. We consider only programming logics in which predicate logic can be embedded, thus justifying the use of the term Furthermore, we single out those programming logics for which proofs of existential formulas have a canonical form explicitly revealing the witness. Thus, only constructive theories can be represented in these programming logics, and proofs in programming logics are executable. Three programming logics are described in this thesis. The first is based on HA('(omega)) (Heyting arithmetic of the omega order). The second is based on a Martin-Lof style type theory. The third is based on intuitionistic set theory. These programming logics have been implemented in the programming language ML (described in detail in this thesis). The core of each implementation is the same, and this logic engine, written in ML, is described in an appendix. Programming logics would be woefully inadequate as a basis for automatic deduction without provision for reasoning at a higher plane. We show how to implement proof strategies for programming logics. As an example, we show how PROLOG, or more precisely, linear input resolution could be implemented as a proof strategy for a programming logic. Finally, we demonstrate how certain elements of classical logic can be used in proof development and then eliminated in these cases. The experience gained in implementing these programming logics and described in this thesis contributes to the design of theories in which proofs are to be executable. The techniques of implementation demonstrated in this thesis can be used to build prototypes of a wide variety of theories. The ease in experimenting with new theories and the clarity with which the underlying mechanisms can be discussed are due to the representation of these theories at the level of abstract syntax and the directness by which the representation has been implemented in ML.