共誘導

コンピュータサイエンスにおいて、コインダクションは、同時に相互作用するオブジェクトのシステムの特性を定義および証明するための手法です。

共帰納法は構造帰納法の数学的 双対です。^[要出典]共帰納的に定義されたデータ型はコデータと呼ばれ、通常はストリームなどの無限データ構造です。

定義または仕様として、コインダクションは、オブジェクトをより単純なオブジェクトに「観察」、「分解」、または「破壊」する方法を説明します。証明手法としては、そのような仕様の すべての可能な実装によって方程式が満たされることを示すために使用できます。

codata を生成および操作するには、通常、遅延評価と組み合わせてコアカーシブ関数を使用します。非公式には、各帰納的コンストラクターでパターン マッチングによって関数を定義するのではなく、関数の結果に対して各「デストラクタ」または「オブザーバー」を定義します。

プログラミングにおいて、共論理プログラミング（略してco-LP）は「論理プログラミングと共帰性論理プログラミングの自然な一般化であり、無限木、遅延述語、並行通信述語などの論理プログラミングの他の拡張を一般化します。Co-LPは、有理木、無限特性の検証、遅延評価、並行論理プログラミング、モデル検査、双相似性証明などに応用できます。」^[1] co-LPの実験的な実装は、テキサス大学ダラス校^[2]と言語Logtalk（例については ^[3]を参照）およびSWI-Prologで利用できます。

^[4]では、帰納法の原理と共帰納法の原理の両方について簡潔に述べられている。この記事は帰納法を主に扱っているわけではないが、それらのやや一般化された形式を一度に検討することは有益である。原理を述べるためには、いくつかの準備が必要である。

を集合とし、を単調関数とします。つまり、 ${\displaystyle U}$${\displaystyle F}$ ${\displaystyle 2^{U}\rightarrow 2^{U}}$

${\displaystyle X\subseteq Y\Rightarrow F(X)\subseteq F(Y)}$

特に記載がない限り、モノトーンとみなされます。 ${\displaystyle F}$

XがF閉である場合${\displaystyle F(X)\subseteq X}$

XがF-無矛盾であるのは、${\displaystyle X\subseteq F(X)}$

Xが不動点であるのは、${\displaystyle X=F(X)}$

これらの用語は、次のように直感的に理解できます。 がアサーションのセットであり、が の結果を生み出す演算であるとします。 は、すでにアサートした以上の結論を導くことができない場合にF 閉じており、すべてのアサーションが他のアサーションによってサポートされている場合 (つまり、「非F論理的仮定」が存在しない) はF 整合しています。${\displaystyle X}$${\displaystyle F(X)}$${\displaystyle X}$${\displaystyle X}$${\displaystyle X}$

クナスター・タルスキーの定理によれば、（ と表記）の最小の不動点はすべてのF 閉集合の共通部分で与えられ、（ と表記）の最大の不動点はすべてのF 無矛盾集合の和集合で与えられる。これで、帰納法と共帰納法の原理を述べることができる。 ${\displaystyle F}$${\displaystyle \mu F}$${\displaystyle \nu F}$

帰納法の原理:がF閉である場合、${\displaystyle X}$${\displaystyle \mu F\subseteq X}$

共帰納法の原理： がF無矛盾であれば、${\displaystyle X}$${\displaystyle X\subseteq \nu F}$

原理は、述べられているように、いくぶん不明瞭ですが、次のように考えると便利です。 の特性を証明したいとします。帰納法の原理により、特性が成り立つF 閉集合を示すだけで十分です。 逆に、 であることを証明したいとします。 その場合、のメンバーであることがわかっている F 整合集合を示すだけで十分です。${\displaystyle \mu F}$${\displaystyle X}$${\displaystyle x\in \nu F}$${\displaystyle x}$

次のデータ型の文法を考えてみましょう。

${\displaystyle T=\bot \;|\;\top \;|\;T\times T}$

つまり、型の集合には、「ボトム型」、 「トップ型」、および（非同次）リストが含まれます。 これらの型は、アルファベット 上の文字列で識別できます。 は上のすべての（無限の可能性がある）文字列を表します。 関数 を考えます。 ${\displaystyle \bot}$${\displaystyle \top}$${\displaystyle \Sigma =\{\bot ,\top ,\times \}}$${\displaystyle \Sigma ^{\leq \omega }}$${\displaystyle \Sigma }$${\displaystyle F:2^{\Sigma ^{\leq \omega }}\rightarrow 2^{\Sigma ^{\leq \omega }}}$

${\displaystyle F(X)=\{\bot ,\top \}\cup \{x\times y:x,y\in X\}}$

この文脈では、 は「文字列、シンボル、文字列の連結」を意味します。ここで、データ型のセットを の固定点として定義する必要がありますが、最小の固定点を取るか最大の固定点を取るかが重要です。 ${\displaystyle x\times y}$${\displaystyle x}$${\displaystyle \times }$${\displaystyle y}$${\displaystyle F}$

データ型のセットをとするとします。帰納法の原理を使用して、次の主張を証明できます。 ${\displaystyle \mu F}$

のすべてのデータ型は有限である${\displaystyle \mu F}$

この結論に至るには、 上のすべての有限文字列の集合を考えます。 は明らかに無限文字列を生成できないため、この集合はF 閉集合であることがわかり、結論は次式に従います。 ${\displaystyle \Sigma }$${\displaystyle F}$

ここで、データ型のセットとしてを取ると仮定します。共帰納法の原理を使用して、次の主張を証明します。 ${\displaystyle \nu F}$

タイプ${\displaystyle \bot \times \bot \times \cdots \in \nu F}$

ここで は、すべて からなる無限リストを表します。共帰納法の原理を使用するには、次の集合を考えます。 ${\displaystyle \bot \times \bot \times \cdots }$${\displaystyle \bot}$

${\displaystyle \{\bot \times \bot \times \cdots \}}$

この集合はF-無矛盾であることが判明しており、したがって である。これは、 ${\displaystyle \bot \times \bot \times \cdots \in \nu F}$

${\displaystyle \bot \times \bot \times \cdots =(\bot \times \bot \times \cdots )\times (\bot \times \bot \times \cdots )}$

この正式な正当性は技術的なものであり、文字列をシーケンス、つまり からの関数として解釈することに依存します。直感的には、この議論は という議論に似ています(繰り返し小数 を参照)。 ${\displaystyle \mathbb {N} \rightarrow \Sigma }$${\displaystyle 0.{\bar {0}}1=0}$

ストリームの次の定義を考えてみましょう: ^[5]

データストリームa = S a (ストリームa )       

-- ストリームの「デストラクタ」
head ( S a astream ) = a tail ( S a astream ) = astream     
     

これは根拠の薄い定義のように思えますが、それでもプログラミングには役立ち、推論することができます。いずれにせよ、ストリームは要素の無限リストであり、そこから最初の要素を観察したり、要素を前に配置して別のストリームを取得したりすることができます。

出典: ^[6]

集合のカテゴリにおける自己関数 を考えてみましょう。 ${\displaystyle F}$

${\displaystyle F(x)=A\times x}$

${\displaystyle F(f)=\langle \mathrm {id} _{A},f\rangle }$

最終的な F 余代数 には、次の射が関連付けられています。 ${\displaystyle \nu F}$

${\displaystyle \mathrm {out} :\nu F\rightarrow F(\nu F)=A\times \nu F}$

これにより、関連する射を伴う別の余代数が誘導される。は最終的であるため、一意の射が存在する。 ${\displaystyle F(\nu F)}$${\displaystyle F(\mathrm {out} )}$${\displaystyle \nu F}$

${\displaystyle {\overline {F(\mathrm {out} )}}:F(\nu F)\rightarrow \nu F}$

そのような

${\displaystyle \mathrm {out} \circ {\overline {F(\mathrm {out} )}}=F\left({\overline {F(\mathrm {out} )}}\right)\circ F(\mathrm {out} )=F\left({\overline {F(\mathrm {out} )}}\circ \mathrm {out} \right)}$

この合成により、別のF余代数準同型が誘導されます。は最終的であるため、この準同型は一意であり、したがって です。全体として、次のようになります。 ${\displaystyle {\overline {F(\mathrm {out} )}}\circ \mathrm {out} }$${\displaystyle \nu F\rightarrow \nu F}$${\displaystyle \nu F}$${\displaystyle \mathrm {id} _{\nu F}}$

${\displaystyle {\overline {F(\mathrm {out} )}}\circ \mathrm {out} =\mathrm {id} _{\nu F}}$

${\displaystyle \mathrm {out} \circ {\overline {F(\mathrm {out} )}}=F\left({\overline {F(\mathrm {out} )}}\right)\circ \mathrm {out} )=\mathrm {id} _{F(\nu F)}}$

これは同型 を証明しており、カテゴリカルな用語では がの不動点であることを示しており、表記法を正当化します。 ${\displaystyle \nu F\simeq F(\nu F)}$${\displaystyle \nu F}$${\displaystyle F}$

私たちはそれを示します

ストリームA

は関数 の最終的な余代数です。次の実装を検討してください。 ${\displaystyle F(x)=A\times x}$

out astream = ( head astream 、tail astream ) out' ( a 、astream ) = S a astream      
      

これらは相互に逆であることが簡単にわかり、同型性が証明されます。詳細については参考文献を参照してください。

ここでは、帰納法の原理が数学的帰納法を包含する仕組みを説明します。 を自然数のある特性とします。数学的帰納法の定義を次のようにします。 ${\displaystyle P}$

${\displaystyle 0\in P\land (n\in P\Rightarrow n+1\in P)\Rightarrow P=\mathbb {N} }$

ここで関数を考えてみましょう: ${\displaystyle F:2^{\mathbb {N} }\rightarrow 2^{\mathbb {N} }}$

${\displaystyle F(X)=\{0\}\cup \{x+1:x\in X\}}$

であることは容易に分かるはずです。したがって、帰納法の原理により、の何らかの性質を証明したい場合、がF 閉じていることを示すだけで十分です。詳しくは、次のことを要求します。 ${\displaystyle \mu F=\mathbb {N} }$${\displaystyle P}$${\displaystyle \mathbb {N} }$${\displaystyle P}$

${\displaystyle F(P)\subseteq P}$

つまり、

${\displaystyle \{0\}\cup \{x+1:x\in P\}\subseteq P}$

これはまさに述べられている数学的帰納法です。

• F-余代数
• 共起
• バイシミュレーション
• アナモルフィズム
• トータル関数型プログラミング

教科書

• Davide Sangiorgi (2012)。『双模倣と共帰納法入門』ケンブリッジ大学出版局。
• Davide Sangiorgiと Jan Rutten (2011)。双模倣と共帰納法の高度なトピック。ケンブリッジ大学出版局。

入門テキスト

• Andrew D. Gordon (1994)。「共帰納法と関数型プログラミングに関するチュートリアル」。1994 年。78 ～ 95 ページ。CiteSeerX 10.1.1.37.3914。 — 数学的な説明
• バート・ジェイコブスとヤン・ルッテン（1997年）。（共）代数と（共）帰納法に関するチュートリアル（代替リンク）—帰納法と共帰納法を同時に説明している。
• エドゥアルド・ヒメネスとピエール・カステラン（2007）。 「Coq の [Co-] 帰納型に関するチュートリアル」
• Coduction — 簡単な紹介

歴史

• Davide Sangiorgi . 「双模倣と共帰納法の起源について」、ACM Transactions on Programming Languages and Systems、第31巻、第4号、2009年5月。

その他

• 共論理プログラミング：共帰納法による論理プログラミングの拡張 — 共論理プログラミングのパラダイムについて説明します