15 
> {-# LANGUAGE DeriveFunctor, Rank2Types, ExistentialQuantification #-}

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

> newtype Ind f = Ind {flipinduct :: forall r. (f r -> r) -> r}
> induction = flip flipinduct

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

> data CoInd f = forall r. Coinduction (r -> f r) r
> coinduction = Coinduction

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

> data StringF rec = Nil | Cons Char rec deriving Functor

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

> wrap :: (Functor f) => f (CoInd f) -> CoInd f
> wrap fc = coinduction igo Nothing where
>   --igo :: Maybe (CoInd f) -> f (Maybe (CoInd f))
>   igo Nothing  = fmap Just fc
>   igo (Just (Coinduction step seed)) = fmap (Just . Coinduction step) $ step seed

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

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

> convert :: (Functor f) => Ind f -> CoInd f
> convert = induction wrap

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

> cowrap :: (Functor f) => Ind f -> f (Ind f)
> cowrap = induction igo where
>    --igo :: f (f (Ind f)) -> f (Ind f)
>    igo = fmap (\fInd -> Ind $ \fold -> fold $ fmap (`flipinduct` fold) fInd)

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

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

> convert' :: (Functor f) => Ind f -> CoInd f
> convert' = coinduction cowrap

これも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'気の利いたですね！

4

1 に答える 1

1

はい、これは正式に可能です:

https://github.com/jyp/ControlledFusion/blob/master/Control/FixPoints.hs

ただし、変換には、実行時にループを使用してのみ行うことができる中間バッファーの構築が依然として必要です。

この制限の根底にある理由は、「帰納的」タイプの値は与えられた評価順序 (*) に応答するのに対し、「共帰納的」タイプの値は評価の順序を固定するためです。多くの再計算を強制せずに移行を可能にする唯一の方法は、何らかの中間バッファーを割り当てて、中間結果をメモすることです。

ところで、'co-inductive' から 'inductive' への変換にはバッファは必要ありませんが、明示的なループを使用して評価順序を具体化する必要があります。

ところで、私は 2 つの論文で基礎となる概念を研究しました 。http://lopezjuan.com/limestone/vectorcomp.pdf

(*)厳密な言語を想定しています。遅延評価があると状況は少し変わりますが、概念と最終的な答えは同じです。ソースコードには遅延評価に関するコメントがいくつかあります。

于 2015-12-10T21:19:54.920 に答える