Доказательство равенства потоков

У меня есть тип данных

data N a = N a [N a]

розовых деревьев и аппликативный экземпляр

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

и нужно доказать для нее Аппликативные законы. Однако чистое создает бесконечно глубокие, бесконечно ветвящиеся деревья. Так, например, доказав закон гомоморфизма

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)))

где ап - аппроксимационная функция. Как я могу доказать равенство без явного коиндуктивного доказательства?

Ответ 1

Ниже приводится эскиз того, что, по моему мнению, работает и остается на уровне программного синтаксиса и эквациональных рассуждений.

Основная интуиция заключается в том, что гораздо легче рассуждать о 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)

Ответ 2

Я бы использовал универсальное свойство разворачивания (так как разворачиваются повторяющиеся и незанятые zipWith). В моем блоге есть связанное обсуждение . Но вам также могут понравиться работы Ральфа Хинзе по уникальным фиксированным точкам ICFP2008 (и последующая бумага JFP).

(Просто проверяя: все ваши розовые деревья бесконечно широкие и бесконечно глубокие? Я предполагаю, что законы не останутся иначе).

Ответ 3

Почему мне нужна монетация? Просто вводят.

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

также можно записать (вам нужно доказать равенство влево и вправо)

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

который позволяет вам отключать один термин за раз. Это дает вам вашу индукцию.