A Mechanizable Theory for Existence Proofs of Inclusive Predicates

CMU-CS-85-149

Ketan Mulmuley

July 1985

The Scott-Stachey approach to language semantics is well known. In this approach, a language is given semantics by mapping each language construct to its meaning in an appropriately constructed mathematical domain - this map is called denotational semantics of the language. The map is denotational in the sense that a denotation of a complex term depends only on the denotations of its constituents and not their structure. Of course, if the language is to be of any use at all, it must have an operational semantics. Generally this operational semantics is specified in terms of a compiler or an interpreter.

The question which arises is: are the denotational and operational semantics equivalent? This is the problem of semantic equivalence. Milne and Reynolds gave a general technique for proving such semantic equivalences. Their technique involves constructing certain predicates, called inclusive predicates, which connect the domains used for denotational and operational semantics. The most difficult part of their technique is showing the existence of such inclusive predicates. Unfortunately these existence proofs are known to be quite complicated, hence one is reluctant to carry out these proofs. Moreover, so far nobody has known any nontrivial example of a system of equations over inclusive predicates which does not have a solution. In the absence of such a counterexample it does not seem justified to carry out the complicated existence proofs with all their details. In this paper we shall construct such a counterexample through diagonalization. This means one must carry out the existence proofs with care. For quite a long time many people had expressed a need for much simpler methods for proving these existences. For example, several people suggested that there might be a language which can define most of the frequently arising predicates. Unfortunately the above mentioned counterexample shows that there are some fundamental difficulties in doing this. However, in this paper we shall give a theory for proving inclusive predicate existence which has a distinct advantage of being mechanizable. This means a computer can now carry out a large chunk of details. In fact, a system, which we shall call IPL Inclusive Predicate Logic , was implemented on top of LCF which can almost automatically prove the existence of most of the inclusive predicates which arise in practice.

37 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu