Implementation of an interpreter for abstract equations

ABSTRACT

This paper summarizes a project, introduced in [HO79, HO82b], whose goal is the implementation of a useful interpreter for abstract equations that is absolutely faithful to the logical semantics of equations. The Interpreter was first distributed to Berkeley UNIX VAX sites in May, 1983. The main novelties of the interpreter are (1) strict adherence to semantics based on logical consequences; (2) “lazy” (outermost)evaluation applied uniformly; (3) an implementation based on table-driven pattern matching, with no run-time penalty for large sets of equations; (4) strict separation of syntactic and semantic processing, so that different syntaxes may be used for different problems.

REFERENCES

• 1: Alfred V. Aho , Margaret J. Corasick, Efficient string matching: an aid to bibliographic search, Communications of the ACM, v.18 n.6, p.333-340, June 1975 [doi>10.1145/360825.360855]
• 2: Alfred V. Aho , John E. Hopcroft, The Design and Analysis of Computer Algorithms, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1974
• 3: Alfred V. Aho , Jeffrey D. Ullman, The Theory of Parsing, Translation, and Compiling, Prentice Hall Professional Technical Reference, 1972
• 4: Ashcroft, E. and W. Wadge, Lucid - A Formal System for Writing and Proving Programs. SIAM Journal on Computing 5:3, 1976, 336:354.
• 5: E. A. Ashcroft , W. W. Wadge, Lucid, a nonprocedural language with iteration, Communications of the ACM, v.20 n.7, p.519-526, July 1977 [doi>10.1145/359636.359715]
• 6: John Backus, Programming language semantics and closed applicative languages, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.71-86, October 01-03, 1973, Boston, Massachusetts [doi>10.1145/512927.512934]
• 7: 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]
• 8: Friedrich L. Bauer , Manfred Broy , Rupert Gnatz , Wolfgang Hesse , Bernd Krieg-Brückner , Helmuth Partsch , Peter Pepper , Hans Wössner, Towards a Wide Spectrum Language to Support Program Specification and Program Development, Program Construction, International Summer Schoo, p.543-552, July 26-August 06, 1978
• 9: Gérard Berry , Jean-Jacques Lévy, Minimal and optimal computations of recursive programs, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.215-226, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512971]
• 10: Bérry, G. and Lévy, J. J. Letter to the Editor, SIGACT News, v. 11, no. 1, Summer 1979, 3-4.
• 11: Bjorner, D. Finite State Tree Computations (Part I). IBM Research Technical Report RJ 1053 (#17598), 1972.
• 12: Bruynooghe, M., An Interpreter for Predicate Logic Programs Part I, Report CWI0, Applied Mathematics and Programming Division, Katholieke Universiteit, Leuven, Belgium, 1976.
• 13: Burstall, R. M. and Goguen, J. A. Putting Theories Together to Make Specifications. 5th International Joint Conference on Artificial Intelligence, Cambridge, Mass., 1965.
• 14: Burstall, R., MacQueen, D., Sannella, D. HOPE: An Experimental Applicative Language. Internal Report CSR-62-80, University of Edinburgh, 1980.
• 15: Jean-Marie Cadiou, Recursive definitions of partial functions and their computations, 1972
• 16: Cargill, T., Deterministic Operational Semantics for Lucid, Research Report C'S-76-19, University of Waterloo, 1976.
• 17: Chew, L. P. An Improved Algorithm for Computing With Equations. 21st Annual Symposium on Foundations of Computer Science, 1980, 108-117.
• 18: Alonzo Church, The Calculi of Lambda Conversion. (AM-6) (Annals of Mathematics Studies), Princeton University Press, Princeton, NJ, 1985
• 19: de Bruijn, N. G. Lambda Ca1culus Notation with Nameless Dummies, Nederl. Akad. Wetensch. Proc. Series A 75, 1972, 381-392.
• 20: Curry, H. B., and Feys, R., Combinatory Logic volume I. North-Holland, Amsterdam, 1958.
• 21: Downey, P. and R. Sethi, Correct Computation Rules for Recursive Languages. SIAM Journal on Computing 5:3, 1976, 378-401.
• 22: Mansour Farah, Correct compilation of a useful subset of lucid., 1977
• 23: Friedman, D., and D. Wise, Cons should not evaluate its arguments, 3rd International Colloquium on Automata, Languages and Programming, Edinburgh, Edinburgh University Press, 1976, 257-284.
• 24: Ingrid Glasner , Ulrich Möncke , Reinhard Wilhelm, OPTRAN, a Language for the Specification of Program Transformations, Programmiersprachen und Programmentwicklung, 6. Fachtagung des Fachausschusses Programmiersprachen der GI, p.125-142, March 11-12, 1980
• 25: Goguen, J., Abstract Errors for Abstract Data Types, IFIP Working Conference on Formal Description of Programming Concepts, E. J. Neuhold, ed., North-Holland, 1977,
• 26: Guibas, L. and R. Sedgewick, A Dichromatic Frame-work for Balanced Trees, 19th Symposium on Foundations of computer Science, 1978, 8-21.
• 27: Guttag, J., E. Horowitz and D. Musser, Abstract Data Types and Software Validation, Information Science Research Report ISI/RR-76-48, University of Southern California, 1976.
• 28: Peter Henderson , James H. Morris, Jr., A lazy evaluator, Proceedings of the 3rd ACM SIGACT-SIGPLAN symposium on Principles on programming languages, p.95-103, January 19-21, 1976, Atlanta, Georgia [doi>10.1145/800168.811543]
• 29: Hoffmann, C., Design and Correctness of a Compiler for a Nonprocedural Language, Acta Informatica 9, 1978, 217-241.
• 30: Christoph M. Hoffmann , Michael J. O'Donnell, An interpreter generator using tree pattern matching, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.169-179, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567768]
• 31: 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]
• 32: Christoph M. Hoffman , Michael J. O'Donnell, Programming with Equations, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.1, p.83-112, Jan. 1982 [doi>10.1145/357153.357158]
• 33: Huet, G. and J.-J. Lévy, Computations in Non-ambiguous Linear Term Rewriting Systems, IRIA Technical Report #359, 1979.
• 34: Johnson, S. D., An Interpretive Model for a Language Based on Suspended Construction, Technical Report #68, Dept. of Computer Science, Indiana University, 1977.
• 35: Kahn, G. and MacQueen, D. B. Coroutines and Networks of Parallel Processes, Information Processing 77, B. Gilchrist ed., North-Holland, 1977, 993-998.
• 36: Knuth, D., J. Morris and V. Pratt, Fast Pattern Matching in Strings, SIAM J. on Comp. 6:2 (1977)323-350
• 37: Klop, J. W. Combinatory Reduction Systems, Ph.D.dissertation, Mathematisch Centrum, Amsterdam, 1980.
• 38: Knuth, D., and P. Bendix, Simple Word Problems inUniversal Algebras. Computational Problems in Abstract Algebra. J. Leech, ed., Pergammon Press, Oxford, 1970, 263-297.
• 39: Robert Kowalski, Algorithm = logic + control, Communications of the ACM, v.22 n.7, p.424-436, July 1979 [doi>10.1145/359131.359136]
• 40: 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]
• 41: McIlroy, M. D., Coroutines, Internal report, Bell Telephone Laboratories, Murray Hill, New Jersey, May 1968.
• 42: Möncke, U. An Incremental and Decremental Generator for Tree Analysers Bericht Nr. A 80/3, Fachber. Informatik Univ. des Saarlandes, Saarbrücken, April 1980
• 43: Greg Nelson , Derek C. Oppen, A simplifier based on efficient decision algorithms, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.141-150, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512775]
• 44: Greg Nelson , Derek C. Oppen, Fast Decision Procedures Based on Congruence Closure, Journal of the ACM (JACM), v.27 n.2, p.356-364, April 1980 [doi>10.1145/322186.322198]
• 45: Michael J. O'Donnell, Computing in Systems Described by Equations, Springer-Verlag New York, Inc., Secaucus, NJ, 1977
• 46: O'Donnell, M. J. Letter to the Editor, SIGACT News, v. 11, no. 2, Fall 1979, p. 2.
• 47: Roberts, G., An Implementation of PROLOG, M.S. Thesis, Dept. of Computer Science, University of Waterloo, 1977.
• 48: Barry K. Rosen, Tree-Manipulating Systems and Church-Rosser Theorems, Journal of the ACM (JACM), v.20 n.1, p.160-187, Jan. 1973 [doi>10.1145/321738.321750]
• 49: Staples, J., A Class of Replacement Systems with Simple Optimality Theory, Bulletin of the Australian Mathematical Society, 17:3, 1977, 335-350.
• 50: John Staples, A Graph-Like Lambda Calculus for Which Leftmost-Overmost Reduction is Optimal, Proceedings of the International Workshop on Graph-Grammars and Their Application to Computer Science and Biology, p.440-455, October 30-November 03, 1978
• 51: Stenlund, S. Combinators, Lambda-Terms, and Proof Theory. D. Reidel Publishing Company, Dordrecht, Holland, 1972.
• 52: Vuillemin, J., Correct and Optimal implementations of Recursion in a Simple Programming Language, JCSS 9:3, 1974, 332-354.
• 53: Wand, M., First Order Identities as a Defining Language, Technical Report #29, Dept. of Computer Science, Indiana University, 1976.
• 54: Warren, D., Implementing PROLOG, Research Reports #39, 40, Dept. of Artificial Intelligence, University of Edinburgh, 1977.

INDEX TERMS

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

Additional Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Pattern matching

General Terms:
Design, Performance