The Mechanization of Existence Proofs of Recursive Predicates

Abstract

Proving the congruence of two semantics of a language is a well known problem. Milne[3] and Reynolds [5] gave techniques for proving such congruences. Both techniques hinge on proving the existence of certain recursively defined predicates. Milne’s technique is more general than Reynolds’, but the proofs based on that technique are known to be very complicated. In the last eight years:many authors have expressed the need for a more systematic method and a mechanical aid to assist the proofs. In this paper we give a systematic method based on domain theory. The method works by building up appropriate cpos and continuous functions on them. Existence of a predicate then follows by using the Fixed Point Theorem. A mechanized tool has been developed on top of LCF to assist proofs based on this method. The paper refutes the fear expressed by many people that fixed-point theory could not be used to show existence of such predicates.

This research was supported in part by the Defense Advanced Research Projects Agency (DOD), ARPA Order No. 3597, monitored by the Air Force Avionics Laboratory under Contract F33615:81-K-1539, and in part by the U.S. Army Communications R&D Command under Contract DAAI(80-81-K-0074. The views and conclusions contained ill this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of the Defense Advanced Research Projects Agency or the U.S. Government.