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.
@InProceedings{tarlecki:LIPIcs.CALCO.2023.8, author = {Tarlecki, Andrzej}, title = {{Interpolation Is (Not Always) Easy to Spoil}}, booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)}, pages = {8:1--8:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-287-7}, ISSN = {1868-8969}, year = {2023}, volume = {270}, editor = {Baldan, Paolo and de Paiva, Valeria}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.8}, URN = {urn:nbn:de:0030-drops-188059}, doi = {10.4230/LIPIcs.CALCO.2023.8}, annote = {Keywords: interpolation, institutions, institutional abstract model theory, specification theory} }
Feedback for Dagstuhl Publishing