В информатике , коиндукция представляет собой метод для определения и доказательства свойств систем параллельных взаимодействующих объектов .
Коиндукции являются математическим двойственной к структурной индукции . Коиндуктивно определенные типы известны как codata и обычно представляют собой бесконечные структуры данных , такие как потоки .
В качестве определения или спецификации коиндукция описывает, как объект можно «наблюдать», «разбивать» или «разрушать» на более простые объекты. В качестве метода доказательства его можно использовать, чтобы показать, что уравнение удовлетворяется всеми возможными реализациями такой спецификации.
Для генерации кодовых и управления ими обычно используются коркурсивные функции в сочетании с ленивым вычислением . Неформально, вместо того, чтобы определять функцию путем сопоставления с образцом для каждого из индуктивных конструкторов, каждый из «деструкторов» или «наблюдателей» определяет результат функции.
В программировании ко-логическое программирование (co-LP для краткости) «является естественным обобщением логического программирования и совместного логического программирования, которое, в свою очередь, обобщает другие расширения логического программирования, такие как бесконечные деревья, ленивые предикаты и параллельные сообщающиеся предикаты. Co-LP имеет приложения к рациональным деревьям, проверке бесконечных свойств, отложенному вычислению, параллельному логическому программированию, проверке моделей, доказательствам двойственности и т. Д. " [1] Экспериментальные реализации co-LP доступны в Техасском университете в Далласе [2], а также в Logtalk (примеры см. [3] ) и SWI-Prolog .
Смотрите также
Рекомендации
дальнейшее чтение
- Учебники
- Давиде Санджорджи (2012). Введение в бисимуляцию и коиндукцию . Издательство Кембриджского университета.
- Давиде Санджорджи и Ян Руттен (2011). Продвинутые темы бисимуляции и коиндукции . Издательство Кембриджского университета.
- Вступительные тексты
- Эндрю Д. Гордон (1994). «Учебник по коиндукции и функциональному программированию». CiteSeerX 10.1.1.37.3914 . Цитировать журнал требует
|journal=
( помощь ) - математически ориентированное описание - Барт Джейкобс и Ян Руттен (1997). Учебник по (ко) алгебрам и (ко) индукции ( альтернативная ссылка ) - описывает индукцию и коиндукцию одновременно
- Эдуардо Хименес и Пьер Кастеран (2007). "Учебное пособие по [ко-] индуктивным типам в Coq"
- Коиндукция - краткое введение
- История
- Давиде Санджорджи . « Об истоках бисимуляции и коиндукции », Транзакции ACM по языкам и системам программирования, Vol. 31, Nb 4, май 2009 г.
- Разнообразный
- Ко-логическое программирование: расширение логического программирования с помощью коиндукции - описывает парадигму ко-логического программирования.