Институт (информатика)

Понятие института было создано Джозефом Гогеном и Родом Берстоллом в конце 1970-х годов, чтобы справиться с «демографическим взрывом среди логических систем, используемых в информатике ». Это понятие пытается «формализовать неформальную» концепцию логической системы. ^[1]

Использование институтов позволяет разрабатывать концепции языков спецификаций (таких как структурирование спецификаций, параметризация, реализация, уточнение и развитие), исчисления доказательств и даже инструменты способом, полностью независимым от базовой логической системы. Существуют также морфизмы , позволяющие связывать и переводить логические системы. Важными применениями этого являются повторное использование логической структуры (также называемое заимствованием), а также гетерогенная спецификация и комбинация логик.

Распространение теории институциональных моделей обобщило различные понятия и результаты теории моделей , а сами институты повлияли на развитие универсальной логики . ^[2]^[3]

Определение [ править ]

Теория институтов ничего не предполагает о природе логической системы. То есть модели и предложения могут быть произвольными объектами; единственное предположение состоит в том, что между моделями и предложениями существует отношение удовлетворения , показывающее, соответствует ли предложение модели или нет. Удовлетворение вдохновлено определением истины Тарского , но на самом деле может быть любым бинарным отношением.Ключевой особенностью институтов является то, что модели, предложения и их удовлетворение всегда считаются живущими в некотором словаре или контексте (называемом сигнатурой ), который определяет (нелогические) символы, которые могут использоваться в предложениях и которые необходимо интерпретировать. в моделях. Более того, морфизмы сигнатур позволяют расширять сигнатуры, изменять обозначения и т. д. В отношении сигнатур и морфизмов сигнатур ничего не предполагается, за исключением того, что морфизмы сигнатур могут быть составлены; это означает наличие категория сигнатур и морфизмов. Наконец, предполагается, что морфизмы сигнатур приводят к переводам предложений и моделей таким образом, чтобы удовлетворение сохранялось. В то время как предложения переводятся вместе с сигнатурными морфизмами (представьте себе, что символы заменяются вдоль морфизма), модели переводятся (или, лучше сказать, сокращаются). против сигнатурных морфизмов. Например, в случае расширения сигнатуры модель (более крупной) целевой сигнатуры может быть сведена к модели (меньшей) исходной сигнатуры, просто забывая о некоторых компонентах модели.

Позволять $\mathbf {Cat} ^{\mathrm {op} }$ Обозначают противоположные категории малых категорий . Формально учреждение состоит из

категория $\mathbf {Sign}$ подписей ,
функтор ${\mathit {Sen}}\colon \mathbf {Sign} \to$ $\mathbf {Set}$ давая за каждую подпись $\Sigma$ , набор предложений ${\mathit {Sen}}(\Sigma )$ и для каждого сигнатурного морфизма $\sigma \colon \Sigma \to \Sigma '$ , карта перевода предложения ${\mathit {Sen}}(\sigma )\colon {\mathit {Sen}}(\Sigma )\to {\mathit {Sen}}(\Sigma ')$ , где часто ${\mathit {Sen}}(\sigma )(\varphi )$ написано как $\sigma (\varphi )$ ,
функтор $\mathbf {Mod} \colon \mathbf {Sign} \to \mathbf {Cat} ^{\mathrm {op} }$ давая за каждую подпись $\Sigma$ , категория моделей $\mathbf {Mod} (\Sigma )$ и для каждого сигнатурного морфизма $\sigma \colon \Sigma \to \Sigma '$ , функтор редукции $\mathbf {Mod} (\sigma )\colon \mathbf {Mod} (\Sigma ')\to \mathbf {Mod} (\Sigma )$ , где часто $\mathbf {Mod} (\sigma )(M')$ написано как $M'|_{\sigma }$ ,
удовлетворения отношение ${\models _{\Sigma }}\subseteq |{\mathbf {Mod} (\Sigma )|\times {\mathit {Sen}}(\Sigma )}$ для каждого $\Sigma \in \mathbf {Sign}$ ,

такой, что для каждого $\sigma \colon \Sigma \to \Sigma '$ в $\mathbf {Sign}$ , имеет место следующее условие выполнения :

M'\models _{\Sigma '}\sigma (\varphi )\quad {\text{if and only if}}\quad M'|_{\sigma }\models _{\Sigma }\varphi

для каждого $M'\in \mathbf {Mod} (\Sigma ')$ и $\varphi \in {\mathit {Sen}}(\Sigma )$ .

Условие удовлетворения выражает, что истина инвариантна при изменении обозначений. (а также при расширении или факторизации контекста).

Строго говоря, модельный функтор заканчивается в «категории» всех больших категорий.

Примеры учреждений [ править ]

См. также [ править ]

Ссылки [ править ]

^ Ж. А. Гоген; Р. М. Берстолл (1992), «Институты: абстрактная теория моделей для спецификации и программирования», Журнал ACM , 39 (1): 95–146, doi : 10.1145/147508.147524 , S2CID 16856895
^ Разван Диаконеску (2012), «Три десятилетия теории институтов» , в Жан-Иве Безио (редактор), Universal Logic: An Anthology , Springer, стр. 309–322.
^ Т. Моссаковски; Ж. А. Гоген; Р. Дьяконеску; А. Тарлецкий (2007), «Что такое логика?: В память о Жозефе Гогене», в Жан-Иве Безио (ред.), Logica Universalis: На пути к общей теории логики (2-е изд.), Биркхойзер, Базель, стр. . 113–133, номер телефона : 10.1007/978-3-7643-8354-1_7.

Дальнейшее чтение [ править ]

Ж. А. Гоген; Р. М. Берстолл (1984), «Введение учреждений», Э. Кларк; Д. Козен (ред.), Логика программ: материалы семинара по логике программирования, 1983 г. , Конспекты лекций по информатике, том. 164, Springer, Берлин, Германия, стр. 221–256, doi : 10.1007/3-540-12896-4_366 , ISBN. 978-3-540-12896-0 . Это была первая публикация по теории институтов и предварительная версия Гогена и Берстолла (1992).
Ж. Мезегер (1989), «Общая логика», в книге Х.-Д. Эббингауз; Х. Фернандес-Прида; М. Гарридо; Д. Ласкар; М. Родригес Арталехо (ред.), Коллоквиум по логике '87: Материалы коллоквиума, состоявшегося в Гранаде, Испания , том. 129, Эльсервье, стр. 274–307.
Ж. А. Гоген; Г. Росу (2002), «Институциональные морфизмы», Формальные аспекты вычислений , 13 (3–5): 274–307, doi : 10.1007/s001650200013 , S2CID 5687318
Д. Саннелла; А. Тарлецкий (1988), «Спецификации произвольного учреждения», Information and Computation , 76 (2–3): 165–210, doi : 10.1016/0890-5401(88)90008-9
Р. Диаконеску (2008), Институционально-независимая модельная теория , Биркхойзер, Базель

Внешние ссылки [ править ]

Рэзван Дьяконеску, «Теория институтов» , Интернет-энциклопедия философии , получено 31 января 2021 г.
Джозеф Гоген (2006 г.), Институты , Калифорнийский университет, Сан-Диего , данные получены 31 января 2021 г.
Формализм, логика, институт – связь, перевод и структурирование . Включает большую библиографию.
Рэзван Дьяконеску, Избранные публикации , Институт математики Симиона Стоилова Румынской академии , получено 31 января 2021 г. Содержит недавние работы по теории институциональных моделей.

[1] Ж. А. Гоген; Р. М. Берстолл (1992), «Институты: абстрактная теория моделей для спецификации и программирования», Журнал ACM , 39 (1): 95–146, doi : 10.1145/147508.147524 , S2CID 16856895

[2] Разван Диаконеску (2012), «Три десятилетия теории институтов» , в Жан-Иве Безио (редактор), Universal Logic: An Anthology , Springer, стр. 309–322.

[3] Т. Моссаковски; Ж. А. Гоген; Р. Дьяконеску; А. Тарлецкий (2007), «Что такое логика?: В память о Жозефе Гогене», в Жан-Иве Безио (ред.), Logica Universalis: На пути к общей теории логики (2-е изд.), Биркхойзер, Базель, стр. . 113–133, номер телефона : 10.1007/978-3-7643-8354-1_7.

[1]

[2]

[3]