Advertisement

Logical closures

  • Dominic Duggan
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 822)

Abstract

Uniform proof procedures for hereditary Harrop formulae have been proposed as a foundation for logic programming. A non-standard approach to defining hereditary Harrop formula is given, allowing quantification over predicate variables but distinguishing the forms of predicate quantification. The benefits of this approach include a treatment of higher order procedures which avoids some scoping problems with languages such as λ-Prolog, and the possibility of extending the language straightforwardly with a module system such as that developed for Standard ML. To enable a style of programming found in existing logic programming languages, a form of implementation inheritance is introduced into the language. Combining this with explicit type quantification provides a form of dynamic dispatching similar to CLOS generic procedures in a statically typed language.

Keywords

Logic Program Logic Programming Operational Semantic Predicate Variable Procedure Definition 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Andrew Appel. Compiling with Continuations. Cambridge University Press, 1992.Google Scholar
  2. 2.
    Thierry Coquand. An analysis of Girard's paradox. In Proceedings of IEEE Symposium on Logic in Computer Science, 1986.Google Scholar
  3. 3.
    Dominic Duggan. Higher-order substitutions. Technical Report CS-9344, University of Waterloo, 1993. 34 pages. Submitted for publication. An earlier version of this paper was presented at the λ-Prolog Workshop, Philadelphia PA, July 1992.Google Scholar
  4. 4.
    Dominic Duggan. Logical closures. Technical Report UWCS-94-20, Department of Computer Science, University of Waterloo, 1994.Google Scholar
  5. 5.
    Dominic Duggan. Possible worlds semantics for higher-order, explicitly polymorphic logic programming. In preparation, 1994.Google Scholar
  6. 6.
    Dominic Duggan. Unification with extended patterns. Technical Report CS-93-37, University of Waterloo, 1994. 57 pages. Revised March 1994. Submitted for publication.Google Scholar
  7. 7.
    Amy Felty. Encoding the calculus of constructions in a higher-order logic. In Proceedings of IEEE Symposium on Logic in Computer Science, 1993.Google Scholar
  8. 8.
    Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types. Cambridge University Press, 1989.Google Scholar
  9. 9.
    Robert Harper, John Mitchell, and Eugenio Moggi. Higher-order modules and the phase distinction. In Proceedings of ACM Symposium on Principles of Programming Languages, pages 341–354. Association for Computing Machinery, 1990.Google Scholar
  10. 10.
    Robert Harper and John C. Mitchell. On the type structure of Standard ML. ACM Transactions on Programming Languages and Systems, 15(2):211–252, 1993.Google Scholar
  11. 11.
    S. C. Keene. Object Oriented Programming in Common Lisp: A Programming Guide in CLOS. Addison-Wesley, 1989.Google Scholar
  12. 12.
    Zhaohui Luo. ECC, an extended calculus of constructions. In Proceedings of IEEE Symposium on Logic in Computer Science, pages 385–395. IEEE, 1989.Google Scholar
  13. 13.
    P. Martin-Löf. An intuitionistic theory of types: Predicative part. In H. E. Rose and J. C. Shepherdson, editors, Logic Colloquium '73, pages 73–118. North-Holland, 1973.Google Scholar
  14. 14.
    Dale Miller. Abstractions in logic programming. In Peirgiorgio Odifreddi, editor, Logic and Computer Science, pages 329–359. Academic Press, 1990.Google Scholar
  15. 15.
    Dale Miller. A logic programming language with lambda-abstraction, function variables and simple unification. Journal of Logic and Computation, 1(4):497–536, 1991.Google Scholar
  16. 16.
    Dale Miller. Unification of simply typed λ-terms as logic programming. In Proceedings of the International Conference on Logic Programming, pages 255–269. MIT Press, 1991.Google Scholar
  17. 17.
    Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125–157, 1991.Google Scholar
  18. 18.
    Gopalan Nadathur and Dale Miller. An overview of λ-Prolog. In Proceedings of the International Conference on Logic Programming, pages 810–827. MIT Press, 1988.Google Scholar
  19. 19.
    Gopalan Nadathur and Dale Miller. Higher-order Horn clauses. Journal of the ACM, 37(4):777–814, October 1990.Google Scholar
  20. 20.
    Lawrence C. Paulson and Andrew W. Smith. Logic programming, functional programming and inductive definitions. In Peter Schroeder-Heister, editor, Extensions of Logic Programming. Springer-Verlag, 1990.Google Scholar
  21. 21.
    Frank Pfenning. Logic programming in the LF logical framework. In Gerard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 149–181. Cambridge University Press, 1990.Google Scholar
  22. 22.
    Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 199–208. Association for Computing Machinery, 1988.Google Scholar
  23. 23.
    Vijay Saraswat. The category of constraint systems is Cartesian closed. In Proceedings of IEEE Symposium on Logic in Computer Science, pages 341–345, 1992.Google Scholar
  24. 24.
    Peter Schroeder-Heister. Hypothetical reasoning and definitional reflection in logic programming. In Peter Schroeder-Heister, editor, Extensions of Logic Programming. Springer-Verlag Lecture Notes in Computer Science, 1990.Google Scholar
  25. 25.
    William Wadge. Higher order Horn logic programming. In Proceedings of the IEEE International Logic Programming Symposium, 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • Dominic Duggan
    • 1
  1. 1.Department of Computer ScienceUniversity of WaterlooWaterlooCanada

Personalised recommendations