haskell - Haskell の整数の非整数居住者

Question

Haskell で次のように定義されたペアノ自然数は、data Peano = Zero | Succ Peano非常に奇妙な獣です。単純な自然数と底値に加えて、inf = Succ infそれらの中に「無限の整数」があります。

このタイプの他の住民はいPeanoますか？この無限の数に名前はありますか?

Answer 1

それらは奇妙ではありません。単純に共導的な自然体です。⊥ の問題はさておき、ここで自然数型を定義することができZeroますSucc。帰納的な定義は、明確に定義された終わり、つまり、任意の数がZeroコンストラクターから始まることを想定します。帰納的定義は、任意の自然数が与えられた場合、それは になるか、Zeroまたは外側Succを取り除いて別の自然数を得ることができると言っているだけです。

一見微妙な違いに見えますが、複導の定義には無限の一連のSuccコンストラクターが含まれており、これは実際には無限の真の表現です。帰納的定義は再帰が明確に定義された基本ケースに到達することを保証するものであるのに対し、共導的定義は明確に定義された次のステップが常に利用可能であることを保証するものであるため、これは意味があります。

Haskell では、データ コンストラクタが怠惰であるため、複帰的な解釈は便利であり、ある意味で必須です。

したがって、ダニエル・フィッシャーが言ったように、この無限数は実際には無限大であり、どの無限大かを指定する必要がある場合は ω です。それは、より一般的に遭遇する無限リストによく似た、単なる誘導無限です。

教会のエンコーディングを介して自然数を考える場合、有限数は「この関数を N 回反復する」ことを意味します。ω は「この関数を無期限に反復する」ことを意味します。

Answer 2

などがあります。ただしSucc _|_、Succ (Succ _|_)「下位値」にそれらを含めた可能性があります。inf = Succ infは通常infinityor omega(自然数の序数として) と呼ばれます。