A local termination property for term rewriting systems

  • Dana May Latch
  • Ron Sigal
Regular Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 355)


We describe a desirable property, local termination, of rewrite systems which provide an operational semantics for formal functional programming (FFP) languages, and we give a multiset ordering which can be used to show that the property holds.


Term Variable Operational Semantic Local Termination Reduction Rule Functional Language 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

6 References

  1. Ba78.
    BACKUS, J., ‘Can programming be liberated from the von Neumann style? A functional style and its algebra of programs,’ Communications of the ACM, 21(1978), 613–641.Google Scholar
  2. BaW286.
    BACKUS, J., WILLIAMS, J. H., and WIMMERS, E. L. ‘FL Language Manual,’ Research Report RJ 5339, IBM Research Laboratory, San Jose, CA, November, 1986.Google Scholar
  3. BiWa88.
    BIRD, R. and WALDER, P., Introduction to Functional Programming, Prentice Hall, New York, 1988.Google Scholar
  4. BoMo79.
    BOYER, R. S., and MOORE, J. S., A Computational Logic; Academic Press, New York, 1979.Google Scholar
  5. CoBo72.
    CONSTABLE, R. E., and BORODIN, A., ‘Subrecursive programming languages. Part 1,’ J. Assoc. Comp. Mach., 19(1972), 526–568.Google Scholar
  6. De82.
    DERSHOWITZ, N., ‘Orderings for term rewriting systems,” J. of Theoretical Comp. Sci., 17(1982), 279–310.Google Scholar
  7. De85.
    DERSHOWITZ, N., ‘Termination,’ Proceedings of Rewriting Techniques and Applications, Dijon, France, May 1985, LNCS 202, Springer-Verlag, New York, 1985, 180–224.Google Scholar
  8. DeMa79.
    DERSHOWITZ, N., and MANNA, Z., ‘Proving termination with multiset orderings,’ Communications of the ACM, 22(1979), 465–467.Google Scholar
  9. Ei87.
    EISENBACH, S., Functional Programming: Languages, Tools and Architectures, John Wiley & Sons, New York, 1987.Google Scholar
  10. Fr79.
    FRANK, G., Virtual Memory Systems for Closed Applicative Language Interpreters, Ph.D. Dissertation, University of North Carolina at Chapel Hill, 1979.Google Scholar
  11. HaW385.
    HALPERN, J. Y., WILLIAMS, J. H., WIMMERS, E.L. and WINKLER, T. C., ‘Denotational semantics and rewrite rules for FP,’ Proceedings of the Twelfth ACM Symposium of Principles of Programming Languages, January 1985, 108–120.Google Scholar
  12. HoUl79.
    HOPCROFT, J. E., and ULLMAN, J. D., Introduction to Automata Theory, Languages, and Computation, Addison-Wesley, Reading, MA, 1979.Google Scholar
  13. Hu80.
    HUET, G., ‘Confluent reductions: abstract properties and applications to term rewriting systems,’ J. of Assoc. Comp. Mach., 27(1980), 797–821.Google Scholar
  14. KnBe70.
    KNUTH, D. and BENDIX, P., 'simple word problems in universal algebras,’ Computational Problems in Abstract Algebra, Leech, J., ed., Pergamon Press, 1970, 263–297.Google Scholar
  15. La75.
    LANKFORD, D. S., ‘Canonical algebraic simplification in computational logic,’ MEM ATP-25, Automated Theorem Proving Project, University of Texas, Austin, TX, May 1985.Google Scholar
  16. LatSi88.
    LATCH, D. M. and SIGAL, R., ‘Generating evaluation theorems for functional programming languages,’ Proceedings of the Third International Symposium on Methodologies for Intelligent Systems, Torino, Italy, October, 1988, 47–58.Google Scholar
  17. Tu82.
    TURNER, D., ‘On the Kent recursive calculator,’ Functional Programming and Its Applications, Darlington, J., ed., Cambridge University Press, New York, 1982.Google Scholar
  18. Wi81.
    WILLIAMS, J. H., ‘Formal representations for recursively defined functional programs,’ Formalization of Programming Concepts, LNCS 107, Springer-Verlag, New York, 1981, 460–470.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1989

Authors and Affiliations

  • Dana May Latch
    • 1
  • Ron Sigal
    • 2
  1. 1.Department of MathematicsNorth Carolina State UniversityRaleigh
  2. 2.Dipartimento di MatematicaUniversità di CataniaCataniaItaly

Personalised recommendations