Relative Completeness for Logics of Functional Programs

程序逻辑在计算机科学中扮演着重要的角色，是对测试的补充。程序逻辑允许人们证明程序满足给定的规范。20世纪70年代初，Hoare在有状态程序的公理语义学方面做了开创性的工作。从那时起，为各种编程语言开发了许多演算，同时在许多验证工具中存在这些逻辑的机械化。程序逻辑的两个性质特别令人感兴趣：可靠性，即人们可以证明的微积分中程序的任何性质实际上都是有效的。完备性说明了相反的情况，即也可以派生任何有效的属性。在理想世界中，程序逻辑的形式化演算应该既健全又完整，从而忠实而完整地反映程序的语义和正确性断言，也称为规范。然而，由于歌德尔的不完备性定理，寻找(绝对)完全程序逻辑是没有希望的，因为对于任何形式系统S，总是存在一个正确断言是真的，但不能在S中证明。尽管如此，人们可能会问，一些程序逻辑的公理是否足以推导出相对于某个完整数据理论的所有真正确断言，例如所有一阶算术的真语句。这首先针对简单命令式语言进行了研究，其中规范是所谓的Hoare三元组，形式为{P}C{Q}，其中C是程序，P是前置条件，Q是后置条件。这样的三元组表示，如果C在满足P的状态下运行并终止，则得到的新状态将满足断言Q。然后，Hoare演算提供了一组规则和公理，即如何推导出这样的三元组。证明程序满足由前置条件和后置条件给出的特定规范。库克在他的开创性论文中为Hoare逻辑的一个简单变体建立了这种逻辑的相对完备性。他证明了，如果我们被允许使用一阶算术的所有真句子作为公理，那么所有形式为{P}C{Q}的正确的部分正确性断言都可以使用Hoare逻辑的规则来推导。这样做的原因是，一阶算术的语言足够强大，可以用一阶算术的公式来表示所有程序P的输入/输出关系。然而，程序逻辑也对函数式程序感兴趣。流行的函数式编程语言有ML、Caml或Haskell。纯函数式语言不使用状态，而是使用递归定义的数据结构和高阶函数。就我们所知，函数式程序设计语言的逻辑是否具有相对完备性的问题还没有得到系统和深入的研究。因此，本项目将研究D·斯科特的LCF(或其扩展)等逻辑。经验告诉我们，大多数纯功能程序的验证都可以在LCF中表达。但是，在LCF中也很容易找到既不能证明也不能反驳的断言，比如“PARALLEL OR”规范。原因很简单，因为前者适用于斯科特模型，但其否定适用于完全抽象的模型。重要的是要注意，这两个模型并不是不同的w.r.t.自然数的数据类型NAT(以及NAT上一元函数的数据类型NAT)，但它们在较高类型上确实不同。因此，询问LCF是否相对完整是没有意义的。不同于基本的命令式语言，它不能完全确定模型的(更高类型的部分)。因此，正确的问题，也是我们在这个项目中要解决的一个问题是，PCF的“自然”模型是否可以有很好的完全公理。

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.