First and Second Order Recursion on Abstract Data Types

• Autorzy: Xu J. , Zucker J.
• Języki publikacji: EN

Abstrakty

EN

This paper compares two scheme-based models of computation on abstract many-sorted algebras A: Feferman's system of ``abstract computational procedures" based on a least fixed point operator, and Tucker and Zucker's system based on primitive recursion on the naturals together with a least number operator. We prove a conjecture of Feferman that (assuming A contains sorts for natural numbers and arrays of data) the two systems are equivalent. The main step in the proof is showing the equivalence of both systems to a system of computation by an imperative programming language with recursive calls. The result provides a confirmation for a Generalized Church-Turing Thesis for computation on abstract data types.

Słowa kluczowe

EN

model of computation; many-sorted algebras; recursive schems; recursive procedures; fixed point; computation on abstract data types; abstract computability

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2005
• Tom: Vol. 67, nr 4
• Strony: 377--419
• Opis fizyczny: Bibliogr. 23 poz.

Twórcy

autor

Xu J.

• Department of Computing and Software McMaster University 1280 Main Street West, Hamilton, Ontario, Canada L8S 4L7

autor

Zucker J.

• Department of Computing and Software McMaster University 1280 Main Street West, Hamilton, Ontario, Canada L8S 4L7

Bibliografia

• [1] de Bakker, J.: Mathematical Theory of Program Correctness, Prentice-Hall International, 1980.
• [2] Brattka, V.: Recursive characterisation of computable real-valued functions and relations, Theoretical Computer Science, 162, 1996, 45–77.
• [3] Feferman, S.: Inductive schemata and recursively continuous functionals, in: Logic Colloquium ’76 (R. O. Gandy,M. Hyland, Eds.), North-Holland, Amsterdam, 1977, 373–392.
• [4] Feferman, S.: A new approach to abstract data types, I: Informal development, Mathematical Structures in Computer Science, 2, 1992, 193–229.
• [5] Feferman, S.: A new approach to abstract data types, II: Computability on ADTs as ordinary computation, in: Computer Science Logic, Springer-Verlag, 1992, 79–95.
• [6] Feferman, S.: Computation on abstract data types. The extensional approach, with an application to streams, Annals of Pure and Applied Logic, 81, 1996, 75–113.
• [7] Hinman, P.: Recursion on abstract structures, in: Handbook of Computability Theory (E. Griffor, Ed.), North-Holland, Amsterdam, 1999, 317–359.
• [8] Hobley, K., Thompson, B., Tucker, J.: Specification and verification of synchronous concurrent algorithms: a case study of a convoluted algorithm, in: The Fusion of Hardware Design and Verification (Proceedings of IFIPWorking Group 10.2Working Conference) (G.Milne, Ed.), North-Holland, Amsterdam, 1988, 347–374.
• [9] Kleene, S. C.: Introduction to Metamathematics, North-Holland, Amsterdam, 1952.
• [10] Meinke, K.: Universal algebra in higher types, Theoretical Computer Science, 100, 1992, 385–417.
• [11] Meinke, K., Tucker, J.: Universal algebra, in: Handbook of Logic in Computer Science, vol. 1, Oxford University Press, 1992.
• [12] Moldestad, J., Stoltenberg-Hansen, V., Tucker, J. V.: Finite algorithmic procedures and inductive definibility, Mathematica Scandinavica, 46, 1980, 62–76.
• [13] Moore, C.: Recursion theory on reals and continuous time computation, Theoretical Computer Science, 162, 1996, 23–44.
• [14] Moschovakis, Y. N.: Abstract recursion as a foundation for the theory of recursive algorithms, in: Computation and Proof Theory, Springer-Verlag, 1984, 289–364.
• [15] Moschovakis, Y. N.: The formal language of recursion, Joutnal of Symbolic Logic, 54, 1989, 1216–1252.
• [16] Mycka, J., Costa, J.: Real recursive functions and their hierarchy, Journal of Complexity, 2005, To appear.
• [17] Stoy, J. E.: Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, The MIT Press, 1977.
• [18] Tucker, J., Zucker, J.: Program Correctness over Abstract Data Types, with Error-State Semantics, North-Holland, 1988.
• [19] Tucker, J., Zucker, J.: Computable functions on stream algebras, in: NATO Advanced Study Institute, International Summer School at Marktoberdorf, 1993, on Proof and Computation (H. Schwichtenberg, Ed.), Springer-Verlag, 1994, 341–382.
• [20] Tucker, J., Zucker, J.: Computable Functions and Semicomputable Sets on Many-sorted Algebras, in: Handbook of Logic in Computer Science (S. Abramsky, D. M. Gabbay, T. S. E. Maibaum, Eds.), vol. 5, Oxford University Press, 2000, 317–523.
• [21] Tucker, J., Zucker, J.: Abstract Computability and Algebraic Specification, ACM Transactions on Computational Logic, 3, 2002, 279–333.
• [22] Winskel, G.: The Formal Semantics of Programming Languages: An Introduction, The MIT Press, 1993.
• [23] Xu, J.: Models of computation on abstract data types based on recursive schemes, Master Thesis, Department of Computing and Software, McMaster University, Hamilton, Ontario, Canada, August 2003.