- Коиндукция
-
Коиндукция — в информатике техника для определения и доказательства свойств систем параллельно взаимодействующих объектов (обобщённо). С математической точки зрения является дуальной к индукции (структурной индукции).
В качестве определения или спецификации коиндукция описывает метод, при помощи которого объект может быть разбит на более простые объекты. Как техника математического доказательства коиндукция может быть использована для того, чтобы показать у некоторого коданного выполнимость всех заявленных спецификацией требований.
В программировании кологическая парадигма является естественным расширением логического программирования и коиндукции, которое также обобщает другие расширения логического программирования, такие как бесконечные деревья, ленивые предикаты и параллельно взаимодействующие предикаты. Кологическое программирование имеет применение в областях рациональных деревьев, доказательства бесконечных свойств, ленивых вычислений, параллельного логического вывода, проверки моделей и т. д.
Содержание
Коданные
Коданные — сущность, дуальная к данным. Коданные являются потенциально бесконечными контейнерами, которые могут содержать в себе как элементы данных, так и элементы коданных. Для оперирования коданными используется механизм корекурсии, для доказательства свойств коданных используется коиндукция (в прямой аналогии с данными, для которых используются рекурсия и индукция соответственно).
См. также
Литература
- Bart Jacobs. Coalgebraic specications and models of deterministic hybrid systems. In AMAST’96, volume 1101 of Lecture Notes in Computer Science, pages 520—535. Springer Verlag, July 1996
- D.Turner. Total Functional Programming // Journal of Universal Computer Science 10 (7): 751—768
- http://www-internal.cse.ogi.edu/PacSoft/publications/phaseiiiq10papers/codata.pdf
Ссылки
Категории:- Логика
- Информатика
Wikimedia Foundation. 2010.