Parametric order-sorted types in logic programming

  • Michael Hanus
CCPSD Colloquium On Combining Paradigms For Software Development
Part of the Lecture Notes in Computer Science book series (LNCS, volume 494)


This paper proposes a type system for logic programming where types are structured in two ways. Firstly, functions and predicates may be declared with types containing type parameters which are universally quantified over all types. In this case each instance of the type declaration can be used in the logic program. Secondly, types are related by subset inclusions. In this case a function or predicate can be applied to all subtypes of its declared type. While previous proposals for such type systems have strong restrictions on the subtype relation, we assume that the subtype order is specified by Horn clauses for the subtype relation ≤. This allows the declaration of a lot of interesting type structures, e.g., type constructors which are monotonic as well as anti-monotonic in their arguments. For instance, parametric order-sorted type structures for logic programs with higher-order predicates can be specified in our framework.

This paper presents the declarative and operational semantics of the typed logic language. The operational semantics requires a unification procedure on well-typed terms. This unification procedure is described by a set of transformation rules which generate a set of type constraints from a given unification problem. The solvability of these type constraints is decidable for particular type structures.


Logic Program Logic Programming Operational Semantic Horn Clause Unification Procedure 
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.


  1. [AvE82]
    K.R. Apt and M.H. van Emden. Contributions to the Theory of Logic Programming. Journal of the ACM, Vol. 29, No. 3, pp. 841–862, 1982.Google Scholar
  2. [BG86]
    P.G. Bosco and E. Giovannetti. IDEAL: An Ideal Deductive Applicative Language. In Proc. IEEE Internat. Symposium on Logic Programming, pp. 89–94, Salt Lake City, 1986.Google Scholar
  3. [BG89]
    R. Barbuti and R. Giacobazzi. A Bottom-Up Polymorphic Type Inference in Logic Programming. Technical Report 27/89, Dip. di Informatica, Università di Pisa, 1989.Google Scholar
  4. [CvER89]
    M.H.M. Cheng, M.H. van Emden, and B.E. Richards. On Warren's Method for Functional Programming in Logic. Report LP-12 DCS-122-IR, Univ. of Victoria, 1989.Google Scholar
  5. [CW85]
    L. Cardelli and P. Wegner. On Understanding Types, Data Abstraction, and Polymorphism. acm computing surveys, Vol. 17, No. 4, pp. 471–523, 1985.Google Scholar
  6. [EM85]
    H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1: Equations and Initial Semantics, volume 6 of EATCS Monographs on Theoretical Computer Science. Springer, 1985.Google Scholar
  7. [FM88]
    Y.-C. Fuh and P. Mishra. Type Inference with Subtypes. In Proc. ESOP 88, Nancy, pp. 94–114. Springer LNCS 300, 1988.Google Scholar
  8. [GM84]
    J.A. Goguen and J. Meseguer. Completeness of Many-Sorted Equational Logic. Report No. CSLI-84-15, Stanford University, 1984.Google Scholar
  9. [Han89a]
    M. Hanus. Horn Clause Programs with Polymorphic Types: Semantics and Resolution. In Proc. of the TAPSOFT '89, pp. 225–240. Springer LNCS 352, 1989. Extended version to appear in Theoretical Computer Science.Google Scholar
  10. [Han89b]
    M. Hanus. Polymorphic Higher-Order Programming in Prolog. In Proc. Sixth International Conference on Logic Programming (Lisboa), pp. 382–397. MIT Press, 1989.Google Scholar
  11. [Han90]
    M. Hanus. Logic Programs with Equational Type Specifications. In Proc. of the 2nd International Conference on Algebraic and Logic Programming, pp. 70–85. Springer LNCS 463, 1990.Google Scholar
  12. [Han91]
    M. Hanus. Parametric Order-Sorted Types in Logic Programming. Technical Report, FB Informatik, Univ. Dortmund, 1991.Google Scholar
  13. [HT90]
    P.M. Hill and R.W. Topor. A Semantics for Typed Logic Programs. Report TR-90-11, Computer Science Department, University of Bristol, 1990.Google Scholar
  14. [HV87]
    M. Huber and I. Varsek. Extended Prolog with Order-Sorted Resolution. In Proc. 4th IEEE Internat. Symposium on Logic Programming, pp. 34–43, San Francisco, 1987.Google Scholar
  15. [JL87]
    J. Jaffar and J.-L. Lassez. Constraint Logic Programming. In Proc. of the 14th ACM Symposium on Principles of Programming Languages, pp. 111–119, Munich, 1987.Google Scholar
  16. [Llo87]
    J.W. Lloyd. Foundations of Logic Programming. Springer, second, extended edition, 1987.Google Scholar
  17. [Mis84]
    P. Mishra. Towards a theory of types in Prolog. In Proc. IEEE Internat. Symposium on Logic Programming, pp. 289–298, Atlantic City, 1984.Google Scholar
  18. [MN86]
    D.A. Miller and G. Nadathur. Higher-Order Logic Programming. In Proc. Third International Conference on Logic Programming (London), pp. 448–462. Springer LNCS 225, 1986.Google Scholar
  19. [MO84]
    A. Mycroft and R.A. O'Keefe. A Polymorphic Type System for Prolog. Artificial Intelligence, Vol. 23, pp. 295–307, 1984.Google Scholar
  20. [Nai87]
    L. Naish. Specification = Program + Types. In Proc. Foundations of Software Technology and Theoretical Computer Science, pp. 326–339. Springer LNCS 287, 1987.Google Scholar
  21. [Poi86]
    A. Poigné. On Specifications, Theories, and Models with Higher Types. Information and Control, Vol. 68, No. 1–3, 1986.Google Scholar
  22. [Rey74]
    J.C. Reynolds. Towards a Theory of Type Structure. In Proc. Colloque sur la Programmation, pp. 408–425. Springer LNCS 19, 1974.Google Scholar
  23. [Rob65]
    J.A. Robinson. A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM, Vol. 12, No. 1, pp. 23–41, 1965.Google Scholar
  24. [Smo86]
    G. Smolka. Order-Sorted Horn Logic: Semantics and Deduction. SEKI Report SR-86-17, FB Informatik, Univ. Kaiserslautern, 1986.Google Scholar
  25. [Smo89]
    G. Smolka. Logic Programming over Polymorphically Order-Sorted Types. Dissertation, FB Informatik, Univ. Kaiserslautern, 1989.Google Scholar
  26. [SNGM89]
    G. Smolka, W. Nutt, J.A. Goguen, and J. Meseguer. Order-Sorted Equational Computation. In Hassan Aït-Kaci and Maurice Nivat, editors, Resolution of Equations in Algebraic Structures, Volume 2, Rewriting Techniques, chapter 10, pp. 297–367. Academic Press, New York, 1989.Google Scholar
  27. [SS85]
    M. Schmidt-Schauss. A Many Sorted Calculus with Polymorphic Functions Based on Resolution and Paramodulation. In Proc. 9th IJCAI. W. Kaufmann, 1985.Google Scholar
  28. [SS86]
    L. Sterling and E. Shapiro. The Art of Prolog. MIT Press, 1986.Google Scholar
  29. [War82]
    D.H.D. Warren. Higher-order extensions to PROLOG: are they needed? In Machine Intelligence 10, pp. 441–454, 1982.Google Scholar
  30. [XW88]
    J. Xu and D.S. Warren. A Type Inference System For Prolog. In Proc. 5th Conference on Logic Programming & 5th Symposium on Logic Programming (Seattle), pp. 604–619, 1988.Google Scholar
  31. [Zob87]
    J. Zobel. Derivation of Polymorphic Types for Prolog Programs. In Proc. Fourth International Conference on Logic Programming (Melbourne), pp. 817–838. MIT Press, 1987.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • Michael Hanus
    • 1
  1. 1.Fachbereich InformatikUniversität DortmundDortmund 50Germany

Personalised recommendations