Advertisement

Abstract Data Types in Computer Algebra

  • James H. Davenport
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1893)

Abstract

The theory of abstract data types was developed in the late 1970s and the 1980s by several people, including the “ADJ” group, whose work influenced the design of Axiom. One practical manifestation of this theory was the OBJ-3 system. An area of computing that cries out for this approach is computer algebra, where the objects of discourse are mathematical, generally satisfying various algebraic rules. There have been various theoretical studies of this in the literature: [36, 42, 45] to name but a few.

The aim of this paper is to report on the practical applications of this theory within computer algebra, and also to outline some of the theoretical issues raised by this practical application. We also give a substantial bibliography.

Keywords

Computer Algebra Computer Algebra System Proof Obligation Type Inference Springer Lecture Note 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Abbott, J.A., Bradford, R.J& Davenport, J.H., The Bath Algebraic Number Package. Proc. SYMSAC 86, ACM, New York, 1986, pp. 250–253.CrossRefGoogle Scholar
  2. 2.
    Abdali, S.K., Cherry, G.W. & Soiffer, N., An Object-oriented Approach to Algebra System Design. Proc. SYMSAC 86, ACM, New York, 1986, pp. 24–30.CrossRefGoogle Scholar
  3. 3.
    Abdali, S.K., Cherry, G.W. & Soiffer, N., A Smalltalk System for Algebraic Manipulation. Proc. OOPSLA 86 SIGPLAN Notices 21 1986 11) pp. 277–283.CrossRefGoogle Scholar
  4. 4.
    Bareiss, E.H., Sylvester’s Identity and Multistep Integer-preserving Gaussian Elimination. Math. Comp. 22 1968 pp. 565–578. Zbl. 187,97.zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Becker, T. & Weispfeninng, V. (with H. Kredel), Groebner Bases. A Computational Approach to Commutative Algebra. Springer Verlag, Graduate Texts in Mathematics 141, 1993.Google Scholar
  6. 6.
    Boehm, H.-J., Cartwright, R., Riggle, M. & O’Donnell, M.J., Exact Real Arithmetic: A Case Study in Higher Order Programming. Proc. LISP & Functional Programming (ACM, 1986) pp. 162–173.Google Scholar
  7. 7.
    Bogen, R.A. et al., MACSYMA Reference Manual (version 9). M.I.T. Laboratory for Computer Science, Cambridge, Mass., 1977.Google Scholar
  8. 8.
    Bosma, W., Cannon, J.& Matthews, G., Programming with algebraic structures: design of the Magma language. Proc. ISSAC 1994, ACM, New York, 1994, pp. 52–57.CrossRefGoogle Scholar
  9. 9.
    Bosma, W., Cannon, J.& Playoust, C., The Magma algebra system. I: The user language. J. Symbolic Comp. 24 1997 pp. 235–265. Zbl. 898.68039.zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Bradford, R.J., Hearn, A.C., Padget, J.A. & Schrufer, E., Enlarging the REDUCE Domain of Computation. Proc. SYMSAC 86, ACM, New York, 1986, pp. 100–106.CrossRefGoogle Scholar
  11. 11.
    Comon, H., Lugiez, D. & Schnoebelen, P., A rewrite-based type discipline for a subset of computer algebra. J. Symbolic Comp. 11 1991 pp. 349–368.zbMATHMathSciNetCrossRefGoogle Scholar
  12. 12.
    Coppo, M., An extended polymorphic type system for applicative languages. Proc. MFCS 80 (Springer Lecture Notes in Computer Science, Springer-Verlag, Berlin-Heidelberg-New York), pp. 194–204.Google Scholar
  13. 13.
    Davenport, J.H. & Trager, B.M., Scratchpad’s View of Algebra I: Basic Commutative Algebra. Proc. DISCO’ 90 Springer Lecture Notes in Computer Science Vol. 429, ed. A. Miola, Spinger-Verlag, 1990, pp. 40–54. A revised version is in Axiom Technical Report ATR/1, Nag Ltd., December 1992.Google Scholar
  14. 14.
    Davenport, J.H., Gianni, P.& Trager, B.M., Scratchpad’s View of Algebra II: A Categorical View of Factorization. Proc. ISSAC 1991 ed. S.M. Watt, ACM, New York, pp. 32–38. A revised version is in Axiom Technical Report ATR/2, Nag Ltd., December 1992.Google Scholar
  15. 15.
    Dodgson, C.L., Condensation of determinants, being a new and brief method for computing their algebraic value. Proc. Roy. Soc. Ser. A 15 1866 pp. 150–155.CrossRefGoogle Scholar
  16. 16.
    Doye, N.J., Order Sorted Computer Algebra and Coercions. Ph.D. Thesis, University of Bath, 1997. http://www.bath.ac.uk/~ccsnjd/research/phd.ps http://www.nic.uklinux.net/research/phd.ps
  17. 17.
    Doye, N.J., Automated Coercion for Axiom. Proc. ISSAC 1999 ed. S. Dooley, ACM, New York, 1999, pp. 229–235.CrossRefGoogle Scholar
  18. 18.
    Dunstan, M.N., Larch/Aldor-A Larch BISL for AXIOM and Aldor. Ph.D. Thesis, University of St. Andrews, 1999.Google Scholar
  19. 19.
    Dunstan, M., Kelsey, T., Linton, S.& Martin, U., Lightweight Formal Methods for Computer Algebra Methods. Proc. ISSAC 1998 ed. O. Gloor, ACM, New York, 1998, pp. 80–87.CrossRefGoogle Scholar
  20. 20.
    Dunstan, M., Kelsey, T., Linton, S. & Martin, U., Formal methods for extensions to CAS. FM’ 99 Vol. II Springer Lecture Notes in Computer Science Vol. 1709, ed. J.W.J. Wing, J. Woodcock & J. Davies, Springer-Verlag, 1999, pp. 1758–1777.Google Scholar
  21. 21.
    Ehrig, H.-D., On the Theory of Specification, Implementation and Parameterization of Abstract Data Types. J. A CM 29 1982 pp. 206–227. MR 83g:68030.Google Scholar
  22. 22.
    Ehrig, H.& Mahr, B., Fundamentals of Algebraic Specification 1: Equations and Initial Semantics. EATCS Monographs in Theoretical Computer Science 6, Springer-Verlag, Berlin, 1985.Google Scholar
  23. 23.
    Faugére, J.-C., Gianni, P., Lazard, D.& Mora, T., Efficient Computation of Zero-Dimensional Gröbner Bases by Change of Ordering. J. Symbolic Comp. 16 1993 pp. 329–344.zbMATHCrossRefGoogle Scholar
  24. 24.
    Fortenbacher, A., Efficient Type Inference and Coercion in Computer Algebra. Proc. DISCO’ 90 Springer Lecture Notes in Computer Science Vol. 429, ed. A. Miola pp. 56–60.Google Scholar
  25. 25.
    Fröhlich, A.& Shepherdson, J.C., Effective Procedures in Field Theory. Phil. Trans. Roy. Soc. Ser. A 248 1955–6 pp. 407–432. Zbl. 70,35.CrossRefGoogle Scholar
  26. 26.
    Goguen, J.A. & Malcolm, G. (eds.), Software Engineering with OBJ: algebraic specification in action. Kluwer, 2000.Google Scholar
  27. 27.
    Goguen, J.A. & Meseguer, J., Order-sorted Algebra I: Equational deduction for multiple inheritance, polymorphism and partial operations. Theor. Comp. Sci. 105 1992 pp. 217–293.zbMATHCrossRefMathSciNetGoogle Scholar
  28. 28.
    Goguen,J.A., Thatcher, J.W., Wagner, E.G. & Wright, J.B., A Junction Between Computer Science and Category Theory I: Basic Concepts and Examples (Part 1). IBM Research RC 4526, 11 September 1973.Google Scholar
  29. 29.
    Goguen, J.A., Thatcher, J.W., Wagner, E.G.& Wright, J.B., An Introduction to Categories, Algebraic Theories and Algebras. IBM Research RC 5369, 16 April 1975.Google Scholar
  30. 30.
    Goguen, J.A., Thatcher, J.W., Wagner, E.G. & Wright, J.B., A Junction Between Computer Science and Category Theory I: Basic Concepts and Examples (Part 2). IBM Research RC 5908, 18 March 1976.Google Scholar
  31. 31.
    Goguen, J.A., Thatcher, J.W., Wagner, E.G.& Wright, J.B., Initial Algebra Semantics and Continuous Algebras. J. A CM 24 1977 pp. 68–95.zbMATHMathSciNetGoogle Scholar
  32. 32.
    Gruntz, D. & Monagan, M., Introduction to Gauss. MapleTech: The Maple Technical Newsletter, Issue 9, Spring 1993, pp. 23–49.Google Scholar
  33. 33.
    Guttag, J.V. & Horning, J.J., Larch: Languages and Tools for Formal Specification. Texts and Monographs in Computer Science, Springer-Verlag, 1993.Google Scholar
  34. 34.
    Hearn, A.C., REDUCE User’s Manual, Version 3.4, July 1991. RAND Corporation Publication CP-78.Google Scholar
  35. 35.
    Hearn, A.C. & Schrüfer, E., An Order-Sorted Approach to Algebraic Computation. Proc. DISCO’ 93 ed. A. Miola, Springer Lecture Notes in Computer Science 722, Springer-Verlag, 1993, pp. 134-144.Google Scholar
  36. 36.
    Hohfeld, B., Correctness Proofs of the Implementation of Abstract Data Types. Proc. EUROCAL 85, Vol. 2 Springer Lecture Notes in Computer Science Vol. 204, Springer-Verlag, 1985) pp. 446–447.Google Scholar
  37. 37.
    Hur, N., A Symbolic and Numeric Approach to Real Number Computation. Draft Ph.D. Thesis, University of Bath, 2000.Google Scholar
  38. 38.
    Hur, N. & Davenport, J.H., An Exact Real Algebraic Arithmetic with Equality Determination. Proc. ISSAC 2000 ed. C. Traverso, pp. 169–174.Google Scholar
  39. 39.
    Jenks, R.D. & Sutor, R.S., AXIOM: The Scientific Computation System. Springer-Verlag, New York, 1992.zbMATHGoogle Scholar
  40. 40.
    Jenks, R.D. & Trager, B.M., A Language for Computational Algebra. Proc. SYM-SAC 81, ACM, New York, 1981, pp. 6–13. Reprinted in SIGPLAN Notices 16 1981 No. 11, pp. 22–29.Google Scholar
  41. 41.
    Kelsey, T.W., Formal Methods and Computer Algebra: A Larch Specification of Axiom Categories and Functors. Ph.D. Thesis, St. Andrews, 2000.Google Scholar
  42. 42.
    Kounalis, E., Completeness in Data Type Specifications. Proc. EUROCAL 85, Vol. 2 Springer Lecture Notes in Computer Science Vol. 204, Springer-Verlag, 1985) pp. 348–362.Google Scholar
  43. 43.
    Ménissier-Morain, V., Arithmétique exacte, conception, algorithmique et performances d’une implémentation informatique en précision arbitraire. Thése, Université Paris 7, Dec. 1994.Google Scholar
  44. 44.
    Monagan, B., Gauss: A Parameterized Domain of Computation System with Support for Signature Functions. Proc. DISCO’ 93 ed. A. Miola, Springer Lecture Notes in Computer Science 722, Springer-Verlag, 1993, pp. 81–94.Google Scholar
  45. 45.
    Musser, D.R. & Kapur, D., Rewrite Rule Theory and Abstract Data Type Analysis. Proc. EUROCAM 82 Springer Lecture Notes in Computer Science 144, Springer-Verlag, Berlin-Heidelberg-New York, 1982), pp. 77–90. MR 83m:68022.Google Scholar
  46. 46.
    Naylor, W.A., Polynomial GCD Using Straight Line Program Representation. Ph.D. Thesis, University of Bath, 2000.Google Scholar
  47. 47.
    Nordström, B., Petersson, K.& Smith, J.M., Programming in Martin-Löf’ Type Theory — An Introduction. OUP, 1990.Google Scholar
  48. 48.
    Poll, E. & Thompson, S., Integrating Computer Algebra and Reasoning through the Type System of Aldor. Proc. Frontiers of Combining Systems: FroCoS 2000 Springer Lecture Notes in Computer Science 1794, Springer-Verlag, 2000, ed. H. Kirchner & C. Ringeissen.CrossRefGoogle Scholar
  49. 49.
    Rector, D.L., Semantics in Algebraic Computation. Computers and Mathematics ed. E. Kaltofen & S.M. Watt, Springer-Verlag, 1989, pp. 299–307.Google Scholar
  50. 50.
    Reynaud, J.-C., Putting Algebraic Components Together: A Dependent Type Approach. Proc. DISCO’ 90 Springer Lecture Notes in Computer Science Vol. 429, ed. A. Miola pp. 141–150.Google Scholar
  51. 51.
    Reynolds, J.C., Using Category Theory to Design Implicit Conversions and Generic Operators. Semantics-Directed Compiler Generation Springer Lecture Notes in Computer Science 94, ed. N.D. Jones, 1980, pp. 211–258.Google Scholar
  52. 52.
    Rotman, J.J., An Introduction to the Theory of Groups. Springer Graduate Texts in Mathematics 148, Springer-Verlag, 1995.Google Scholar
  53. 53.
    Stoutemyer, D.R., Which Polynomial Representation is Best: Surprises Abound. Proc. 1984 MACSYMA Users’ Conference (ed. V.E. Golden), G.E., Schenectady, pp. 221–243.Google Scholar
  54. 54.
    Sutor, R.S. & Jenks, R.D., The Type Inference and Coercion Facilities in the Scratchpad II Interpreter. Proc. SIGPLAN’ 87 Symp. Interpreters and Interpretive Techniques SIGPLAN Notices 22 (1987) pp. 56–63.CrossRefGoogle Scholar
  55. 55.
    Thatcher, J.W., Wagner, E.G.& Wright, J.B., Notes on Algebraic Fundamentals for Theoretical Computer Science. Foundations of Computer Science III (ed. J.W. de Bakker & J. van Leeuwen), Mathematical Centre Tract 109, Amsterdam, 1979.Google Scholar
  56. 56.
    Thatcher, J.W., Wagner, E.G. & Wright, J.B., Data Type Specification: Parameterization and the Power of Specification Techniques. ACM TOPLAS 4 (1982) pp. 711–732.zbMATHCrossRefGoogle Scholar
  57. 57.
    Thompson, S., Logic and dependent types in the Aldor Computer Algebra System. To appear in Proc. Calculemus 2000.Google Scholar
  58. 58.
    Watt, S.M., Broadbery, P.A., Dooley, S.S., Iglio, P., Morrison, S.C., Steinbach, J.M. & Sutor, R.S., Axiom Library Compiler User Guide. NAG Ltd., Oxford, 1994.Google Scholar
  59. 59.
    Weber, A., Algorithms for type inference with coercions. Proc. ISSAC 1994, ACM, New York, 1994, pp. 324–329.CrossRefGoogle Scholar
  60. 60.
    Zippel, R.E., The Weyl Computer Algebra Substrate. Proc. DISCO’ 93 (ed. A. Miola), Springer Lecture Notes in Computer Science 722, Springer-Verlag, 1993, pp. 303–318.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • James H. Davenport
    • 1
  1. 1.Department of Mathematical SciencesUniversity of BathBathEngland

Personalised recommendations