有限集合 \(A\) 上のリストというものは次のように、 帰納的に定義される.
次のようにも書ける: \[List = nil + A \times List\]
この構成は、ただひとつの定数 \(nil\) と、 ただひとつの構成子 \(::\) によって、 ただひと通りに定まる. リストの \(length\) 、 \(concat\) といった関数は、 この構成に沿って定義できる.
みたいに. これの上のいくつかの命題も、構成に沿って証明される.
これらは、 帰納法と言われる. さて、 双対として、余帰納法がある. 帰納法は大変馴染み深いのに対して、余帰納法は馴染みがないし、綺麗な形式化もない. 帰納法においては、基底があってそこからスタートするのに対して、 余帰納法では基底がなく、無限しかない.
余帰納法が登場する例として、
\(A\) の上の無限ストリーム (有限を許さない) \(X\) とは、次のような 自己関手 \(F : A^\omega \rightarrow A^\omega\) の 終余代数 (final coalgebra) である. \[F(X) = A \times X\]
一方で、 有限はまたは無限の列 \(X\) は、 \[F(X) = 1 + A \times X\] という 自己関手 \(F: A^\infty \rightarrow A^\infty\) の終余代数である.
\(A^\omega\) 上の半順序 \(\preceq\) を定める. ストリームとは \(A^\omega\) の要素、
\(A^\omega\) 上の 二項関係 \(\preceq_{lex}\) を、 次を満たす関係\(R\) の内で最大のものだとする.
これが半順序であるのはいいとして、 次のように定義することもできる.
\[T : (A^\omega , A^\omega) \rightarrow (A^\omega , A^\omega)\] \[T(R) = \{ (s,t) : hd(s) \leq hd(t) \land hd(s) = hd(t) \Rightarrow tl(s) ~R~ tl(t) \}\]
これを用いて、 \(T\) の最大不動点が \(\leq_{lex}\) である.