共誘導

させて${\displaystyle U}$セットであり、${\displaystyle F}$単調関数である${\displaystyle 2^{U}\rightarrow 2^{U}}$つまり：

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

特に明記されていない限り、${\displaystyle F}$単調であると想定されます。

• Xは、​${\displaystyle F(X)\subseteq X}$
• XがF-一貫性を持つのは、${\displaystyle X\subseteq F(X)}$
• Xが固定点であるのは、${\displaystyle X=F(X)}$

これらの用語は、次のように直感的に理解できます。${\displaystyle X}$は一連の主張であり、${\displaystyle F(X)}$は、${\displaystyle X}$。 それから${\displaystyle X}$すでに主張された以上の結論を導き出せない場合、F-閉合となる。${\displaystyle X}$すべての主張が他の主張によって裏付けられている場合（つまり、「非F論理的な仮定」がない場合）、F-一貫性があると言えます。

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

• 帰納法の原理：もし${\displaystyle X}$F-閉の場合、${\displaystyle \mu F\subseteq X}$
• 共帰納法の原理：もし${\displaystyle X}$F-一貫性がある場合、${\displaystyle X\subseteq \nu F}$

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

$${\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}$有限である

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

ここで、${\displaystyle \nu F}$データ型の集合として、共帰納法の原理を用いて以下の主張を証明したいと思います。

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

ここ${\displaystyle \bot \times \bot \times \cdots }$無限文字列を表す${\displaystyle (\bot ,\times ,\bot ,\times ,\ldots )}$帰納法の原理を用いるために、次の集合を考えてみましょう。

$${\displaystyle S=\{\bot ,\;\bot \times \bot \times \cdots \}}$$

このセットはF-一貫性があります。まず、${\displaystyle \bot \in \{\bot ,\top \}\subseteq F(S)}$第二に、${\displaystyle \bot \in S}$そして${\displaystyle \bot \times \bot \times \cdots \in S}$、 我々は持っています${\displaystyle \bot \times (\bot \times \bot \times \cdots )\in F(S)}$文字列をシーケンスとして解釈する（関数は${\displaystyle \mathbb {N} \rightarrow \Sigma }$）有限接頭辞を前に付ける${\displaystyle \bot \times }$無限弦へ${\displaystyle \bot \times \bot \times \cdots }$収量${\displaystyle \bot \times \bot \times \cdots }$それ自体、${\displaystyle \bot \times \bot \times \cdots \in F(S)}$。 したがって${\displaystyle S\subseteq F(S)}$、そして共帰納法の原理により、${\displaystyle \bot \times \bot \times \cdots \in \nu F}$。

注。 型を文字列として表現することは、${\displaystyle \Sigma }$基となるツリー構造に忠実ではありません。有限文字列など${\displaystyle \bot \times \top \times \bot }$括弧なしでは曖昧であり、任意の無限文字列に対して${\displaystyle s}$連結${\displaystyle s\times t=s}$すべての人々のために${\displaystyle t}$、したがって、異なるツリーを識別できます。これは、 F-一貫性による共帰納の原理を示すだけの上記の議論には影響しませんが、コンストラクタ構造を保持する必要がある設定では重要になります。標準的な構造的処理では、同型性によって型が表現されます。${\displaystyle T\cong 1+1+(T\times T)}$詳細はF-共代数を参照してください。

Haskellにおけるストリームの次の定義を考えてみましょう: ^{[ 5 ]}

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

最初の行は、ストリームは要素とそれに続くストリームで構成されると述べています（Sは要素のコンストラクタであり、は要素の任意の型を表します）。基本ケースがないため、これは根拠が不十分な定義のように思えますが、それでもプログラミングでは有用であり、推論することができます。いずれにせよ、ストリームは要素の無限リストであり、最初の要素を観察したり、要素の前に要素を置いて別のストリームを取得したりできます。

エンドファンクターを考える${\displaystyle F}$集合のカテゴリーにおいて：

$${\displaystyle {\begin{aligned}F(x)&=A\times x\\F(f)&=\langle \mathrm {id} _{A},f\rangle \end{aligned}}}$$

最終的な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)}$$

構成${\displaystyle {\overline {F(\mathrm {out} )}}\circ \mathrm {out} }$別のF-共代数準同型を誘導する${\displaystyle \nu F\rightarrow \nu F}$。 以来${\displaystyle \nu F}$が最終であるため、この準同型は一意であり、したがって${\displaystyle \mathrm {id} _{\nu F}}$合計すると以下のようになります。

$${\displaystyle {\begin{aligned}{\overline {F(\mathrm {out} )}}\circ \mathrm {out} &=\mathrm {id} _{\nu F}\\[0.5ex]\mathrm {out} \circ {\overline {F(\mathrm {out} )}}=F{\bigl (}{\overline {F(\mathrm {out} )}}\circ \mathrm {out} {\bigr )}&=\mathrm {id} _{F(\nu F)}\end{aligned}}}$$

これは同型性を証明するものである${\displaystyle \nu F\simeq F(\nu F)}$これは、明確に言えば、${\displaystyle \nu F}$は固定点である${\displaystyle F}$そして、その表記を正当化する。^{[ 6 ]}

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 \mathbb {N} \subseteq P}$$

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

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

容易に理解できるはずだ${\displaystyle \mu F=\mathbb {N} }$したがって、帰納法の原理により、ある性質を証明したい場合${\displaystyle P}$の${\displaystyle \mathbb {N} }$示すだけで十分である${\displaystyle P}$F閉集合である。具体的には、以下の条件を満たす必要がある。

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

つまり、

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

これはまさに、述べられている通りの数学的帰納法である。