Koinduktion i datalogi er en metode til at bestemme og bevise egenskaberne af systemer af parallelt interagerende objekter (generelt). Fra et matematisk synspunkt er det dobbelt til strukturel induktion .
Som en definition eller specifikation beskriver coinduction en metode, hvorved et objekt kan opdeles i enklere objekter. Som en teknik til matematisk bevis kan coinduktion bruges til at vise, at alle kravene i specifikationen er tilfredsstillende for et eller andet kodenavn .
I programmering er det økologiske paradigme en naturlig forlængelse af logisk programmering og koinduktion, der også generaliserer andre udvidelser af logisk programmering, såsom uendelige træer , dovne prædikater og parallelt interagerende prædikater. Kologisk programmering har applikationer inden for områderne rationelle træer, beviser uendelige egenskaber, doven evaluering, parallel inferens, modelkontrol osv.
Codata er en enhed, der er dobbelt til data . Kodata er potentielt uendelige beholdere , der kan indeholde både data og kodedataelementer. Corecursion-mekanisme bruges til at operere med codata , coinduction bruges til at bevise egenskaberne af codata (i direkte analogi med data, hvortil henholdsvis rekursion og induktion bruges ).