Закон слияния для 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