Hostname: page-component-586b7cd67f-gb8f7 Total loading time: 0 Render date: 2024-11-24T21:41:18.726Z Has data issue: false hasContentIssue false
  • English
  • Français

Interpolation and compactness in categories of pre-institutions

Published online by Cambridge University Press:  04 March 2009

Antonino Salibra  and
Giuseppe Scollo
Antonino Salibra
Affiliation:
University of Venice, Dip. Matematica Applicata e Informatica Via Torino 155, 1–30173 Venezia, Italy Email [email protected]
Giuseppe Scollo
Affiliation:
University of Twente, Fac. Informatica PO Box 211, NL-7500AE Enschede, The Netherlands Email [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

An analysis of relationships between Craig-style interpolation, compactness, and other related model-theoretic properties is carried out in the softer framework of categories of pre-institutions. While the equivalence between sentence interpolation and the Robinson property under compactness and Boolean closure is well known, a similar result under different assumptions (not involving compactness) is newly established for presentation interpolation. The standard concept of naturality of model transformation is enriched by a new property, termed restriction adequacy, which proves useful for the reduction of interpolation along pre-institution transformations. A distinct reduction theorem for the Robinson property is presented as well. A variant of the ultraproduct concept is further introduced, and the related closure property for pre-institutions is shown to be equivalent to compactness

Type
Research Article
Information
Mathematical Structures in Computer Science , Volume 6 , Issue 3 , June 1996 , pp. 261 - 286
Copyright
Copyright © Cambridge University Press 1996

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Andreéka, H. and Nemeti, I. (1981) A general axiomatizability theorem formulated in terms of coneinjective subcategories. In: Csakany, B., Fried, E. and Schmidt, E. T. (eds.) Universal Algebra. Colloquia Mathematics Societatis János Bolyai 29 13–35.Google Scholar
Andréka, H., Németi, I. and Sain, I. (1984) Abstract model theoretic approach to algebraic logic (an overview). Manuscript, Mathematical Institute, Budapest. Revised version available as CCSOM Working Paper92–92 (1992), Amsterdam, The Netherlands.Google Scholar
Andréka, H.Németi, I. and Sain, I. (1994) Applying Algebraic Logic to Logic. In: Nivat, M., Rattray, C. M. I., Rus, T. and Scollo, G. (eds.) Algebraic Methodology and Software Technology (AMAST'93) Workshops in Computing, Springer-Verlag5–26.CrossRefGoogle Scholar
Astesiano, E. and Cerioli, M. (1993) Relationships between logical frameworks. In: Bidoit, M. and Choppy, C. (eds.) Recent Trends in Data Type Specification. Springer-Verlag Lecture Notes in Computer Science 665 126–143.CrossRefGoogle Scholar
Bernot, G. and Bidoit, M. (1992) Proving the correctness of algebraically specified software: Modularity and Observability issues. In: Nivat, M., Rattray, C. M. I., Rus, T. and Scollo, G. (eds.) Algebraic Methodology and Software Technology (AMAST'93) Workshops in Computing, Springer-Verlag 216–239.Google Scholar
Cerioli, M. (1993) Relationships between logical formalisms, Ph.D. Thesis, DISI, University of Genova, Genova, Italy.Google Scholar
Diaconescu, R., Goguen, J. A. and Stefaneas, P. (1993) Logical Support for Modularisation. In: Huet, G. and Plotkin, G. (eds.) Logical Environments, Cambridge University Press 83–130.Google Scholar
Ebbinghaus, H.-D. (1985) Extended logics: the general framework. In: Barwise, J. and Feferman, S. (eds.) Model-Theoretic Logics, Springer-Verlag 25–76.Google Scholar
Ebbinghaus, H.-D., Flum, J. and Thomas, W. (1984) Mathematical Logic, Springer-Verlag.Google Scholar
Ehrig, H., Baldamus, M., Cornelius, F. and Orejas, F. (1992) Theory of Algebraic Module Specification Including Behavioural Semantics and Constraints. In: Nivat, M., Rattray, C. M. I., Rus, T. and Scollo, G. (eds.) Algebraic Methodology and Software Technology (AMAST'93) Workshops in Computing, Springer-Verlag 145–172.Google Scholar
Goguen, J.A. and Burstall, R.M. (1984) Introducing Institutions. In: Clarke, E. and Kozen, D. (eds.) Logics of Programs. Springer-Verlag Lecture Notes in Computer Science 164 221–256.CrossRefGoogle Scholar
Goguen, J. A. and Burstall, R. M. (1986) A Study in the Foundations of Programming Methodology: Specifications, Institutions, Charters and Parchments. In: Pitt, D., Abramsky, S., Poigne, A. and Rydeheard, D. (eds.) Category Theory and Computer Programming. Springer-Verlag Lecture Notes in Computer Science 240 313–333.CrossRefGoogle Scholar
Goguen, J.A. and Burstall, R.M. (1992) Institutions: Abstract model theory for specification and programming. J. Assoc. Comput. Mack 39 95–146.CrossRefGoogle Scholar
Goguen, J.A. and Meseguer, J. (1989) Order-Sorted Algebra I: Equational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations, Report SRI-CSL-89–10, SRI International, Computer Science Laboratory, Menlo Park, California.Google Scholar
Kreowski, H.-J. and Mossakowski, T. (1993) Equivalence and Difference of Institutions: Simulating Horn Clause Logic with Based Algebras. Draft, FB Informatik, Universität Bremen.Google Scholar
Los, J. (1954) Quelques remarques, théorèmes, et problèmes sur les classes définissables d'algèbres. In: Mathematical Interpretation of Formal Systems, Studies in Logic and the Foundations of Mathematics, Symposium, Amsterdam98–113.Google Scholar
Mac Lane, S. (1971) Categories for the Working Mathematician, Graduate Texts in Mathematics 5Springer-Verlag.CrossRefGoogle Scholar
Makowski, J.-A. (1985) Compactness, Embeddings and Definability. In: Barwise, J. and Feferman, S. (eds.) Model-Theoretic Logics, Springer-Verlag 645–716.Google Scholar
Makowski, J.-A. and Mundici, D. (1985) Abstract Equivalence Relations. In: Barwise, J. and Feferman, S. (eds.) Model-Theoretic Logics, Springer-Verlag 717–746.Google Scholar
Manca, V., Salibra, A. and Scollo, G. (1990) Equational type logic. Theoretical Computer Science 77 131–159.CrossRefGoogle Scholar
Manca, V., Salibra, A. and Scollo, G. (1992) On the expressiveness of equational type logic. In: Rattray, C. M. I., AND Clark, R. G. (eds.) The Unified Computation Laboratory: Modelling, Specifications and Tools, Oxford University Press 85–100.Google Scholar
Meseguer, J. (1989) General Logics. In: Ebbinghaus, H.-D.et al. (eds.) Logic Colloquium '87, North-Holland275–329.Google Scholar
Mossakowski, T. (1994) Parameterized Recursion Theory – A Tool for the Systematic Classification of Specification Methods. In: Nivat, M., Rattray, C. M. I., Rus, T. and Scollo, G. (eds.) Algebraic Methodology and Software Technology (AMAST'93) Workshops in Computing, Springer-Verlag 137–144.CrossRefGoogle Scholar
Nivela, M.P. and Orejas, F. (1988) Initial Behaviour Semantics for Algebraic Specifications. In: Sannella, D. T. and Tarlecki, A. (eds.) Recent Trends in Data Type Specification. Springer-Verlag Lecture Notes in Computer Science 332 184–207.CrossRefGoogle Scholar
Nivela, M. P., Orejas, F. and Ehrig, H. (1989) Semantical Constructions for Categories of Behavioural Specifications. In: Ehrig, H., Herrlich, H., Kreowski, H.-J. and PreuB, G. (eds.) Categorical Methods in Computer Science - with Aspects from Topology. Springer-Verlag Lecture Notes in Computer Science 393 220–245.Google Scholar
Rodenburg, P. H. (1991) A simple algebraic proof of the equational interpolation theorem. Algebra Universalis 28 48–51.CrossRefGoogle Scholar
Rodenburg, P. H. and Van Glabbeek, R. J. (1988) An interpolation theorem in equational logic. CWI Report CS-R8838, Amsterdam, The Netherlands.Google Scholar
Salibra, A. and Scollo, G. (1993) A soft stairway to institutions. In: Bidoit, M. and Choppy, C. (eds.) Recent Trends in Data Type Specification. Springer-Verlag Lecture Notes in Computer Science 665 310–329.CrossRefGoogle Scholar
Salibra, A. and Scollo, G. (1993) Compactness and Löwenheim-Skolem properties in categories of pre-institutions. In: Rauszer, C. (ed.) Algebraic Methods in Logic and in Computer Science, Banach Center Publ. 28, Inst. Math. Polish Acad. Sci., Warszawa. Poland67–94.Google Scholar
Sannella, D. T. and Tarlecki, A. (1988) Specifications in an arbitrary institution. Inform, and Comput. 76 165–210.CrossRefGoogle Scholar
Tarlecki, A. (1985) On the existence of free models in abstract algebraic institutions. Theoretical Computer Science 37 269–304.CrossRefGoogle Scholar
Tarlecki, A. (1986) Bits and pieces of the theory of institutions. In: Pitt, D., Abramsky, S., Poigne, A. and Rydeheard, D. (eds.) Category Theory and Computer Programming. Springer-Verlag Lecture Notes in Computer Science 240 334–360.CrossRefGoogle Scholar