Skip to main content
SpringerLink
Log in

On equivalence transformations for term rewriting systems

  • Conference paper
  • First Online:
RIMS Symposia on Software Science and Engineering II

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

Abstract

This paper proposes some simple methods, based on the Church-Rosser property, for testing the equivalence in a restricted domain of two reduction systems. Using the Church-Rosser property, sufficient conditions for the equivalence of abstract reduction systems are proved. These conditions can be effectively applied to test the equivalence in a restricted domain of term rewriting systems. In addition, equivalence transformation rules for term rewriting systems are proposed.

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. Barendregt,H.P.:" The lambda calculus, its syntax and semantics", North-Holland (1981).

    Google Scholar 

  2. Burstall, R.M. and Darlington, J.:" A transformation system for developing recursive programs", J.ACM, Vol.24 (1977), pp.44–67.

    Article  Google Scholar 

  3. Goguen, J.A.:" How to prove algebraic inductive hypotheses without induction, with applications to the correctness of data type implementation", Proc. 5th Conf. Automated deduction, Les Arcs (1980).

    Google Scholar 

  4. Huet, G.:" Confluent reductions: abstract properties and applications to term rewriting systems", J.ACM, Vol.27 (1980), pp.797–821.

    Article  Google Scholar 

  5. Huet,G. and Oppen,D.C.:" Equations and rewrite rules: a survey", Formal languages: perspectives and open problems, Ed.Book,R., Academic Press (1980), pp.349–393.

    Google Scholar 

  6. Huet, G. and Hullot, J.M.:" Proofs by induction in equational theories with constructors", J. Comput. and Syst.Sci., Vol.25 (1982), pp.239–266.

    Article  Google Scholar 

  7. Klop,J.W.:" Combinatory reduction systems", Dissertation, Univ. of Utrecht (1980).

    Google Scholar 

  8. Knuth,D.E. and Bendix,P.G.:" Simple word problems in universal algebras", Computational problems in abstract algebra, Ed.Leech,J., Pergamon Press (1970), pp.263–297.

    Google Scholar 

  9. Musser,D.R.:" On proving inductive properties of abstract data types", Proc. 7th ACM Sympo. Principles of programming languages (1980), pp.154–162.

    Google Scholar 

  10. O'Donnell,M.:" Computing in systems described by equations", Lecture Notes in Comput. Sci. Vol.58, Springer-Verlag (1977).

    Google Scholar 

  11. Rosen, B.K.:" Tree-manipulating systems and Church-Rosser theorems", J.ACM, Vol 20 (1973), pp.160–187.

    Article  Google Scholar 

  12. Scherlis,W.L.:" Expression procedures and program derivation", Ph.D.thesis, Stanford Computer Science Report STAN-CS-80-818 (1980).

    Google Scholar 

  13. Toyama, Y.:" On commutativity of term rewriting systems ", Trans. IECE Japan, J66-D, 12, pp.1370–1375 (1983).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Musashino Electrical Communication Laboratory, N.T.T. Midori-cho, 180, Musashino-shi, Japan

    Yoshihito Toyama

Authors
  1. Yoshihito Toyama
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Eichi Goto Keijiro Araki Taiichi Yuasa

Rights and permissions

Reprints and permissions

Copyright information

© 1986 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Toyama, Y. (1986). On equivalence transformations for term rewriting systems. In: Goto, E., Araki, K., Yuasa, T. (eds) RIMS Symposia on Software Science and Engineering II. Lecture Notes in Computer Science, vol 220. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16470-7_3

Download citation

  • DOI: https://doi.org/10.1007/3-540-16470-7_3

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-16470-8

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation