Закон слияния для foldr1?

Question

Для foldr мы имеем закон слияния : если f строгое, f a = b и

f (g x y) = h x (f y) для всех x, y, затем f . foldr g a = foldr h b.

Как можно обнаружить / вывести подобный закон для foldr1? (Очевидно, что он даже не может принять одну и ту же форму - рассмотрим случай, когда обе стороны действуют на [x].)

Answer 1

Вы можете использовать свободные теоремы для получения таких утверждений, как закон слияния. Автоматическая генерация свободных теорем делает эту работу за вас, она автоматически выводит следующее утверждение, если вы введете foldr1 или тип (a -> a -> a) -> [a] -> a.

Если f строгий и f (p x y) = q (f x) (f y)) для всех x и y, у вас есть f (foldr1 p z) = foldr1 q (map f z)). То есть, в отличие от вашего утверждения о foldr, вы получаете дополнительный map f с правой стороны.

Также обратите внимание, что свободная теорема для foldr немного более общая, чем ваш закон слияния, и, следовательно, выглядит очень похоже на закон для foldr1. А именно у вас есть для строгих функций g и f, если g (p x y) = q (f x) (g y)) для всех x и y, то g (foldr p z v) = foldr q (g z) (map f v)).

Answer 2

Я не знаю, будет ли что-нибудь удовлетворительное для foldr1. [Я думаю] Это просто определено как

foldr1 f (x:xs) = foldr f x xs

давайте сначала расширим то, что у вас есть выше, для работы со всем списком,

f (foldr g x xs) = foldr h (f x) xs

для foldr1, можно сказать,

f (foldr1 g xs) = f (foldr g x xs)
= foldr h (f x) xs

для повторного уплотнения в foldr1, вы можете создать некоторую мнимую функцию, которая отображает f на левый элемент, в результате,

f . foldr1 g = foldr1 h (mapfst f) where
    mapfst (x:xs) = f x : xs