The Mechanization of Existence Proofs of Recursive Predicates

  • Ketan Mulmuley
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 170)


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.


Free Variable Predicate Symbol Denotational Semantic Constant Symbol Defense Advance Research Project Agency 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. (1).
    Cohn, Avra: The Equivalence of Two Semantic Definitions: A Case Study In LCF; Internal Report, University Of Edinburgh Report, (1981).Google Scholar
  2. (2).
    Gordon, Michael: Towards a Semantic Theory of Dynamic Binding; Memo AIM-265, Computer Science Department, Stanford University.Google Scholar
  3. (3).
    Milne, Robert and Strachey, Christopher: A Theory of Programming Language Semantics; Chapman and Hall, London, and John Wiley, New York (1976).zbMATHGoogle Scholar
  4. (4).
    Mosses, Peter: Mathematical Semantics and Compiler Generation; Ph.D thesis, Oxford University Computing Laboratory, Programming Research Group (1975).Google Scholar
  5. (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. (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. (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
  8. (8).
    Stoy, Joseph: Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory; (MIT Press, Cambridge, MA, 1977).zbMATHGoogle Scholar
  9. (9).
    Stoy, Joseph: The Congruence of Two Programming Language Definitions; Theoretical Computer Science 13 (1981) 151–174. North-Holland Publishing company.MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • Ketan Mulmuley
    • 1
  1. 1.Computer Science DepartmentCarnegie-Mellon UniversityPittsburghUSA

Personalised recommendations