問題タブ [induction]

任意の帰納型はそのように定義されます

inductionタイプがあり(f a -> a) -> Ind f -> aます。これには、共誘導と呼ばれる二重の概念があります。

coinductionタイプがあり(a -> f a) -> a -> CoInd fます。inductionとが二重であることに注意してくださいcoinduction。帰納的および共導的なデータ型の例として、このファンクターを見てください。

再帰がなければ、Ind StringFは有限文字列であり、有限文字列CoInd StringFまたは無限文字列です (再帰を使用すると、それらは両方とも有限文字列または無限文字列または未定義文字列になります)。Ind f -> CoInd f一般に、任意の Functorに変換できfます。たとえば、ファンクター値を共導型にラップできます

Maybeこの操作は、各ステップに余分な操作 (パターン マッチング) を追加します。これは、O(n)オーバーヘッドが発生することを意味します。

Ind fとをwrap得るために帰納法を使うことができますCoInd f。

これはO(n^2)。(最初のレイヤーを取得するのは ですO(1)が、n 番目の要素はO(n)入れ子になったMaybes によるため、この合計になります。) 二重に、帰納型を取り、その最上位の Functor レイヤーを明らかにする をO(n^2)定義できます。cowrap

inductionいつもO(n)そうですcowrap。

からとcoinductionを生成するために使用できます。CoInd fcowrapInd f

これもO(n)要素を取得するたびに、合計でO(n^2).

Ind f私の質問は、再帰を (直接的または間接的に) 使用せずにCoInd f、O(n)時間内に変換できるかどうかです。

私は再帰でそれを行う方法を知っています (に変換Ind fしてFix fからFix f(CoInd f最初の変換はO(n)に変換されますが、 からの各要素CoInd fはO(1)であり、2 番目の変換のO(n)合計は になりO(n) + O(n) = O(n)ます))、それなしで可能かどうかを確認したいと思います。

直接的または間接的に再帰を使用していないことconvertに注意してください。convert'気の利いたですね！

moll n = doll nステートメントを確立するために誘導を行うにはどうすればよいですか?

n = 0 の基本ケースを証明しようとしました

についてn+1、それを示してください

しかし、今はどうですか？これ以上単純化するにはどうすればよいですか？

私は Dafny でのレンマの使用を見てきましたが、理解するのが難しいと感じており、明らかに以下の例は検証されていません。これはおそらく、Dafny が帰納法またはカウントのいくつかのプロパティを証明するためのレンマのようなものを見ていないためです。 ? 基本的に、カウントが帰納的であるなどのことを Dafny に納得させるために、何をどのように定義する必要があるのか​​ わかりません。保証と不変条件の仕様の一部は必要ありませんが、それは重要ではありません。ところで、これは Spec# の方が簡単でした。