The Mechanization of Existence Proofs of Recursive Predicates
Proving the congruence of two semantics of a language is a well known problem. Milne and Reynolds  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.
KeywordsFree Variable Predicate Symbol Denotational Semantic Constant Symbol Defense Advance Research Project Agency
Unable to display preview. Download preview PDF.
- (1).Cohn, Avra: The Equivalence of Two Semantic Definitions: A Case Study In LCF; Internal Report, University Of Edinburgh Report, (1981).Google Scholar
- (2).Gordon, Michael: Towards a Semantic Theory of Dynamic Binding; Memo AIM-265, Computer Science Department, Stanford University.Google Scholar
- (4).Mosses, Peter: Mathematical Semantics and Compiler Generation; Ph.D thesis, Oxford University Computing Laboratory, Programming Research Group (1975).Google Scholar
- (5).Reynolds, J.C.: On the Relation Between Direct and Continuation Semantics; pp. 141–156 of proceedings of the Second Colloquium on Automata, Languages and Programming, Saarbrücken, Springer-verlag, Berlin (1974).Google Scholar
- (6).Scott, Dana: Lectures On a Mathematical Theory of Computation; Technical Monograph PRG-19 (May 1981). Oxford University Computing Laboratory, Programming Research Group.Google Scholar
- (7).Sethi, Ravi and Tang Adrian: Constructing Call-by-value Continuation Semantics; Journal of the Association for Computing Machinery,vol 27. No.3. July 1980.pp.580–597.Google Scholar