Учреждение (информатика)

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

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

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

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

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

Пусть обозначать противоположное из категории малых категорий . Учреждение формально состоит из${\ displaystyle Cat ^ {op}}$

• категории из подписей ,${\ displaystyle Sign}$
• функтор дает для каждой подписи , множество предложений , и для каждой подписи морфизма , то предложение перевода на карту , где часто пишутся как ,${\ displaystyle sen: Войти \ to}$ ${\ displaystyle Set}$${\ displaystyle \ Sigma}$ ${\ displaystyle sen (\ Sigma)}$${\ Displaystyle \ sigma: \ Sigma \ to \ Sigma '}$ ${\ Displaystyle сен (\ сигма): сен (\ Sigma) \ к сен (\ Sigma ')}$${\ Displaystyle сен (\ сигма) (\ varphi)}$${\ Displaystyle \ sigma (\ varphi)}$
• функтор даяние, для каждой подписи , категория моделей , и для каждой сигнатуры морфизма , то редукт функтор , где часто записывается как ,${\ displaystyle Mod: Войдите \ to Cat ^ {op}}$${\ displaystyle \ Sigma}$ ${\ Displaystyle Mod (\ Sigma)}$${\ Displaystyle \ sigma: \ Sigma \ to \ Sigma '}$ ${\ Displaystyle Mod (\ sigma): Mod (\ Sigma ') \ to Mod (\ Sigma)}$${\ Displaystyle Mod (\ sigma) (M ')}$${\ displaystyle M '| _ {\ sigma}}$
• отношение удовлетворения для каждого ,${\displaystyle {\models _{\Sigma }}\subseteq |{Mod(\Sigma )|\times sen(\Sigma )}}$${\displaystyle \Sigma \in Sign}$

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

${\displaystyle M'\models _{\Sigma '}\sigma (\varphi )}$ если и только если ${\displaystyle M'|_{\sigma }\models _{\Sigma }\varphi }$

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

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

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

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

• Логика высказываний
• Логика первого порядка
• Логика высшего порядка
• Интуиционистская логика
• Модальная логика
• Временная логика
• Язык веб-онтологий (OWL)
• Общая логика
• Общий язык алгебраической спецификации (CASL)

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

• Абстрактная теория моделей
• Теория институциональной модели
• Универсальная логика

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

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

• Я. А. Гогуэн; Р. М. Берстолл (1984), «Введение в институты», в Э. Кларке; D. Кодзэн (ред.), Логики программ: Труды логик Программирование Workshop 1983 , Lecture Notes в области компьютерных наук, 164 , Springer, Berlin, Германия, стр 221-256,. DOI : 10.1007 / 3-540-12896 -4_366 , ISBN 978-3-540-12896-0. Это была первая публикация по теории институтов и предварительная версия Гогена и Берстолла (1992).
• J. Meseguer (1989), «Общая логика», в H.-D. Эббингаус; Х. Фернандес-Прида; М. Гарридо; Д. Ласкар; М. Родрикес Арталехо (ред.), Logic Colloquium '87: Proceedings of the Colloquium, проведенного в Гранаде, Испания , 129 , Elservier, стр. 274–307
• Я. А. Гогуэн; Г. Роза (2002), "Учреждение морфизмы", формальные аспекты вычислительной техники , 13 (3-5): 274-307, DOI : 10.1007 / s001650200013 , S2CID  5687318
• Д. Саннелла; А. Tarlecki (1988), "Технические характеристики в произвольном учреждении", информация и вычисления , 76 (2-3): 165-210, DOI : 10,1016 / 0890-5401 (88) 90008-9
• Р. Диаконеску (2008), Институционально-независимая теория моделей , Биркхойзер, Базель

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

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