問題タブ [coinduction]

Isabelle の無限ストリーム データ型を扱う場合、この明らかに正しい補題が必要ですが、それを証明する方法がわかりません (私はまだ帰納法に精通していないため)。それを証明するにはどうすればいいですか？

これは、「遅延モダリティを使用して固定点演算子から (無限) ツリーを計算する」のバリエーションです。

設定。ルートからのパスによってツリー内の任意の他のノードを参照する機能が追加されたバイナリ ツリーの言語を研究します。

パスは何らかのルートのコンテキストで定義され、パスに False/True が表示されると、左/右の子を連続してたどって見つかったサブツリーを識別します。たとえば、パスはツリーで[False, True]識別されます。SLeaf 2SNode (SNode (SLeaf 1) (SLeaf 2)) (SLeaf 3)

このようなツリーは、たとえば、任意のフロー グラフを識別するために使用できます (既約グラフを含み、固定小数点演算子を使用することはできません)。

この記述によって導かれる無限木を考えることができます。

follow以下は、ツリーのあるパスでサブツリーを見つける補助関数を利用した、一方から他方への変換関数です。

残念ながら、この関数は生産的ではありません: で無限ループしflatten (SPath [])ます。

問題。ここで、遅延モダリティ ( 「遅延モダリティを使用して固定点演算子から (無限) ツリーを計算する」で説明されているように) で拡張されたこの構造の変形と、Loop自己参照ループを示すコンストラクターを検討します。

非構造的に再帰的な関数呼び出しを使用せずに (構造的にSTreeand を再帰することができます)、無限ツリーを展開Pathする関数STree -> Tree(または同様のもの) を記述します。

追記。多くの場合、無限の展開を計算したくありません。存在する場合は有限の展開が必要であり、そうでない場合はエラーが必要です。具体的には、元のデータ型が与えられた場合:

非構造的再帰を使用せずにSTree -> Maybe Tree、構文を有限ツリーに展開する関数 (または同様の関数) を記述したいと思うかもしれません。この構造に遅延モダリティがないため、有限であることが保証されます。

この構造には遅延モダリティのインスタンスがないため、 でこれを行うことは不可能に思われfixDます。決して使用できない遅延結果が得られます。ツリーをグラフに変換し、それをトポロジカルにソートしてから、 を使用せずにガウス消去法のアルゴリズムを直接実装する必要があるように思われますfixD。

元の (間違った) コードと同じくらいエレガントに展開を実装できる別の型付け規則はありますか? もしそうなら、グラフのサイクルを見つけるための別のアルゴリズムを (再) 発見しただけかもしれません。

それで、私は最近、coinduction について少し読んでいて、今疑問に思っています: Haskell リストは帰納的ですか、それとも共帰納的ですか? Haskell ではこの 2 つを区別していないと聞いたことがありますが、もしそうなら、どのように正式に区別しているのでしょうか?

リストは帰納的に定義されますが、同時帰納的data [a] = [] | a : [a]に使用できますones = a:ones。無限リストを作成できます。それでも、有限リストを作成できます。それで、彼らはどれですか？

関連は Idris にあり、型List aは厳密に帰納型であり、したがって有限リストのみです。Haskell での定義と同じように定義されています。ただし、Stream a無限リストをモデル化する共導型です。として定義されています（というか、定義は同等です）codata Stream a = a :: (Stream a)。無限のリストや有限のストリームを作成することはできません。しかし、定義を書くと

Haskell のリストに期待する動作が得られます。つまり、有限構造と無限構造の両方を作成できます。

それでは、いくつかの核となる質問に要約してみましょう。

1. Haskell は誘導型と共誘導型を区別しませんか? もしそうなら、その公式化は何ですか？そうでない場合、[a] はどれですか?

2. HList は導帰的ですか? もしそうなら、どのようにして帰納型に有限値を含めることができますか?

3. を定義するとどうなるdata HList' a = L (List a) | R (Stream a)でしょうか? それは何と考えられますか、そして/またはそれはただよりも役に立ちHListますか?

それとも、ある型が導帰的であることを証明するのが難しすぎる場合がありますか?

私が話しているのは完全なプログラミング言語です。つまり、完全なチューリングではなく、再帰はすべて十分に根拠があり、コアカーションはすべて生産的です。チューリングの完全性は、実際にはそのような言語よりも多くのものをもたらしますか?

1) パターンマッチングなしで誘導型を使用することは可能だと思います。(_rec、_rect、_ind のみを使用)。不透明で複雑ですが、可能です。2) パターンマッチングなしで誘導型を使用することは可能ですか?

連導型から連導型の構成子領域の和集合への関数が存在する。Coqはそれを明示的に生成しますか? はいの場合、「hd」を書き換える方法は?