Abstract
In the field of algebraic specification, the semantics of an equationally specified datatype is given by the initial algebra of the specifications. We show in this paper that in general the theory of the initial algebra of a given set of equations is II 02 -complete. The impossibility of complete finite axiomatization of equations as well as inequations true in the initial algebra is therefore established. We, further, establish that the decision problem is, in general, II 01 -complete if the equational theory is decidable. We extend the investigation to a certain semantics of parameterized specifications (the so-called free extension functor semantics) that has been proposed in the literature. We present some results characterizing the recursion-theoretic properties of (a) the theory of the free extension algebras of parameter algebras relative to the the theory of the parameter algebras, and (b) the theory of the models of a parameterized specification relative to the theory axiomatized by the specification itself.
This research was supported by U.S. Army Research Office grant DAAL03-89-C-0031PRI.
Preview
Unable to display preview. Download preview PDF.
References
S. Burris and H. P. Sankappanavar. A course in universal algebra. Volume 78 of Graduate Texts in Mathematics, Springer-Verlag, 1981.
M. Davis, Y. Matijasevič, and J. Robinson. Hilbert's tenth problem, diophantine equations: positive aspects of a negative solution. In Proceedings of Symposia in Pure mathematics, Vol. 28, pages 323–378, American Mathematical Society, 1976.
H. Ehrig and B. Mahr. Fundamentals of algebraic specification 1: equations and initial semantics. Springer-Verlag, 1985.
F. Nourani. On induction for programming logic: syntax, semantics and inductive closure. Bulletin of the EATCS, (13):51–64, February 1981.
J. Goguen and J. Meseguer. Initiality, induction, and computability. In Algebraic Methods in Semantics, Cambridge Univ. Press, 1985.
J. A. Goguen, J. W. Thatcher, and E. G. Wagner. An initial algebra approach to the specification, correctness, and implementation of abstract data types. In R.T. Yeh, editor, Current Trends in Programming Methodology, Prentice-Hall, 1978.
J. A. Goguen. How to prove algebraic inductive hypotheses without induction. In Proceedings of the Conference on Automated Deduction, pages 356–373, Springer-Verlag, 1984.
J. V. Guttag, E. Horowitz, and D. R. Musser. Abstract data types and software validation. Communications of the ACM, 21:1048–1064, 1978.
G. Huet and J-M. Hullot. Proofs by induction in equatioanl theories with constructors. Journal of Computer and System Sciences, 25:239–266, 1982.
F. W. Lawvere. Functorial semantics of algebraic theories. In Proc. Nat. Acad. Sci. Vol.50, pages 869–872, 1963.
S. MacLane. Categories for the Working Mathematician. Volume 5 of Graduate Texts in Mathematics, Springer-Verlag, 1988.
D. MacQueen and D. T. Sannella. Completeness of proof systems for equational specifications. IEEE Transactions on Software Engineering, SE-11:454–461, 1985.
H. Rogers. Theory of Recursive Functions and Effective Computability. New York: McGraw-Hill, 1967.
R. Subrahmanyam. Theory of the initial algebra of a set of equations. Technical Report, University of Pennsylvania, Philadelphia, 1990.
H. Zhang, D. Kapur, and M. S. Krishnamoorthy. A mechanizable induction principle for equational specifications. 1988. Manuscript.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Subrahmanyam, R. (1990). Complexity of algebraic specifications. In: Nori, K.V., Veni Madhavan, C.E. (eds) Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1990. Lecture Notes in Computer Science, vol 472. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-53487-3_33
Download citation
DOI: https://doi.org/10.1007/3-540-53487-3_33
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53487-7
Online ISBN: 978-3-540-46313-9
eBook Packages: Springer Book Archive