Skip to main content
SpringerLink
Log in

Non-deterministic Computations in ELAN

  • Conference paper
  • First Online:
Recent Trends in Algebraic Development Techniques

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

Abstract

The ELAN system is an environment for specifying and prototyping constraint solvers, theorem provers and deduction systems in general. It also provides a framework for experimenting their combination. The ELAN language is based on rewriting logic and evaluation of labelled conditional rewrite rules. ELAN has two originalities with respect to several other algebraic languages, namely to handle non-deterministic computations and to provide a user-defined strategy language for controlling rule application. We focus in this paper on these two related aspects and explain how non-determinism is used in ELAN programs and handled in the ELAN compiler.

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. Aït-Kaci. TheWAM: a (real) tutorial. Technical report 5, Digital Systems Research Center, Paris (France), January 1990.

    Google Scholar 

  2. K. R. Apt and A. Schaerf. Search and imperative programming. In 24th POPL, pages 67–79, 1997.

    Google Scholar 

  3. P. Borovanský, C. Kirchner, and H. Kirchner. Controlling rewriting by rewriting. In J. Meseguer, editor, Proceedings of the first international workshop on rewriting logic, volume 4 of Electronic Notes in Theoretical Computer Science, Asilomar (California), September 1996.

    Google Scholar 

  4. P. Borovanský, C. Kirchner, and H. Kirchner. A functional view of rewriting and strategies for a semantics of ELAN. In M. Sato and Y. Toyama, editors, The Third Fuji International Symposium on Functional and Logic Programming, pages 143–167, Kyoto, April 1998. World Scientific. Also report LORIA 98-R-165.

    Google Scholar 

  5. C. Castro. Building Constraint Satisfaction Problem Solvers Using Rewrite Rules and Strategies. Fundamenta Informaticae, 34:263–293, September 1998.

    Article  MathSciNet  Google Scholar 

  6. M. Clavel, S. Eker, P. Lincoln, and J. Meseguer. Principles of Maude. In J. Meseguer, editor, Proceedings of the first international workshop on rewriting logic, volume 4, Asilomar (California), September 1996. Electronic Notes in Theoretical Computer Science.

    Google Scholar 

  7. H. Cirstea and C. Kirchner. Theorem proving Using Computational Systems: The case of the B Predicate Prover. Available at http://www.loria.fr/ ffcirstea/Papers/TheoremProver.ps, 1997.

  8. Y. Caseau and F. Laburthe. Introduction to the CLAIRE programming language. Technical report 96-15, LIENS Technical, September 1996.

    Google Scholar 

  9. K. Didrich, A. Fett, C. Gerke, W. Grieskamp, and P. Pepper. OPAL: Design and implementation of an algebraic programming language. In J. Gutknecht, editor, Programming Languages and System Architectures PLSA’94, volume 782 of Lecture Notes in Computer Science, pages 228–244. Springer-Verlag, March 1994.

    Chapter  Google Scholar 

  10. K. Futatsugi and A. Nakagawa. An overview of CAFE specification environment — an algebraic approach for creating, verifying, and maintaining formal specifications over networks. In Proceedings of the 1st IEEE Int. Conference on Formal Engineering Methods, 1997.

    Google Scholar 

  11. J. A. Goguen and T. Winkler. Introducing OBJ3. Technical Report SRICSL-88-9, SRI International, 333, Ravenswood Ave.,Menlo Park, CA 94025, August 1988.

    Google Scholar 

  12. F. Henderson, T. Conway, and Z. Somogyi. The execution algorithm of Mercury, an efficient purely declarative logic programming language. Journal of Logic Programming, 29:17–54, October-December 1996.

    Article  Google Scholar 

  13. F. Henderson, Z. Somogyi, and T. Conway. Determinism analysis in the Mercury compiler. In Proceedings of the Nineteenth Australian Computer Science Conference, pages 337–346, Melbourne, Australia, January 1996.

    Google Scholar 

  14. J.-P. Jouannaud and H. Kirchner. Completion of a set of rules modulo set of equations. SIAM Journal of Computing, 15(4):1155–1194, 1986.Preliminary version in Proceedings 11th ACM Symposium on Principles of Programming Languages, Salt Lake City (USA), 1984.

    Article  MathSciNet  Google Scholar 

  15. C. Kirchner, H. Kirchner, and M. Vittek. Designing constraint logic programming languages using computational systems. In P. Van Hentenryck and V. Saraswat, editors, Principles and Practice of Constraint Programming. The Newport Papers., chapter 8, pages 131–158. The MIT press, 1995.

    Google Scholar 

  16. P. Klint. A meta-environment for generating programming environments. ACM Transactions on Software Engineering and Methodology, 2:176–201, 1993.

    Article  Google Scholar 

  17. H. Kirchner and P.-E. Moreau. Prototyping completion with constraints using computational systems. In J. Hsiang, editor, Proceedings 6th Conference on Rewriting Techniques and Applications, Kaiserslautern (Germany), volume 914 of Lecture Notes in Computer Science, pages 438–443. Springer-Verlag, 1995.

    Chapter  Google Scholar 

  18. C. Kirchner and C. Ringeissen. Rule-Based Constraint Programming. Fundamenta Informaticae, 34(3):225–262, September 1998.

    Article  MathSciNet  Google Scholar 

  19. J. Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96(1):73–155, 1992.

    Article  MathSciNet  Google Scholar 

  20. P.-E. Moreau and H. Kirchner. A compiler for rewrite programs in associative-commutative theories. In “Principles of Declarative Programming”, number 1490 in Lecture Notes in Computer Science, pages 230–249. Springer-Verlag, September 1998. Report LORIA 98-R-226.

    Chapter  Google Scholar 

  21. P.-E. Moreau. A choice-point library for backtrack programming. JICSLP’98 Post-Conference Workshop on Implementation Technologies for Programming Languages based on Logic, 1998.

    Google Scholar 

  22. P.-E. Moreau. Compiling nondeterministic computations. Technical Report 98-R-005, CRIN, 1998.

    Google Scholar 

  23. V. Partington. Implementation of an Imperative Programming Language with Backtracking. Technical Report P9714, University of Amsterdam, Programming Research Group, 1997. Available by anonymous ftp from ftp.wins.uva.nl, le pub/programming-research/reports/1997/P9712.ps.Z.

    Google Scholar 

  24. C. Ringeissen. Prototyping Combination of Unification Algorithms with the ELAN Rule-Based Programming Language. In Proceedings 8th Conference on Rewriting Techniques and Applications, Sitges (Spain), volume 1232 of Lecture Notes in Computer Science, pages 323–326. Springer-Verlag, 1997.

    Chapter  Google Scholar 

  25. H. Sawamura and T. Takeshima. Recursive unsolvability of determinacy, solvable cases of determinacy and their applications to Prolog optimization. In Proceedings of the Second International Logic Programming Conference, pages 200–207, Boston, Massachusetts, 1985.

    Google Scholar 

  26. M. Vittek. A compiler for nondeterministic term rewriting systems. In H. Ganzinger, editor, Proceedings of RTA’96, volume 1103 of Lecture Notes in Computer Science, pages 154–168, New Brunswick (New Jersey), July 1996. Springer-Verlag.

    Google Scholar 

  27. D. H. D. Warren. An abstract Prolog instruction set. Technical Report 309, SRI International, Artificial Intelligence Center, 1983.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LORIA-CNRS & INRIA, BP 239 54506, Vandoeuvre-lès-Nancy Cedex, France

    Hélèene Kirchner & Pierre-Etienne Moreau

Authors
  1. Hélèene Kirchner
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pierre-Etienne Moreau
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Informatics, University of Lisbon, Campo Grande 1700, Lisbon, Portugal

    José Luiz Fiadeiro

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kirchner, H., Moreau, PE. (1999). Non-deterministic Computations in ELAN. In: Fiadeiro, J.L. (eds) Recent Trends in Algebraic Development Techniques. Lecture Notes in Computer Science, vol 1589. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48483-3_12

Download citation

  • DOI: https://doi.org/10.1007/3-540-48483-3_12

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66246-4

  • Online ISBN: 978-3-540-48483-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation