Abstract versus concrete computation on metric partial algebras

Abstract

In the theory of computation on topological algebras there is a considerable gap between so-called abstract and concrete models of computation. In concrete models, unlike abstract models, the computations depend on the representation of the algebra. First, we show that with abstract models, one needs algebras with <i>partial operations</i>, and computable functions that are both <i>continuous</i> and <i>many-valued</i>. This many-valuedness is needed even to compute single-valued functions, and so <i>abstract models must be nondeterministic even to compute deterministic problems</i>. As an abstract model, we choose the "while"-array programming language, extended with a nondeterministic "countable choice" assignment, called the <i><b>WhileCC*</b></i> model. Using this, we introduce the concept of <i>approximable many-valued computation</i> on metric algebras. For our concrete model, we choose metric algebras with <i>effective representations</i>. We prove:(1) for any metric algebra <i>A</i> with an effective representation α, <i><b>WhileCC*</b></i> approximability implies computability in α, and (2) also the converse, under certain reasonable conditions on <i>A</i>. From (1) and (2) we derive an equivalence theorem between abstract and concrete computation on metric partial algebras. We give examples of algebras where this equivalence holds.

References

1. Aberth, O. 1980. Computable Analysis. MIT Press, Cambridge, MA.
2. Aberth, O. 2001. Computable Calculus. Addison-Wesley, Reading, MA.
3. Apt, K. and Olderog, E.-R. 1991. Verification of Sequential and Concurrent Programs. Springer-Verlag, Berlin, Germany.
4. Blum, L., Cucker, F., Shub, M., and Smale, S. 1998. Complexity and Real Computation. Springer-Verlag, Berlin, Germany.
5. Blum, L., Shub, M., and Smale, S. 1989. On a theory of computation and complexity over the real numbers: NP-completeness, recursive functions and universal machines. Bull. Amer. Math. Soc. 21, 1--46.
6. Brattka, V. 1996. Recursive characterisation of computable real-valued functions and relations. Theoret. Comput. Sci. 162, 45--77.
7. Brattka, V. 1999. Recursive and computable operations over topological structures. Ph.D. dissertation, FernUniversität Hagen, Fachbereich Informatik, Hagen, Germany. Informatik Berichte 255, FernUniversität Hagen, July 1999.
8. Ceitin, G. 1959. Algebraic operators in constructive complete separable metric spaces. Dok. Akad. Nauk SSSR 128, 49--52.
9. de Bakker, J. 1980. Mathematical Theory of Program Correctness. Prentice Hall, Englewood Cliffs, NJ.
10. Dijkstra, E. 1976. A Discipline of Programming. Prentice Hall, Englewood Cliffs, NJ.
11. Edalat, A. 1995. Dynamical systems, measures, and fractals via domain theory. Inform. Computat. 120, 32--48.
12. Edalat, A. 1997. Domains for computation in mathematics, physics and exact real arithmetic. Bull. Symbol. Log. 3, 401--452.
13. Engelking, R. 1989. General Topology. Heldermann Verlag, Berlin, Lemge, Germany.
14. Goguen, J., Thatcher, J., and Wagner, E. 1978. An initial approach to the specification, correctness and implementation of abstract data types. In Current Trends in Programming Methodology, vol. 4: Data Structuring, R. Yeh, Ed. Prentice Hall, Englewood Cliffs, NJ, 80--149.
15. Grzegorczyk, A. 1955. Computable functions. Fundamenta Mathematicae 42, 168--202.
16. Grzegorczyk, A. 1957. On the defintions of computable real continuous functions. Fundamenta Mathematicae 44, 61--71.
17. Heath, M. 1997. Scientific Computing: An Introductory Survey. McGraw-Hill, New York, NY.
18. Lacombe, D. 1955. Extension de la notion de fonction récursive aux fonctions d'une ou plusieurs variables réelles, I, II, III. C.R. Acad. Sci. Paris. 240, 2470--2480; 241, 13--14, 151--153.
19. Meseguer, J. and Goguen, J. 1985. Initiality, induction and computability. In Algebraic Methods in Semantics, M. Nivat and J. Reynolds, Eds. Cambridge University Press, Cambridge, U.K., 459--541.
20. Moschovakis, Y. 1964. Recursive metric spaces. Fundamenta Mathematicae 55, 215--238.
21. Odifreddi, P. 1999. Classical Recursion Theory, 21st ed. North Holland, Amsterdam, The Netherlands.
22. Pour-El, M. and Richards, J. 1989. Computability in Analysis and Physics. Springer-Verlag, Berlin, Germany.
23. Royden, H. 1963. Real Analysis. Macmillan, London, U.K.
24. Spreen, D. 1998. On effective topological spaces. J. Symbol. Log. 63, 185--221.
25. Spreen, D. 2001. Representations versus numberings: On the relationship of two computability notions. Theoret. Comput. Sci. 263, 473--499.
26. Stephenson, K. 1996. An algebraic approach to syntax, semantics and computation. Ph.D. dissertation, Department of Computer Science, University of Wales, Swansea, U.K.
27. Stewart, K. 1998. Concrete and abstract models of computation over metric algebras. Ph.D. dissertation, Department of Computer Science, University of Wales, Swansea, U.K.
28. Stoltenberg-Hansen, V. and Tucker, J. 1988. Complete local rings as domains. J. Symbol. Log. 53, 603--624.
29. Stoltenberg-Hansen, V. and Tucker, J. 1995. Effective algebras. In Handbook of Logic in Computer Science, S. Abramsky, D. Gabbay, and T. Maibaum, Eds. Vol. 4. Oxford University Press, Oxford, U.K., 357--526.
30. Stoltenberg-Hansen, V. and Tucker, J. 1999. Concrete models of computation for topological algebras. Theoret. Comput. Sci. 219, 347--378.
31. Taylor, A. and Lay, D. 1980. Introduction to Functional Analysis. John Wiley & Sons, New York, NY.
32. Tucker, J. and Zucker, J. 1988. Program Correctness over Abstract Data Types, with Error-State Semantics. CWI Monographs, vol. 6. North Holland, Amsterdam, The Netherlands.
33. Tucker, J. and Zucker, J. 1992a. Examples of semicomputable sets of real and complex numbers. In Constructivity in Computer Science: Summer Symposium, San Antonio, Texas, June 1991, J. Myers, Jr. and M. O'Donnell, Eds. Lecture Notes in Computer Science, vol. 613. Springer-Verlag, Berlin, Germany, 179--198.
34. Tucker, J. and Zucker, J. 1992b. Theory of computation over stream algebras, and its applications. In Mathematical Foundations of Computer Science 1992: 17th International Symposium, Prague, I. Havel and V. Koubek, Eds. Lecture Notes in Computer Science, vol. 629. Springer-Verlag, Berlin, Germany, 62--80.
35. Tucker, J. and Zucker, J. 1994. Computable functions on stream algebras. In Proof and Computation: NATO Advanced Study Institute International Summer School at Marktoberdorf, 1993, H. Schwichtenberg, Ed. Springer-Verlag, Berlin, Germany, 341--382.
36. Tucker, J. and Zucker, J. 1999. Computation by 'while' programs on topological partial algebras. Theoret. Comput. Sci. 219, 379--420.
37. Tucker, J. and Zucker, J. 2000. Computable functions and semicomputable sets on many-sorted algebras. In Handbook of Logic in Computer Science, S. Abramsky, D. Gabbay, and T. Maibaum, Eds. Vol. 5. Oxford University Press, Oxford, U.K., 317--523.
38. Tucker, J. and Zucker, J. 2002a. Abstract computability and algebraic specification. ACM Trans. Computat. Log. 3, 279--333.
39. Tucker, J. and Zucker, J. 2002b. Computable total functions on metric algebras, universal algebraic specifications and dynamical systems. Tech. rep. CAS 02-04-JZ, Department of Computing & Software, McMaster University, Hamilton, Ont., Canada. (Accepted for publication in Journal of Logic and Algebraic Programming.)
40. Weihrauch, K. 2000. Computable Analysis: An Introduction. Springer-Verlag, Berlin, Germany.
41. Wirsing, M. 1991. Algebraic specification. In Handbook of Theoretical Computer Science, Vol. B: Formal Methods and Semantics, J. van Leeuwen, Ed. North Holland, Amsterdam, The Netherlands, 675--788.

Index Terms

• Computing methodologies

  • Symbolic and algebraic manipulation

    • Symbolic and algebraic algorithms

      • Theorem proving algorithms

• Theory of computation

  • Logic

    • Proof theory

  • Models of computation

    • Computability