Skip to main content
SpringerLink
Log in

An effective method for handling initial algebras

  • Submitted Papers
  • Conference paper
  • First Online:
Book cover Algebraic and Logic Programming (ALP 1988)

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

Included in the following conference series:

Abstract

Given an arbitrary Term Rewriting System R, we compute a “conditional grammar” of the language of ground terms which are irreducible for R. Such a presentation provides a powerful tool for reasoning in non-free algebras. We sketch here two applications:

  1. 1.

    The decision of inductive reducibility (which is a key concept in automating proofs by induction)

  2. 2.

    The automatic transformation of non-free, many sorted algebraic specifications into free order-sorted specifications.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. H. Comon and P. Lescanne. Equational Problems and Disunification. Research Report Lifia 82 Imag 727, Univ. Grenoble, May 1988.

    Google Scholar 

  2. A. Colmerauer. Equations and inequations on finite and infinite trees. In FGCS'84 Proceedings, pages 85–99, November 1984.

    Google Scholar 

  3. H. Comon. Sufficient completeness, term rewriting systems and anti-unification. In Proc. 8th Conf. on Automated Deduction, Oxford, LNCS 230, pages 128–140, Springer-Verlag, 1986.

    Google Scholar 

  4. H. Comon. Unification et Disunification: Théorie et Applications. Thèse de Doctorat, I.N.P. de Grenoble, France, 1988.

    Google Scholar 

  5. H. Comon and J.-L. Remy. How to Characterize the Language of Ground Normal Forms. Research Report 676, INRIA, June 1987.

    Google Scholar 

  6. J. H. Gallier and R. V. Book. Reductions in tree replacement systems. Theoretical Computer Science, 37:123–150, 1985.

    Article  MathSciNet  MATH  Google Scholar 

  7. J. Goguen and J. Meseguer. Models and equality for logical programming. In Proc. CFLP, Pisa, LNCS 250, Springer-Verlag, March 1987.

    Google Scholar 

  8. J. A. Goguen, J. W. Thatcher, and E. G. Wagner. An initial algebra approach to the specification, correctness and implementation of abstract data types. In Current Trends in Programming Methodology, vol. 4, pages 80–149, Prentice Hall Int., 1978.

    Google Scholar 

  9. G. Huet and J.-M. Hullot. Proofs by induction in equational theories with constructors. Journal of Computer and System Sciences, 25(2), 1982.

    Google Scholar 

  10. J.-P. Jouannaud and E. Koualis. Automatic proofs by induction in equational theories without constructors. In Proc. 1st IEEE Symp. Logic in Computer Science, Cambridge, Mass., June 1986.

    Google Scholar 

  11. C. Kirchner and P. Lescanne. Solving disequations. In Proc. 2nd IEEE Symp. Logic in Computer Science, Ithaca, NY, pages 347–352, 1987.

    Google Scholar 

  12. D. Kapur, P. Narendran, and H. Zhang. On Sufficient Completeness and Related Properties of Term Rewriting Systems. Research Report, General Electric Company, October 1985. Preprint.

    Google Scholar 

  13. D. Kapur, P. Narendran, and H. Zhang. Complexity of sufficient completeness. 1986. To appear in TCS.

    Google Scholar 

  14. A. Lazrek, P. Lescanne, and J.-J. Thiel. Proving Inductive Equalities. Algorithms and Implementation. Research Report, CRIN, Nancy, France, 1986. To appear in Information and Control.

    Google Scholar 

  15. M. J. Maher. Complete axiomatization of the algebra of finite, rational and infinite trees. January 1988. Draft Paper.

    Google Scholar 

  16. J. Meseguer and J. Goguen. Initiality, induction and computability. In M. Nivat and J. Reynolds, editors, Algebraic Methods in Semantics, chapter 14, Cambridge Univ. Press, 1985.

    Google Scholar 

  17. T. Nipkow and G. Weikum. A decidability result about sufficient completeness of axiomatically specified abstract data types. In Proc. 6th GI. Conf., Springer-Verlag, 1982.

    Google Scholar 

  18. D. Plaisted. Semantic confluence tests and completion methods. Information and Control, 65:182–215, 1985.

    Article  MathSciNet  MATH  Google Scholar 

  19. Ph. Schnoebelen. Refined Compilation of Pattern-Matching for Functional Languages. Research Report Lifia 71 Imag 715, Univ. Grenoble, April 1988. Submitted for publication.

    Google Scholar 

  20. J. J. Thiel. Stop loosing sleep over incomplete specifications. In Proc. ACM Symp. Principles of Programming Languages, 1984.

    Google Scholar 

  21. S. Thompson. Laws in Miranda. In Proc. ACM Conf. Lisp and Functional Programming, Cambridge, Mass., August 1986.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratoire d'Informatique Fondamentale et d'Intelligence Artificielle (LIFIA), 46 Avenue Félix Viallet, 38031, Grenoble, France

    Hubert Comon

Authors
  1. Hubert Comon
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

J. Grabowski P. Lescanne W. Wechler

Rights and permissions

Reprints and permissions

Copyright information

© 1988 Akademie-Verlag Berlin

About this paper

Cite this paper

Comon, H. (1988). An effective method for handling initial algebras. In: Grabowski, J., Lescanne, P., Wechler, W. (eds) Algebraic and Logic Programming. ALP 1988. Lecture Notes in Computer Science, vol 343. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-50667-5_62

Download citation

  • DOI: https://doi.org/10.1007/3-540-50667-5_62

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-46063-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation