Коіндукція в інформатиці — метод визначення та доведення властивостей систем об'єктів, що паралельно взаємодіють (узагальнено). З математичної точки зору є двоїстою до структурної індукції.
Як визначення чи специфікацію коіндукція визначає метод, за допомогою якого об'єкт можна розбитий простіші об'єкти. Як техніку математичного доведення коіндукцію можна використати для того, щоб показати в деякого коданого виконуваність усіх заявлених специфікацією вимог.
У програмуванні кологічна парадигма є природним розширенням логічного програмування та коіндукції, яке також узагальнює інші розширення логічного програмування, такі як нескінченні дерева, ледачі предикати та паралельно взаємодійні предикати. Кологічне програмування має застосування у галузях раціональних дерев, доведення нескінченних властивостей, ледачих обчислень, паралельного логічного виведення, перевірки моделей тощо.
Кодані Кодані — сутність, двоїста до даних. Кодані є потенційно нескінченними контейнерами, які можуть містити як елементи даних, так і елементи коданих. Для оперування коданими використовують механізм корекурсії, для доведення властивостей коданих використовують коіндукцію (у прямій аналогії з даними, для яких використовують рекурсію та індукцію відповідно).
Література
Посилання Coinduction Tatami project