Skip to main content
SpringerLink
Log in

A hidden Herbrand Theorem

  • Conference paper
  • First Online:
Book cover Principles of Declarative Programming (ALP 1998, PLILP 1998)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1490))

  • 104 Accesses

Abstract

The benefits of the object, logic (or relational), functional, and constraint paradigms can be combined, by providing existential queries over objects and their attributes, subject to constraints. This paper provides a precise mathematical foundation for this novel programming paradigm, and shows that it is computationally feasible by reducing it to familiar problems over term algebras (i.e., Herbrand universes). We use the formalism of hidden logic, and our main result is a version of Herbrand's Theorem for that setting. By extending a result of Diaconescu, we lift our results from equational logic to Horn clause logic with equality.

The research reported in this paper has been supported in part by the Science and Engineering Research Council, the EC under ESPRIT-2 BRA Working Groups 6071, IS-CORE and 6112, COMPASS, Fujitsu Laboratories Limited, and a contract under the management of the Information Technology Promotion Agency (IPA), Japan, as part of the Industrial Science and Technology Frontier Program ‘New Models for Software Architectures,’ sponsored by NEDO (New Energy and Industrial Technology Development Organization).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Rod Burstall and RĂzvan Diaconescu. Hiding and behaviour: an institutional approach. In A. W. Roscoe, editor, A Classical Mind: essays dedicated to C.A.R. Hoare. Prentice-Hall International, 1994.

    Google Scholar 

  2. Corina CÎrstea. Coalgebra semantics for hidden algebra: parameterized objects and inheritance. In Proc. 12th Workshop on Algebraic Development Techniques. Springer-Verlag Lecture Notes in Computer Science, to appear, 1998.

    Google Scholar 

  3. Corina CÎrstea, Grant Malcolm, and James Worrell. Hidden order sorted algebra: subtypes for objects. Draft, Oxford University Computing Laboratory, 1998.

    Google Scholar 

  4. Nachum Dershowitz and Jean-Pierre Jouannaud. Rewriting systems. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B: Formal Methods and Semantics, pages 243–320. North-Holland, 1990.

    Google Scholar 

  5. RĂzvan Diaconescu. The logic of Horn clauses is equational. Technical Report PRG-TR-3-93, Programming Research Group, University of Oxford, 1993. Written in 1990.

    Google Scholar 

  6. RĂzvan Diaconescu. Category-based Semantics for Equational and Constraint Logic Programming. PhD thesis, Oxford University, 1994.

    Google Scholar 

  7. RĂzvan Diaconescu. A category-based equational logic semantics to constraint programming. Lecture Notes in Computer Science, 1130:200–222, 1996.

    Google Scholar 

  8. RĂzvan Diaconescu and Kokichi Futatsugi. Logical semantics for Cafeobj. Technical Report IS-RR-96-0024S, Japan Advanced Institute of Science and Technology, 1996.

    Google Scholar 

  9. Hartmut Ehrig and Bernd Mahr. Fundamentals of Algebraic Specification 1: Equations and Initial Semantics. Springer, 1985.

    Google Scholar 

  10. Joseph A. Goguen. Types as theories. In George Michael Reed, Andrew William Roscoe, and Ralph F. Wachter, editors, Topology and Category Theory in Computer Science, pages 357–390. Oxford University Press, 1991.

    Google Scholar 

  11. Joseph A. Goguen and Rod Burstall. Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery, 39(1):95–146, 1992.

    MATH  MathSciNet  Google Scholar 

  12. Joseph A. Goguen and RĂzvan Diaconescu. An Oxford survey of order sorted algebra. Mathematical Structures in Computer Science, 4:363–392, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  13. Joseph A. Goguen and RĂzvan Diaconescu. Towards an algebraic semantics for the object paradigm. In Hartmut Ehrig and Fernando Orejas, editors, Recent Trends in Data Type Specification. Springer-Verlag Lecture Notes in Computer Science 785, 1994.

    Google Scholar 

  14. Joseph A. Goguen and Grant Malcolm. Proof of correctness of object representations. In A. W. Roscoe, editor, A Classical Mind: essays dedicated to C.A.R. Hoare, chapter 8, pages 119–142. Prentice-Hall International, 1994.

    Google Scholar 

  15. Joseph A. Goguen and Grant Malcolm. Situated adaptive software: beyond the object paradigm. In Proc. New Models for Software Architecture (Tokyo). Information-technology Promotion Agency, 1995.

    Google Scholar 

  16. Joseph A. Goguen and Grant Malcolm. Algebraic Semantics of Imperative Programs. MIT Press, 1996.

    Google Scholar 

  17. Joseph A. Goguen and Grant Malcolm. A hidden agenda. Technical Report CS97-538, Department of Computer Science and Engineering, University of California at San Diego, 1997. An extended abstract appears in Proc. Intelligent Systems: a Semiotic Perspective, 1996.

    Google Scholar 

  18. Joseph A. Goguen and José Meseguer. Universal realization, persistent interconnection and implementation of abstract modules. In M. Nielsen and E.M. Schmidt, editors, Proceedings, 9th International Conference on Automata, Languages and Programming, pages 265–281. Springer-Verlag Lecture Notes in Mathematics 140, 1982.

    Google Scholar 

  19. Joseph A. Goguen and José Meseguer. Eqlog: Equality, types, and generic modules for logic programming. In Douglas DeGroot and Gary Lindstrom, editors, Logic Programming: Functions, Relations and Equations, pages 295–363. Prentice-Hall, 1986. An earlier version appears in Journal of Logic Programming, Volume 1, Number 2, pages 179–210, September 1984.

    Google Scholar 

  20. Joseph A. Goguen and José Meseguer. Models and equality for logical programming. In Hartmut Ehrig, Giorgio Levi, Robert Kowalski, and Ugo Montanari, editors, Proceedings, 1987 TAPSOFT, pages 1–22. Springer-Verlag Lecture Notes in Mathematics 250, 1987.

    Google Scholar 

  21. Joseph A. Goguen and José Meseguer. Unifying functional, object-oriented and relational programming, with logical semantics. In Bruce Shriver and Peter Wegner, editors, Research Directions in Object-Oriented Programming, pages 417–477. MIT, 1987.

    Google Scholar 

  22. Joseph A. Goguen and José Meseguer. Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoretical Computer Science, 105(2):217–273, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  23. Joseph A. Goguen, James Thatcher, and Eric Wagner. An initial algebra approach to the specification, correctness and implementation of abstract data types. Technical Report RC 6487, IBM T.J. Watson Research Center, October 1976. In Current Trends in Programming Methodology, IV, Raymond Yeh, editor, Prentice-Hall, 1978, pages 80–149.

    Google Scholar 

  24. Joseph A. Goguen, Timothy Winkler, José Meseguer, Kokichi Futatsugi, and Jean-Pierre Jouannaud. Introducing obj. In Joseph A. Goguen and Grant Malcolm, editors, Software Engineering with OBJ: Algebraic Specification in Practice. to appear. Also available as a technical report from SRI International.

    Google Scholar 

  25. Jacques Herbrand. Recherches sur la théorie de la démonstration. Travaux de la Société des Sciences et des Lettres de Varsovie, Classe III, 33(128), 1930.

    Google Scholar 

  26. B. Jacobs. Inheritance and cofree constructions. In P. Cointe, editor, European Conference on Object-Oriented Programming, number 1098 in LNCS, pages 210–231. Springer, Berlin, 1996.

    Google Scholar 

  27. Grant Malcolm. Behavioural equivalence, bisimilarity, and minimal realisation. In Magne Haveraaen, Olaf Owe, and Ole-Johan Dahl, editors, Recent Trends in Data Type Specifications. 11th Workshop on Specification of Abstract Data Types, WADT11. Oslo Norway, September 1995, pages 359–378. Springer-Verlag Lecture Notes in Computer Science 1130, 1996.

    Google Scholar 

  28. Grant Malcolm and Joseph A. Goguen. Proving correctness of refinement and implementation. Technical Monograph PRG-114, Programming Research Group, Oxford University, 1994.

    Google Scholar 

  29. José Meseguer and Joseph A. Goguen. Initiality, induction and computability. In Maurice Nivat and John Reynolds, editors, Algebraic Methods in Semantics, pages 459–-541. Cambridge, 1985.

    Google Scholar 

  30. Bertrand Meyer. Object-Oriented Software Construction.Prentice Hall, 2nd edition, 1997.

    Google Scholar 

  31. Horst Reichel. Behavioural equivalence — a unifying concept for initial and final specifications. In Proceedings, Third Hungarian Computer Science Conference. Akademiai Kiado, 1981. Budapest.

    Google Scholar 

  32. Horst Reichel. Behavioural validity of conditional equations in abstract data types. In Contributions to General Algebra 3. Teubner, 1985. Proceedings of the Vienna Conference, June 21–24, 1984.

    Google Scholar 

  33. Horst Reichel. An approach to object semantics based on terminal co-algebras. Mathematical Structures in Computer Science, 5:129–152, 1995.

    MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Computer Science & Engineering, University of California at San Diego, USA

    Joseph Goguen

  2. Connect Centre, Dept. of Computer Science, University of Liverpool, England

    Grant Malcolm

  3. Oxford

    Tom Kemp

Authors
  1. Joseph Goguen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Grant Malcolm
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Tom Kemp
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Catuscia Palamidessi Hugh Glaser Karl Meinke

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Goguen, J., Malcolm, G., Kemp, T. (1998). A hidden Herbrand Theorem. In: Palamidessi, C., Glaser, H., Meinke, K. (eds) Principles of Declarative Programming. ALP PLILP 1998 1998. Lecture Notes in Computer Science, vol 1490. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0056632

Download citation

  • DOI: https://doi.org/10.1007/BFb0056632

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65012-6

  • Online ISBN: 978-3-540-49766-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation