18

私はデータ型を持っています

data N a = N a [N a]

バラの木と Applicative インスタンスの

instance Applicative N where
 pure a = N a (repeat (pure a))
 (N f xs) <*> (N a ys) = N (f a) (zipWith (<*>) xs ys)

適用法を証明する必要があります。ただし、pureは無限に深く、無限に分岐するツリーを作成します。したがって、たとえば、準同型の法則を証明する際に、

pure f <*> pure a = pure (f a)

等式の証明だと思った

zipWith (<*>) (repeat (pure f)) (repeat (pure a)) = repeat (pure (f a))

近似（またはテイク）によって補題が機能します。しかし、私の試みは、帰納的なステップで「悪循環」につながります。特に、削減

approx (n + 1) (zipWith (<*>) (repeat (pure f)) (repeat (pure a))

与える

(pure f <*> pure a) : approx n (repeat (pure (f a)))

ここで、approxは近似関数です。明示的な帰納的証明なしに、どうすれば等しいことを証明できますか?

4

3 に答える 3

4

私は unfolds のユニバーサル プロパティを使用します (repeat と適切に非カリー化された zipWith は両方とも unfolds であるため)。私のブログに関連する議論があります。しかし、独自の修正点ICFP2008に関する Ralf Hinze の論文(およびその後の JFP 論文) も気に入るかもしれません。

（確認してください：あなたのバラの木はすべて無限に広く、無限に深いですか？そうでなければ法則は成立しないと思います。）

于 2011-05-18T16:11:44.890 に答える
3

以下は、機能し、プログラム構文と等式推論のレベルにとどまっていると私が考えるもののスケッチです。

基本的な直感はrepeat x、一般的に、ストリーム (さらに悪いことにリスト) について推論するよりも、推論する方がはるかに簡単だということです。

uncons (repeat x) = (x, repeat x)

zipWithAp xss yss = 
    let (x,xs) = uncons xss
        (y,ys) = uncons yss
    in (x <*> y) : zipWithAp xs ys

-- provide arguments to zipWithAp
zipWithAp (repeat x) (repeat y) = 
    let (x',xs) = uncons (repeat x)
        (y',ys) = uncons (repeat y)
    in (x' <*> y') : zipWithAp xs ys

-- substitute definition of uncons...
zipWithAp (repeat x) (repeat y) = 
    let (x,repeat x) = uncons (repeat x)
        (y,repeat y) = uncons (repeat y)
    in (x <*> y) : zipWithAp (repeat x) (repeat y)

-- remove now extraneous let clause
zipWithAp (repeat x) (repeat y) = (x <*> y) : zipWithAp (repeat x) (repeat y)

-- unfold identity by one step
zipWithAp (repeat x) (repeat y) = (x <*> y) : (x <*> y) : zipWithAp (repeat x) (repeat y)

-- (co-)inductive step
zipWithAp (repeat x) (repeat y) = repeat (x <*> y)
于 2011-03-07T16:43:20.153 に答える
1

なぜ共誘導が必要なのですか？誘導するだけ。 

pure f <*> pure a = pure (f a)

と書くこともできます（左右が等しいことを証明する必要があります）

N f [(pure f)] <*> N a [(pure a)] = N (f a) [(pure (f a))]

これにより、一度に 1 つのタームをオフにすることができます。それはあなたの誘導を与えます。

于 2011-03-10T18:40:42.080 に答える