Коиндукция

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

Коиндукция в информатике — метод для определения и доказательства свойств систем параллельно взаимодействующих объектов (обобщённо). С математической точки зрения является дуальной к структурной индукции.

В качестве определения или спецификации коиндукция описывает метод, при помощи которого объект может быть разбит на более простые объекты. Как техника математического доказательства коиндукция может быть использована для того, чтобы показать у некоторого коданного выполнимость всех заявленных спецификацией требований.

В программировании кологическая парадигма является естественным расширением логического программирования и коиндукции, которое также обобщает другие расширения логического программирования, такие как бесконечные деревья, ленивые предикаты и параллельно взаимодействующие предикаты. Кологическое программирование имеет применение в областях рациональных деревьев, доказательства бесконечных свойств, ленивых вычислений, параллельного логического вывода, проверки моделей и т. д.

Коданные[править | править вики-текст]

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

Литература[править | править вики-текст]

  • Bart Jacobs (1996). "Coalgebraic Specifications and Models of deterministic Hybrid Systems". Algebraic Methods and Software Technology, number 1101 in Lect: 520--535, Springer. Jacobs96coalgebraicspecifications. Проверено 2013-12-06. 
  • Turner D. Total Functional Programming // Journal of Universal Computer Science. — Т. 10, № 7. — С. 751—768.
  • Richard B. Kieburtz. Codata and Comonads in Haskell (англ.). Проверено 15 декабря 2013.

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