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

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

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

Коданные

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

Литература

• Bart Jacobs (1996). "Coalgebraic Specifications and Models of deterministic Hybrid Systems". Algebraic Methods and Software Technology, number 1101 in Lect . Springer. pp. 520--535. Jacobs96coalgebraicspecifications. {{ cite conference }} : |access-date= требует |url= ( справка )
• Turner D. // Journal of Universal Computer Science. — Т. 10 , № 7 . — С. 751—768 .
• Richard B. Kieburtz. (англ.) . Дата обращения: 15 декабря 2013. Архивировано из 11 сентября 2006 года.

Ссылки

• Tatami project (англ.)