在計算機科學中，協同歸納是一種定義和證明并發互動對象系統屬性的技術。協同歸納是結構歸納的數學對偶。協同歸納定義的類型被稱為codata，通常是無限的數據結構，如流。作為一種定義或規范，協同歸納描述了一個對象如何被觀察、分解或破壞為更簡單的對象。作為一種證明技術，它可以被用來證明一個方程被這種規范的所有可能的實現所滿足。為了生成和操作編碼數據，人們通常使用corecursive函數，并結合懶惰評估。非正式地，我們不是通過對每個歸納構造函數進行模式匹配來定義一個函數，而是在函數結果上定義每個析構器或觀察者。在編程中，共同邏輯編程（Co-LP）是邏輯編程和共同歸納邏輯編程的自然概括，它反過來又概括了邏輯編程的其他擴展，如無限樹、懶惰謂詞和并發交流謂詞。Co-LP在有理樹、驗證無限屬性、懶惰評價、并發邏輯編程、模型檢查、雙相似性證明等方面有應用。Co-LP的實驗性實現可以從德克薩斯大學達拉斯分校以及Logtalk（例子見）和SWI-Prol中獲得。

在本文中對歸納原則和聯合歸納原則都做了簡明的陳述。雖然本文主要關注的不是歸納法，但一次性考慮它們的一般化形式是很有用的。為了說明這些原則，需要一些初步的資料。當你的所有斷言都被其他斷言所支持時（即沒有非F邏輯的假設），X{displaystyleX}是F-conistent。Knaster-Tarski定理告訴我們，F的最小固定點是F{displaystyleF}的最小固定點(表示為μF{displaystylemuF}的最小固定點（表示μF)是由所有F封閉集的交集給出的，而xxx的固定點(表示為νF{displaystylenuF}）由所有F封閉集的交集給出。)是由所有F封閉集的聯合體給出的。我們現在可以說明歸納和聯合歸納的原則。

歸納法的原則。如果{displaystyleX}是F封閉的。討論如上所述，這些原則有些不透明，但可以有效地用以下方式來思考。

定義一個數據類型集考慮下面的數據類型語法。以及（非同質的）列表。這些類型可以用字母表上的字符串來識別{displaystyletimes}，以及字符串x{displaystyletimes}的連接。.我們現在應該把我們的數據類型集定義為F{displaystyleF}的火點。