2 に答える
完全な言語をチューリングするための設定された理論モデルはありません。言語が強力に正規化されている場合は、何かに「解釈」するためのトータル関数が存在します。非チューリング完全言語で理論的セマンティクスを設定した場合としない場合があります。チューリングが完全であっても、チューリングが完全でなくても、言語は完全なセマンティック マッピング機能を備えた非セットの理論的セマンティクスを持つことができます。
それはここでは問題ではないと思います。
誘導と共誘導の定義には違いがあります。このセットを理論的に調べることができます。
整数のリストの帰納的な定義は次のとおりです。
セット
[Z]は、空のリストが にあり、とのペアの任意のリストがあるような最小のセットです。SSlsSnZ(n,ls)S
これは、「ステップインデックス」の方法で提示することも[Z](0) = {[]}でき[Z](n) = {(n,ls) | n \in Z, ls \in [Z](n-1)}ます。これにより、定義できます[Z] = \Union_{i \in N}([Z](n)（自然数を信じるなら！）
一方、Haskell の「リスト」は、帰納的に定義される「連帰ストリーム」とより密接に関連しています。
セット
[Z](帰納的) は、forall in 、またはwith inおよびinのような最大のセットです。SxSx = []x = (n,ls)nZlsS
つまり、帰納的定義は逆です。帰納的定義は、いくつかの要素を含む最小のセットを定義しますが、総帰納的定義は、すべての要素が特定の形式をとる最大のセットを定義します。
すべての帰納的リストは有限の長さを持つが、一部の帰納的リストは無限に長いことを示すのは簡単です。あなたの例には、誘導が必要です。
より一般的には、帰納的定義は「ファンクターの最小固定点」と見なすことができ、共誘導定義は「ファンクターの最大固定点」と見なすことができます。ファンクターの「最小不動点」は単にその「初期代数」であり、「最大不動点」はその「最終合体」です。これをセマンティック ツールとして使用すると、セットのカテゴリ以外のカテゴリで物事を定義することが容易になります。
Haskell は、これらのファンクターを記述するための優れた言語を提供していることがわかります。
data ListGenerator a r = Cons a r | Nil
instance Functor (ListGenerator a) where
fmap f (Cons a x) = Cons a (f x)
fmap _ Nil = Nil
Haskell はこれらのファンクターを記述するための優れた言語を提供しますが、その関数空間は CBN であり、言語は完全ではないため、希望する最小不動点の種類を定義する方法はありません :(最大不動点
data GF f = GF (f (GF f))
または非再帰的存在量化
data GF f = forall r. GF r (r -> (f r))
厳密な言語または全体的な言語で作業している場合、最小の修正点は普遍的に定量化されたものになります
data LF f = LF (forall r. (f r -> r) -> r)
編集：「最小」/「最大」の区別は正しいものではないかもしれませんが、「最小」は一連の理論的概念であるためです。の定義LFは基本的に に同型でGFあり、「最小不動点」の定言形式である「自由初期代数」です。
に関して
「1とタプル」の有限数ではなく、非生産的な⊥ではないことをどのように納得させることができますか?
この投稿のような構造を信じない限り、できません。もしそうなら、あなたの定義は私を行き詰まらせます!. もしあなたが「onesはペアからなる誘導ストリームである」と言うなら(1,ones)、私は信じなければなりません! 私は定義によるものでonesはないことを知っています。したがって、帰納法により、任意の値に対して1 があり、次に底_|_があるということはあり得ないことを示すことができます。私はあなたの主張を否定しようとすることができます. nn
共導的構造に対する証明手法の詳細については (Philip JF の非常に素晴らしい回答を拡張)、Hinze と James の「Proving the Unique Fixed-Point Principle Correct」を参照してください: http://www.cs.ox.ac .uk/people/daniel.james/unique/unique-tech.pdf