 | Эта статья поднимает множество проблем. Пожалуйста, помогите улучшить его или обсудите эти проблемы на странице обсуждения . ( Узнайте, как и когда удалить эти сообщения-шаблоны ) ( Узнайте, как и когда удалить этот шаблон сообщения )
|
В информатике , коиндукция представляет собой метод для определения и доказательства свойств систем параллельных взаимодействующих объектов .
Коиндукции являются математическим двойственной к структурной индукции . Коиндуктивно определенные типы известны как codata и обычно представляют собой бесконечные структуры данных , такие как потоки .
В качестве определения или спецификации коиндукция описывает, как объект можно «наблюдать», «разбивать» или «разрушать» на более простые объекты. В качестве метода доказательства его можно использовать, чтобы показать, что уравнение удовлетворяется всеми возможными реализациями такой спецификации.
Для генерации кодовых и управления ими обычно используются коркурсивные функции в сочетании с ленивым вычислением . Неформально, вместо того, чтобы определять функцию путем сопоставления с образцом для каждого из индуктивных конструкторов, каждый из «деструкторов» или «наблюдателей» определяет результат функции.
В программировании ко-логическое программирование (co-LP для краткости) «является естественным обобщением логического программирования и совместного логического программирования, которое, в свою очередь, обобщает другие расширения логического программирования, такие как бесконечные деревья, ленивые предикаты и параллельные сообщающиеся предикаты. Co-LP имеет приложения к рациональным деревьям, проверке бесконечных свойств, отложенному вычислению, параллельному логическому программированию, проверке моделей, доказательствам двойственности и т. Д. " [1] Экспериментальные реализации co-LP доступны в Техасском университете в Далласе [2], а также в Logtalk (примеры см. [3] ) и SWI-Prolog .
См. Также [ править ]
Ссылки [ править ]
- ^ http://lambda-the-ultimate.org/node/2513
- ^ http://www.utdallas.edu/~gupta/
- ^ https://github.com/LogtalkDotOrg/logtalk3/tree/master/examples/coinduction
Дальнейшее чтение [ править ]
- Учебники
- Давиде Санджорджи (2012). Введение в бисимуляцию и коиндукцию . Издательство Кембриджского университета.
- Давиде Санджорджи и Ян Руттен (2011). Продвинутые темы бисимуляции и коиндукции . Издательство Кембриджского университета.
- Вступительные тексты
- Эндрю Д. Гордон (1994). «Учебник по коиндукции и функциональному программированию». CiteSeerX 10.1.1.37.3914 . Цитировать журнал требует
|journal=( помощь ) - математически ориентированное описание - Барт Джейкобс и Ян Руттен (1997). Учебник по (ко) алгебрам и (ко) индукции ( альтернативная ссылка ) - описывает индукцию и коиндукцию одновременно
- Эдуардо Хименес и Пьер Кастеран (2007). "Учебное пособие по [ко-] индуктивным типам в Coq"
- Коиндукция - краткое введение
- История
- Давиде Санджорджи . « Об истоках бисимуляции и коиндукции », Транзакции ACM по языкам и системам программирования, Vol. 31, Nb 4, май 2009 г.
- Разное
- Ко-логическое программирование: расширение логического программирования с помощью коиндукции - описывает парадигму ко-логического программирования.
