Коіндукція в інформатиці — метод визначення та доведення властивостей систем об'єктів, що паралельно взаємодіють (узагальнено). З математичної точки зору є двоїстою до структурної індукції.
Як визначення чи специфікацію коіндукція визначає метод, за допомогою якого об'єкт можна розбитий простіші об'єкти. Як техніку математичного доведення коіндукцію можна використати для того, щоб показати в деякого коданого виконуваність усіх заявлених специфікацією вимог.
У програмуванні кологічна парадигма є природним розширенням логічного програмування та коіндукції, яке також узагальнює інші розширення логічного програмування, такі як нескінченні дерева, ледачі предикати та паралельно взаємодійні предикати. Кологічне програмування має застосування у галузях раціональних дерев, доведення нескінченних властивостей, ледачих обчислень, паралельного логічного виведення, перевірки моделей тощо.
Кодані ред.
Кодані — сутність, двоїста до даних. Кодані є потенційно нескінченними контейнерами, які можуть містити як елементи даних, так і елементи коданих. Для оперування коданими використовують механізм корекурсії, для доведення властивостей коданих використовують коіндукцію (у прямій аналогії з даними, для яких використовують рекурсію та індукцію відповідно).
Література ред.
- Bart Jacobs (1996). Coalgebraic Specifications and Models of deterministic Hybrid Systems. Algebraic Methods and Software Technology, number 1101 in Lect. Springer. с. 520––535. Jacobs96coalgebraicspecifications.
{{cite conference}}:|accessdate=вимагає|url=(довідка) - Turner D. Total Functional Programming // Journal of Universal Computer Science. — Т. 10, № 7. — С. 751—768.
- Richard B. Kieburtz. (англ.). Архів оригіналу за 11 вересня 2006. Процитовано 15 грудня 2013.
Посилання ред.
- Coinduction Tatami project (англ.)
В іншому мовному розділі є повніша стаття Coinduction(англ.). Ви можете допомогти, розширивши поточну статтю за допомогою перекладу з англійської.
|