{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:42:04Z","timestamp":1750308124059,"version":"3.41.0"},"reference-count":12,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[1982,11,1]],"date-time":"1982-11-01T00:00:00Z","timestamp":404956800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGSAM Bull."],"published-print":{"date-parts":[[1982,11]]},"abstract":"<jats:p>A general algorithm for reduction with algebraic term rewriting systems is presented and several aspects of rewriting are discussed.It turns out that the well known strategies of innermost and outermost rewriting, which are special cases of the general algorithm, exhibit good performance under different aspects. The general rewriting algorithm suggests improvements for naive reduction algorithms with specific strategies, which in some cases give them better asymptotic behaviour. Empirical results with an algebraic axiomatization of natural numbers show considerably faster runtimes for the improved algorithms.The algorithms presented here do not impose any restrictions on the rewriting systems. They are currently used both within an implementation of the Knuth-Bendix completion algorithm and in a separate term reduction system, whenever sufficiently large terms are involved.<\/jats:p>","DOI":"10.1145\/1089310.1089315","type":"journal-article","created":{"date-parts":[[2007,1,17]],"date-time":"2007-01-17T18:32:02Z","timestamp":1169058722000},"page":"13-23","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Some reduction strategies for algebraic term rewriting"],"prefix":"10.1145","volume":"16","author":[{"given":"Wolfgang","family":"K\u00fcchlin","sequence":"first","affiliation":[{"name":"Universit\u00e4t Karlsruhe, Karlsruhe"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[1982,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567768"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/322290.322295"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/357153.357158"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/322217.322230"},{"key":"e_1_2_1_5_1","first-page":"19","volume-title":"Proc. 1982 European Conf. on Art. Intell.","author":"Hue","year":"1982","unstructured":"{ Hue 82} Huet G.: In Defense of Programming Language Design . Proc. 1982 European Conf. on Art. Intell. , Orsay, France , July 1982 , pp. 19 -- 27 . {Hue82} Huet G.: In Defense of Programming Language Design. Proc. 1982 European Conf. on Art. Intell., Orsay, France, July 1982, pp. 19--27."},{"key":"e_1_2_1_7_1","volume-title":"IRIA, Aout","author":"Hu G.","year":"1979","unstructured":"{ Hu &Le79} Huet G. and Levy J. J .: Call by Need Computations in Non-Ambiguous Linear Term Rewriting Systems. Rapport Laboria 359 , IRIA, Aout 1979 . {Hu&Le79} Huet G. and Levy J. J.: Call by Need Computations in Non-Ambiguous Linear Term Rewriting Systems. Rapport Laboria 359, IRIA, Aout 1979."},{"key":"e_1_2_1_9_1","volume-title":"Leech J.","author":"Kn D. E.","year":"1970","unstructured":"{ Kn &Be70} Knuth D. E. and Bendix P. B .: Simple Word Problems in Universal Algebras. In \"Computational Problems in Abstract Algebra \", Ed. Leech J. , Pergamon , Oxford 1970 . {Kn&Be70} Knuth D. E. and Bendix P. B.: Simple Word Problems in Universal Algebras. In \"Computational Problems in Abstract Algebra\", Ed. Leech J., Pergamon, Oxford 1970."},{"key":"e_1_2_1_10_1","volume-title":"An Implementation and Investigation of the Knuth-Bendix Completion Procedure. Diplomarbeit am Inst. f. Informatik I","author":"K\u00fc W. W.","year":"1982","unstructured":"{ K\u00fc 82} K\u00fcchlin W. W. : An Implementation and Investigation of the Knuth-Bendix Completion Procedure. Diplomarbeit am Inst. f. Informatik I , Univ. Karlsruhe , Karlsruhe W. Germ. April 1982 (Reprinted as Internal Report 17\/82). {K\u00fc82} K\u00fcchlin W. W.: An Implementation and Investigation of the Knuth-Bendix Completion Procedure. Diplomarbeit am Inst. f. Informatik I, Univ. Karlsruhe, Karlsruhe W. Germ. April 1982 (Reprinted as Internal Report 17\/82)."},{"key":"e_1_2_1_11_1","volume-title":"LNCS 144","author":"K\u00fc W. W.","year":"1982","unstructured":"{ K\u00fc 82a} K\u00fcchlin W. W. : A Theorem-Proving Approach to the Knuth-Bendix Completion Algorithm. In \"Computer Algebra \", LNCS 144 , Springer Verlag 1982 . {K\u00fc82a} K\u00fcchlin W. W.: A Theorem-Proving Approach to the Knuth-Bendix Completion Algorithm. In \"Computer Algebra\", LNCS 144, Springer Verlag 1982."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1093390.1093395"},{"key":"e_1_2_1_13_1","volume-title":"Musser D. R.: A Data Type Verification System Based on Rewrite Rules. 6th Texas Conf. on Computing Systems","author":"Mu","year":"1978","unstructured":"{ Mu 78} Musser D. R.: A Data Type Verification System Based on Rewrite Rules. 6th Texas Conf. on Computing Systems , Austin, Texas , November 1978 . {Mu78} Musser D. R.: A Data Type Verification System Based on Rewrite Rules. 6th Texas Conf. on Computing Systems, Austin, Texas, November 1978."},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-08531-9","volume-title":"Computing in Systems Described by Equations. LNCS 58","author":"O'Donnell M. J.","year":"1977","unstructured":"{OD77} O'Donnell M. J. : Computing in Systems Described by Equations. LNCS 58 , Springer 1977 . {OD77} O'Donnell M. J.: Computing in Systems Described by Equations. LNCS 58, Springer 1977."}],"container-title":["ACM SIGSAM Bulletin"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1089310.1089315","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1089310.1089315","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:08:23Z","timestamp":1750262903000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1089310.1089315"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1982,11]]},"references-count":12,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1982,11]]}},"alternative-id":["10.1145\/1089310.1089315"],"URL":"https:\/\/doi.org\/10.1145\/1089310.1089315","relation":{},"ISSN":["0163-5824"],"issn-type":[{"type":"print","value":"0163-5824"}],"subject":[],"published":{"date-parts":[[1982,11]]},"assertion":[{"value":"1982-11-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}