Within ARM's reach: compilation of left-linear rewrite systems via minimal rewrite systems

ABSTRACT

A new compilation technique for left-linear term-rewriting systems is presented, where rewrite rules are transformed into so-called minimal rewrite rules. These minimal rules have such a simple form that they can be viewed as instructions for an abstract rewriting machine (ARM).

REFERENCES

• 1: Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• 2: Martin Alt , Christian Fecht , Christian Ferdinand , Reinhard Wilhelm, Transformation Development: TrafoLa-H Subsystem, Program Development by Specification and Transformation, The PROSPECTRA Methodology, Language Family, and System, p.539-576, January 1993
• 3: L. Augustsson , T. Johnsson, The Chalmers lazy ML-compiler, The Computer Journal, v.32 n.2, p.127-141, April 1989 [doi>10.1093/comjnl/32.2.127]
• 4: John Backus, Can programming be liberated from the von Neumann style?: a functional style and its algebra of programs, Communications of the ACM, v.21 n.8, p.613-641, Aug. 1978 [doi>10.1145/359576.359579]
• 5: J. C. M. Baeten , J. A. Bergstra , J. W. Klop , W. P. Weijland, Term-rewriting systems with rule priorities, Theoretical Computer Science, v.67 n.2-3, p.283-301, Oct. 1989 [doi>10.1016/0304-3975(89)90006-6]
• 6: J. A. Bergstra , Jan Heering , Paul Klint, Algebraic specification, ACM Press, New York, NY, 1989
• 7: J A Bergstra , J W Klop, Conditional rewrite rules: Confluence and termination, Journal of Computer and System Sciences, v.32 n.3, p.323-362, June 1986 [doi>10.1016/0022-0000(86)90033-4]
• 8: BURSTALL, R. M. AND LANDIN, P. J. 1969. Programs and their proofs: An algebraic approach. In Proceedings of the ~th Workshop on Machine Intelligence, B. Melzer and D. Michie, Eds. Edinburgh University Press, Edinburgh, 17-43.
• 9: CANN, D. C. 1992. The optimizing SISAL compiler: Version 12.0. Manual UCRL-MA- 110080, Lawrence Livermore National Laboratory, Livermore, Calif. Available via ftp as sisal.llnl.gov/pub/sisal/OSC-manual.ps.
• 10: Luca Cardelli, Compiling a functional language, Proceedings of the 1984 ACM Symposium on LISP and functional programming, p.208-217, August 06-08, 1984, Austin, Texas, United States [doi>10.1145/800055.802037]
• 11: Jacques Cohen, Garbage Collection of Linked Data Structures, ACM Computing Surveys (CSUR), v.13 n.3, p.341-367, Sept. 1981 [doi>10.1145/356850.356854]
• 12: Thomas T. Cormen , Charles E. Leiserson , Ronald L. Rivest, Introduction to algorithms, MIT Press, Cambridge, MA, 1990
• 13: G. Cousineau , P.-L. Curien, The categorical abstract machine, Science of Computer Programming, v.8 n.2, p.173-202, April 1, 1987 [doi>10.1016/0167-6423(87)90020-7]
• 14: Nachum Dershowitz , Jean-Pierre Jouannaud, Rewrite systems, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 15: FOKKINK, W. J. AND VAN DE POL, J. C. 1996. Correct implementation of rewrite systems for implementation purposes. Logic Group Preprint Series 164, Utrecht University, Utrecht. Available at http:////www.phil.ruu.nl//preprints.html.
• 16: Wan Fokkink , Jaco van de Pol, Simulation as a Correct Transformation of Rewrite Systems, Proceedings of the 22nd International Symposium on Mathematical Foundations of Computer Science, p.249-258, August 25-29, 1997
• 17: Pascal Fradet , Daniel Le Métayer, Compilation of functional languages by program transformation, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.1, p.21-51, Jan. 1991 [doi>10.1145/114005.102805]
• 18: M. Gordon , R. Milner , L. Morris , M. Newey , C. Wadsworth, A Metalanguage for interactive proof in LCF, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.119-130, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512773]
• 19: Lutz H. Hamel , Joseph A. Goguen, Towards a Provably Correct Compiler for OBJ3, Proceedings of the 6th International Symposium on Programming Language Implementation and Logic Programming, p.132-146, September 14-16, 1994
• 20: HARTEL, P. H., FEELEY, M., ALT, M., AUGUSTSSON, L., BAUMANN, P., BEEMSTER, M., CHAILLOUX, E., FLOOD, C. H., GRIESKAMP, W., VAN GRONINGEN, J. H. G., HAMMOND, K., HAUSMAN, B., IVORY, M. Y., JONES, R. E., KAMPERMAN, J. F. WH., LEE, P., LEROY, X., LINS, R. D., LOOSE- MORE, S., RJEMO, N., SERRANO, M., TALPIN, J.-P., THACKRAY, J., THOMAS, S., WALTERS, H. R., WEIS, P., AND WENTWORTH, P. 1996. Benchmarking implementations of functional languages with "pseudoknot", a float-intensive benchmark. J. Funct. Program. 6, 4, 621-655.
• 21: J. Heering , P. R. H. Hendriks , P. Klint , J. Rekers, The syntax definition formalism SDF—reference manual—, ACM SIGPLAN Notices, v.24 n.11, p.43-75, Nov. 1989 [doi>10.1145/71605.71607]
• 22: Christoph M. Hoffmann , Michael J. O'Donnell, Pattern Matching in Trees, Journal of the ACM (JACM), v.29 n.1, p.68-95, Jan. 1982 [doi>10.1145/322290.322295]
• 23: Paul Hudak , Simon Peyton Jones , Philip Wadler , Brian Boutel , Jon Fairbairn , Joseph Fasel , María M. Guzmán , Kevin Hammond , John Hughes , Thomas Johnsson , Dick Kieburtz , Rishiyur Nikhil , Will Partain , John Peterson, Report on the programming language Haskell: a non-strict, purely functional language version 1.2, ACM SIGPLAN Notices, v.27 n.5, p.1-164, May 1992 [doi>10.1145/130697.130699]
• 24: Thomas Johnsson, Efficient compilation of lazy evaluation, ACM SIGPLAN Notices, v.19 n.6, p.58-69, June 1984
• 25: KAMPERMAN, J. F. WH. 1996. Compilation of term rewriting systems. Ph.D. thesis, University of Amsterdam, Amsterdam. Available at http://www.babelfish.nl.
• 26: KAMPERMAN, J. F. WH. AND WALTERS, H. R. 1993. ARM--abstract rewriting machinery. In Proceedings of Computer Science in the Netherlands. Stichting Mathematisch Centrum, Aresterdam, 193-204.
• 27: J. F. Th. Kamperman , H. R. Walters, Lazy Rewriting and Eager Machinery, Proceedings of the 6th International Conference on Rewriting Techniques and Applications, p.147-162, April 05-07, 1995
• 28: J. F. Th. Kamperman , H. R. Walters, Minimal Term Rewriting Systems, Selected papers from the 11th Workshop on Specification of Abstract Data Types Joint with the 8th COMPASS Workshop on Recent Trends in Data Type Specification, p.274-290, September 19-23, 1995
• 29: H. Klaeren , K. Indermark, Efficient implementation of an algebraic specification language, Algebraic methods: theory, tools and applications, Springer-Verlag New York, Inc., New York, NY, 1989
• 30: P. Klint, A meta-environment for generating programming environments, ACM Transactions on Software Engineering and Methodology (TOSEM), v.2 n.2, p.176-201, April 1993 [doi>10.1145/151257.151260]
• 31: J. W. Klop, Term rewriting systems, Handbook of logic in computer science (vol. 2): background: computational structures, Oxford University Press, Inc., New York, NY, 1993
• 32: LANDIN, P. 1964. The mechanical evaluation of expressions. Comput. J. 6, 4, 308-320.
• 33: P. J. Landin, The next 700 programming languages, Communications of the ACM, v.9 n.3, p.157-166, March 1966 [doi>10.1145/365230.365257]
• 34: David Lester, The G-machine as a representation of stack semantics, Proc. of a conference on Functional programming languages and computer architecture, p.46-59, October 1987, Portland, Oregon, United States
• 35: John McCarthy, Recursive functions of symbolic expressions and their computation by machine, Part I, Communications of the ACM, v.3 n.4, p.184-195, April 1960 [doi>10.1145/367177.367199]
• 36: MCCARTHY, J. 1963. Towards a mathematical science of computation. In Proceedings of Informarion Processing '62. North-Holland, Amsterdam, 21-28.
• 37: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 38: F. Lockwood Morris, Advice on structuring compilers and proving them correct, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.144-152, October 01-03, 1973, Boston, Massachusetts [doi>10.1145/512927.512941]
• 39: Mikael Pettersson, A Term Pattern-Match Compiler Inspired by Finite Automata Theory, Proceedings of the 4th International Conference on Compiler Construction, p.258-270, October 05-07, 1992
• 40: Simon L. Peyton Jones , David R. Lester, Implementing functional languages, Prentice-Hall, Inc., Upper Saddle River, NJ, 1992
• 41: Simon L. Peyton Jones , Jon Salkild, The spineless tagless G-machine, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.184-201, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99385]
• 42: J Rees , W Clinger, Revised report on the algorithmic language scheme, ACM SIGPLAN Notices, v.21 n.12, p.37-79, Dec. 1986 [doi>10.1145/15042.15043]
• 43: SASSA, M. AND GOTO, E. 1976. A hashing method for fast set operations. Inf. Process. Lett. 5, 2, 31-34.
• 44: Satish R. Thatte, On the correspondence between two classes of reduction systems, Information Processing Letters, v.20 n.2, p.83-85, Feb. 1985 [doi>10.1016/0020-0190(85)90068-7]
• 45: WURNER, D. A. 1979. A new implementation technique for applicative languages. Softw. Pract. Exper. 9, 1, 31-49.
• 46: D. A. Turner, Miranda: a non-strict functional language with polymorphic types, Proc. of a conference on Functional programming languages and computer architecture, p.1-16, January 1985, Nancy, France
• 47: VAN DEN BRAND, M. G. J. 1997. The missing links. In Liber Amicorum Paul Klint. CWI, Amsterdam, 55-60.
• 48: Arie Van Deursen , Jan Heering , Paul Klint, Language Prototyping: An Algebraic Specification Approach: Vol. V, World Scientific Publishing Co., Inc., River Edge, NJ, 1996
• 49: WALTERS, H. R. 1991. On equal terms, implementing algebraic specifications. Ph.D. thesis, University of Amsterdam, Amsterdam. Available at http://www.babelfish.nl.
• 50: H. R. Walters, Epic and ARM -- user''s guide --, CWI (Centre for Mathematics and Computer Science), Amsterdam, The Netherlands, 1997
• 51: H. R. Walters , Jasper F.T Kamperman, Epic 1.0 (unconditional) an equational programming language, CWI (Centre for Mathematics and Computer Science), Amsterdam, The Netherlands, 1996
• 52: H. R. Walters , J. F. Th. Kamperman, EPIC: An Equational Language -Abstract Machine Supporting Tools-, Proceedings of the 7th International Conference on Rewriting Techniques and Applications, p.424-427, July 27-30, 1996
• 53: WEIS, P. AND LEROY, X. 1993. Le Langage Carol. Intert~ditions, Paris.
• 54: S. C. Wray , J. Fairbairn, Non-strict languages-programming and implementation, The Computer Journal, v.32 n.2, p.142-151, April 1989 [doi>10.1093/comjnl/32.2.142]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Compilers

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Optimization

General Terms:
Languages

Keywords:
abstract machine, automata, specificity ordering, term rewriting