Коіндукція

Коіндукція в інформатиці — метод визначення та доведення властивостей систем об'єктів, що паралельно взаємодіють (узагальнено). З математичної точки зору є двоїстою до структурної індукції.

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

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

Кодані

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

Література

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

Посилання

• Coinduction Tatami project (англ.)