Relative Completeness for Logics of Functional Programs

点击翻译按钮获取中文摘要

Program logics play an important role in Computer Science to complement testing. A program logic allows one to prove that a program satisfies a given specification. Seminal work has been done in the early seventies by Hoare on axiomatic semantics for stateful programs. Since then many calculi have been developed for all kinds of programming languages and meanwhile mechanizations of these logics in numerous verification tools exist. Two properties of a program logic are of particular interest: Soundness states that any property one can prove of a program in the calculus is actually valid. Completeness states the converse, namely that any valid property can also be derived. In an ideal world, a formal calculus for a program logic would be both, sound and complete, thus faithfully and completely reflecting the semantics of programs and correctness assertions, also called specifications. However, due to Goedel's Incompleteness Theorem it is hopeless to look for (absolutely) complete program logics since for any formal system S there always exists a correctness assertion which is true but cannot be proved in S.In spite of this, one might ask whether the axioms of some program logic are sufficient to derive all true correctness assertions relative to some complete theory of data as e.g. all true sentences of first order arithmetic. This was first investigated for simple imperative languages where specifications are so-called Hoare triples, of the form {P}C{Q} where C is a program, P the pre-condition, and Q the post-condition. Such a triple states that if C is run in a state fulfilling P and terminates, the resulting new state will meet assertion Q. The Hoare-calculus then provides a set of rules and axioms how one can derive such triples, ie. proofs that programs meet a certain specification given by pre- and post-conditions.The property of relative completeness for such a logic was established by Cook in his seminal paper for a simple variant of Hoare logic. He showed that all correct partial correctness assertions of the form {P}C{Q} can be derived using the rules of Hoare's logic provided we are allowed to use all true sentences of first order arithmetic as axioms. The reason for this is that the language of first order arithmetic is strong enough to express for all programs P its input/output relation by a formula of first order arithmetic.Program logics, however, are also of interest for functional programs. Popular functional programming languages are ML, Caml, or Haskell. Pure functional languages do not use state but recursively defined data structures and higher-order functions on them. To the best of our knowledge the question whether relative completeness holds for logics of functional programming languages has not been investigated systematically and thoroughly. Therefore, this project will investigate logics such as D. Scott's LCF (or extensions of it). Experience tells us that verification of most purely functional programs can be expressed within LCF. But it is also easy to find assertions which can neither be proved nor disproved within LCF, like the specification of 'parallel or'. The reason simply is that the former holds in the Scott model but its negation holds in the fully abstract model. It is important to note that these two models are not different w.r.t. the data type NAT of natural numbers (and also the data type NAT->NAT of unary functions on NAT) but they do differ at higher types. Accordingly, it does not make sense to ask whether LCF is relatively complete w.r.t. to a full axiomatization of its first order part since the latter -- unlike for a basic imperative language -- does not fully determine the (higher type part of the) model.Thus, the right question, the one we will tackle in this project, is whether 'natural' models for PCF can have nice complete axiomatizations.