Document Open Access Logo

Interpolation Is (Not Always) Easy to Spoil

Author Andrzej Tarlecki

PDF
Thumbnail PDF

File

LIPIcs.CALCO.2023.8.pdf
  • Filesize: 0.8 MB
  • 19 pages

Document Identifiers

Author Details

Andrzej Tarlecki
  • Institute of Informatics, University of Warsaw, Poland

Acknowledgements

Thanks to the anonymous reviewers for a number of useful comments.

Cite As Get BibTex

Andrzej Tarlecki. Interpolation Is (Not Always) Easy to Spoil. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.CALCO.2023.8

Abstract

We study a version of the Craig interpolation theorem as formulated in the framework of the theory of institutions. This formulation proved crucial in the development of a number of key results concerning foundations of software specification and formal development. We investigate preservation of interpolation under extensions of institutions by new models and sentences. We point out that some interpolation properties remain stable under such extensions, even if quite arbitrary new models or sentences are permitted. We give complete characterisations of such situations for institution extensions by new models, by new sentences, as well as by new models and sentences, respectively.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Theory of computation → Logic and verification
Keywords
  • interpolation
  • institutions
  • institutional abstract model theory
  • specification theory

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Egidio Astesiano, Michel Bidoit, Hélène Kirchner, Bernd Krieg-Brückner, Peter D. Mosses, Donald Sannella, and Andrzej Tarlecki. CASL: the Common Algebraic Specification Language. Theoretical Computer Science, 286(2):153-196, 2002. URL: https://doi.org/10.1016/S0304-3975(01)00368-1.
  2. Jon Barwise. Axioms for abstract model theory. Annals of Mathematical Logic, 7:221-265, 1974. URL: https://doi.org/10.1016/0003-4843(74)90016-3.
  3. Jan A. Bergstra, Jan Heering, and Paul Klint. Module algebra. Journal of the Association for Computing Machinery, 37(2):335-372, 1990. URL: https://doi.org/10.1145/77600.77621.
  4. Evert W. Beth. On Padoa’s method in the theory of definition. Indagationes Mathematicae (Proceedings), 56:330-339, 1953. URL: https://doi.org/10.1016/S1385-7258(53)50042-3.
  5. Tomasz Borzyszkowski. Logical systems for structured specifications. Theoretical Computer Science, 286(2):197-245, 2002. URL: https://doi.org/10.1016/S0304-3975(01)00317-6.
  6. Tomasz Borzyszkowski. Generalized interpolation in first-order logic. Fundamenta Informaticae, 66(3):199-219, 2005. URL: http://content.iospress.com/articles/fundamenta-informaticae/fi66-3-01.
  7. Carlos Caleiro, Paula Gouveia, and Jaime Ramos. Completeness results for fibred parchments: Beyond the propositional base. In Martin Wirsing, Dirk Pattinson, and Rolf Hennicker, editors, Recent Trends in Algebraic Development Techniques. Selected Papers from the 16th International Workshop on Algebraic Development Techniques, volume 2755 of Lecture Notes in Computer Science, pages 185-200. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-40020-2_10.
  8. Carlos Caleiro, Paulo Mateus, Jaime Ramos, and Amílcar Sernadas. Combining logics: Parchments revisited. In Maura Cerioli and Gianna Reggio, editors, Recent Trends in Algebraic Development Techniques. Selected Papers from the 15th Workshop on Algebraic Development Techniques Joint with the CoFI WG Meeting, volume 2267 of Lecture Notes in Computer Science, pages 48-70. Springer, 2001. URL: https://doi.org/10.1007/3-540-45645-7_3.
  9. Carlos Caleiro, Amílcar Sernadas, and Cristina Sernadas. Fibring logics: Past, present and future. In Sergei N. Artëmov, Howard Barringer, Artur S. d'Avila Garcez, Luís C. Lamb, and John Woods, editors, We Will Show Them! Essays in Honour of Dov Gabbay, Volume One, pages 363-388. College Publications, 2005. Google Scholar
  10. María Victoria Cengarle. Formal Specifications with Higher-Order Parameterization. PhD thesis, Ludwig-Maximilians-Universität München, Institut für Informatik, 1994. Google Scholar
  11. Chen-Chung Chang and H. Jerome Keisler. Model Theory. North-Holland, third edition, 1990. Google Scholar
  12. William Craig. Linear reasoning. A new form of the Herbrand-Gentzen theorem. The Journal of Symbolic Logic, 22(3):250-268, 1957. URL: https://doi.org/10.2307/2963593.
  13. Rǎzvan Diaconescu. Institution-Independent Model Theory. Birkhäuser, 2008. URL: https://doi.org/10.1007/978-3-7643-8708-2.
  14. Răzvan Diaconescu. An institution-independent proof of Craig interpolation theorem. Studia Logica, 77(1):59-79, 2004. URL: https://doi.org/10.1023/B:STUD.0000034185.62660.d6.
  15. Răzvan Diaconescu. Interpolation for predefined types. Mathematical Structures in Computer Science, 22(1):1-24, 2012. URL: https://doi.org/10.1017/S0960129511000430.
  16. Răzvan Diaconescu. Three decades of institution theory. In Jean-Yves Béziau, editor, Universal Logic: An Anthology, pages 309-322. Birkhäuser, 2012. Google Scholar
  17. Răzvan Diaconescu. Generalised graded interpolation. International Journal of Approximate Reasoning, 152:236-261, 2023. URL: https://doi.org/10.1016/j.ijar.2022.10.018.
  18. Răzvan Diaconescu. Borrowing interpolation. J. Logic and Computation, 22(3):561-586, 2011. URL: https://doi.org/10.1093/logcom/exr007.
  19. Theodosis Dimitrakos and Thomas S.E. Maibaum. On a generalised modularization theorem. Information Processing Letters, 74(1-2):65-71, 2000. URL: https://doi.org/10.1016/S0020-0190(00)00037-5.
  20. Hartmut Ehrig, Hans-Jörg Kreowski, James W. Thatcher, Eric G. Wagner, and Jesse B. Wright. Parameter passing in algebraic specification languages. Theoretical Computer Science, 28(1-2):45-81, 1984. URL: https://doi.org/10.1016/0304-3975(83)90065-8.
  21. Dov M. Gabbay and Larisa Maksimova. Interpolation and Definability: Modal and Intuitionistic Logics. Oxford University Press, 2005. URL: https://doi.org/10.1093/acprof:oso/9780198511748.001.0001.
  22. Daniel Găină. Interpolation in logics with constructors. Theoretical Computer Science, 474:46-59, 2013. URL: https://doi.org/10.1016/j.tcs.2012.12.002.
  23. Daniel Găină. Downward Löwenheim–Skolem theorem and interpolation in logics with constructors. Journal of Logic and Computation, 27(6):1717-1752, 2015. URL: https://doi.org/10.1093/logcom/exv018.
  24. Daniel Găină and Andrei Popescu. An institution-independent proof of the Robinson consistency theorem. Studia Logica, 85:41-73, 2007. URL: https://doi.org/10.1007/s11225-007-9022-4.
  25. Joseph A. Goguen and Rodney M. Burstall. Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery, 39(1):95-146, 1992. URL: https://doi.org/10.1145/147508.147524.
  26. Joseph A. Goguen and Grigore Roşu. Institution morphisms. Formal Aspects of Computing, 13(3-5):274-307, 2002. URL: https://doi.org/10.1007/s001650200013.
  27. Thomas S.E. Maibaum, Martin R. Sadler, and Paolo A.S. Veloso. Logical specification and implementation. In Mathai Joseph and Rudrapatna Shyamasundar, editors, Foundations of Software Technology and Theoretical Computer Science, pages 13-30. Springer, 1984. URL: https://doi.org/10.1007/3-540-13883-8_62.
  28. Till Mossakowski, Wiesław Pawłowski, Donald Sannella, and Andrzej Tarlecki. Parchments for CafeOBJ logics. In Shusaku Iida, José Meseguer, and Kazuhiro Ogata, editors, Specification, Algebra, and Software - Essays Dedicated to Kokichi Futatsugi, volume 8373 of Lecture Notes in Computer Science, pages 66-91. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54624-2_4.
  29. Till Mossakowski, Andrzej Tarlecki, and Wiesław Pawłowski. Combining and representing logical systems using model-theoretic parchments. In Francesco Parisi-Presicce, editor, Recent Trends in Data Type Specification. Selected Papers from the 12th International Workshop on Specification of Abstract Data Types, volume 1376 of Lecture Notes in Computer Science, pages 349-364. Springer, 1998. URL: https://doi.org/10.1007/3-540-64299-4_44.
  30. Andrei Popescu, Traian Florin Şerbănuţă, and Grigore Roşu. A semantic approach to interpolation. Theoretical Computer Science, 410(12-13):1109-1128, 2009. URL: https://doi.org/10.1016/j.tcs.2008.09.038.
  31. Gerard R. Renardel de Lavalette. Interpolation in computing science: The semantics of modularization. Synthese, 164(3):437-450, 2008. URL: https://doi.org/10.1007/s11229-008-9358-y.
  32. Abraham Robinson. A result on consistency and its application to the theory of definition. Indagationes Mathematicae (Proceedings), 59:47-58, 1956. URL: https://doi.org/10.1016/S1385-7258(56)50008-X.
  33. Pieter Hendrik Rodenburg. A simple algebraic proof of the equational interpolation theorem. Algebra Universalis, 28:48-51, 1991. URL: https://doi.org/10.1007/BF01190411.
  34. Grigore Roşu and Joseph A. Goguen. On equational Craig interpolation. Journal of Universal Computer Science, 6(1):194-200, 2000. URL: https://doi.org/10.3217/jucs-006-01-0194.
  35. Donald Sannella and Andrzej Tarlecki. Foundations of Algebraic Specification and Formal Software Development. Monographs in Theoretical Computer Science. An EATCS Series. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-17336-3.
  36. Donald Sannella and Andrzej Tarlecki. Property-oriented semantics of structured specifications. Mathematical Structures in Computer Science, 24(2):e240205, 2014. URL: https://doi.org/10.1017/S0960129513000212.
  37. Andrzej Tarlecki. Bits and pieces of the theory of institutions. In David H. Pitt, Samson Abramsky, Axel Poigné, and David E. Rydeheard, editors, Proceedings of the Tutorial and Workshop on Category Theory and Computer Programming, volume 240 of Lecture Notes in Computer Science, pages 334-360. Springer, 1986. URL: https://doi.org/10.1007/3-540-17162-2_132.
  38. Andrzej Tarlecki. Towards heterogeneous specifications. In Dov Gabbay and Maarten de Rijke, editors, Frontiers of Combining Systems 2, volume 7 of Studies in Logic and Computation, pages 337-360. Research Studies Press, 2000. Google Scholar
  39. Andrzej Tarlecki. Some nuances of many-sorted universal algebra: A review. Bulletin of the European Association for Theoretical Computer Science, 104:89-111, 2011. URL: http://eatcs.org/beatcs/index.php/beatcs/article/view/121.
  40. Jouko Väänänen. The Craig interpolation theorem in abstract model theory. Synthese, 164:401-420, 2008. URL: https://doi.org/10.1007/s11229-008-9357-z.
  41. Paulo A.S. Veloso. On pushout consistency, modularity and interpolation for logical specifications. Information Processing Letters, 60(2):59-66, 1996. URL: https://doi.org/10.1016/S0020-0190(96)00146-9.
  42. Paulo A.S. Veloso and Thomas S.E. Maibaum. On the modularization theorem for logical specifications. Information Processing Letters, 53(5):287-293, 1995. URL: https://doi.org/10.1016/0020-0190(94)00203-B.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact