×

A unifying theorem for algebraic semantics and dynamic logics. (English) Zbl 0616.03016

Various logics have been proposed and studied for expressing and proving program properties. This paper considers the problem whether the class of models of a logic is first-order definable, yielding a general tool to prove that it is not first-order axiomatizable if it is indeed not. The authors show, by using the technical tool of ultraproducts, that a class of structures which is first-order axiomatizable is bounded in the sense that all iterations stop after a finite number of steps. They apply this idea to continuous algebras, dynamic algebras and general computational models of programs. They deduce as easy corollaries of the main theorem the results of A. J. Kfoury and D. M. Park [Inf. Control 29, 243-251 (1975; Zbl 0329.68015)] and B. Courcelle and I. Guessarian [J. Comput. Syst. Sci. 17, 388-413 (1978; Zbl 0392.68009)] and others.
Reviewer: H.Nishimura

MSC:

03B70 Logic in computer science
68Q65 Abstract data types; algebraic specification
68N01 General topics in the theory of software
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] ADI, Initial algebra semantics and continuous algebras, J. Assoc. Comput. Mach., 24, 68-95 (1977), (1977) · Zbl 0359.68018
[2] Andréka, H.; Németi, I., Generalization of variety and quasi-variety concepts to partial algebras through category theory (1976), report · Zbl 0518.08007
[3] Andréka, H.; Németi, I.; Sain, I., A complete logic for reasoning about programs via nonstandard model theory, Theoret. Comput. Sci., 17, 259-278 (1982) · Zbl 0475.68010
[4] Birkhoff, G., On the structure of abstract algebras, (Proc. Cambridge Philos. Soc., 31 (1935)), 433-454 · JFM 61.1026.07
[5] Burstall, R.; Goguen, J., Institution: An Abstract Model Theory for Program Specification (1982), SRI Report
[6] Chang, C. C.; Keisler, H. J., (Model Theory (1973), North-Holland: North-Holland Amsterdam) · Zbl 0276.02032
[7] Courcelle, B.; Guessarian, I., On some classes of interpretations, J. Comput. System Sci., 17, 388-413 (1978) · Zbl 0392.68009
[8] Ehrig, H.; Mahr, B., (Fundamentals of Algebraic Specification (1985), Springer-Verlag: Springer-Verlag Berlin) · Zbl 0557.68013
[9] Grätzer, G., (Universal Algebra (1979), Springer-Verlag: Springer-Verlag Berlin)
[10] Guessarian, I., Algebraic Semantics, (Lecture Notes in Comput. Sci., Vol. 99 (1981), Springer-Verlag: Springer-Verlag Berlin) · Zbl 0602.68017
[11] Henkin, L.; Monk, J.; Tarski, A., (Cylindric Algebras (1985), North-Holland: North-Holland Amsterdam), Part II · Zbl 0214.01302
[12] Henkin, L.; Monk, D.; Tarski, A.; Andréka, H.; Néméti, I., Cylindric Set Algebras, (Lecture Notes in Math., Vol. 883 (1981), Springer-Verlag: Springer-Verlag Berlin) · Zbl 0497.03025
[13] Jónsson, B., The theory of binary relations, (Proceedings, Séminaire de Mathématiques supérieures de l’Université de Montréal (1984)) · Zbl 0111.03803
[14] Kfoury, D. J.; Park, D. M., On the termination of program schemas, Inform. and Control, 29, 243-251 (1975) · Zbl 0329.68015
[15] Kozen, D., On induction vs. \(^∗\)-continuity, (Logics of Programs Proceedings. Logics of Programs Proceedings, New York, 1981. Logics of Programs Proceedings. Logics of Programs Proceedings, New York, 1981, Lecture Notes in Computer Science, Vol. 131 (1982), Springer-Verlag: Springer-Verlag New York/Berlin), 167-176
[16] Németi, I., Dynamic algebras of programs FCT 81, (Lecture Notes in Comput. Sci., Vol. 117 (1981), Springer-Verlag: Springer-Verlag Berlin), 281-290
[17] Németi, I., Every free algebra in the variety generated by separable dynamic algebras is separable and representable, Theoret. Comput. Sci., 17, 343-347 (1982) · Zbl 0491.08012
[18] Németi, I., Nonstandard dynamic logic, (Logics of Programs Proceedings. Logics of Programs Proceedings, New York 1981. Logics of Programs Proceedings. Logics of Programs Proceedings, New York 1981, Lecture Notes in Computer Science, Vol. 131 (1982), Springer-Verlag: Springer-Verlag New York/Berlin), 311-348 · Zbl 0493.68032
[19] Németi, I.; Sain, I., Cone-implicational subcategories and some Birkhoff-type theorems, (Universal Algebra. Universal Algebra, Colloq. Math. Soc. J. Bolyai, Vol. 29 (1982), North-Holland: North-Holland Amsterdam), 535-578 · Zbl 0495.18001
[20] Nivat, M., On the interpretation of recursive polyadic program schemes, (15th Sympos. Mathematica. 15th Sympos. Mathematica, Rome (1975)), 255-281
[21] Plotkin, G., A power domain construction, SIAM J. Comput., 5, 452-487 (1976) · Zbl 0355.68015
[22] Pratt, V. R., Dynamic logic, (Logic, Methodology and Philosophy of Science VI Proceedings. Logic, Methodology and Philosophy of Science VI Proceedings, Hannover, 1979. Logic, Methodology and Philosophy of Science VI Proceedings. Logic, Methodology and Philosophy of Science VI Proceedings, Hannover, 1979, Studies in Logic and the Foundations of Math., Vol. 104 (1982), North-Holland: North-Holland Amsterdam), 251-261 · Zbl 0433.68031
[23] Reiterman, J.; Trnkova, V., From dynamic algebras to test algebras, ((1984), Charles University: Charles University Prague), preprint · Zbl 0551.68030
[24] Sain, I., On the applicability of a category-theoretic notion of ultraproducts, Mat. lapok, 31, No. 1.3 (1983), [Hungarian]
[25] Sain, I., and Hien, H.Studia Sci. Math. Hungar.; Sain, I., and Hien, H.Studia Sci. Math. Hungar.
[26] Scott, D., Data types as lattices, SIAM J. Comput., 5, 522-587 (1976) · Zbl 0337.02018
[27] Smyth, M., Powerdomains, J. Comput. System Sci., 6, 23-36 (1978) · Zbl 0408.68017
[28] Ng, K. C.; Tarski, A., Relation algebras with transitive closure, Notices Amer. Math. Soc., 24, A-29 (1977)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.