доказать foldr f n xs = foldl f n xs при условии, что f x (f y z) = f (f x y) z

Доказать с помощью аксиомы структурной индукции справедливость свойства:
foldr f n xs = foldl f n xs при условии, что f x (f y z) = f (f x y) z

0

Может как-то так начать:

1.
2.
Дальше — хз, ничего в этом не понимаю.

1

Я сначала подумал, что доказательство можно найти почти в любом учебнике по списковому программированию, но максимум, что я смог найти, этов «Merging Monads and Folds for Functional Programming» Эрика Мейера.

Во-первых, это равенство не выполняется, если xs — бесконечный список.
Действительно, foldl f n xs = _|_, в то время как foldr f n xs вполне может иметь (головную) нормальную форму, если f нестрогая.
Пусть xs — конечный список и L — его длина.
Как было сказано, foldr f n (x:xs) = foldl f n (x:xs) тогда и только тогда, когда f n (foldr f n xs) = foldl f (f n x) xs

Сперва докажем вспомогательную лемму: foldr t (x:xs) = f t (foldr x xs) = foldr f (f t x) xs
Доказательство индуктивное, то есть основывается на свойстве универсальности катаморфизма foldr.
База индукции f t (foldr x []) = foldr f (f t x) [] = f t x
Индуктивный шаг f t (foldr x' (x:xs)) = f t (f x' (foldr x xs)) = f (f t x') (foldr x xs) = foldr f (f t x') (x:xs)

Построим индуктивное доказательство в L шагов.
База индукции foldr f n [] == foldl f n [], foldr f n [x] == foldl f n [x] и foldr f n [x,y] == foldl f n [x,y]
Шаг индукции:
1. Предположение foldr f n (x:xs) == foldl f n (x:xs) и foldr f n xs = foldl f n xs для любых f, n, x и конечного xs
2. foldr f n (x:xs) = foldr f (f n x) xs по лемме
3. foldr f (f n x) xs = foldl f (f n x) xs по предположению
4. foldl f (f n x) xs = foldl f n (x:xs)
5. Следовательно, foldr f n (x:xs) = foldl f n (x:xs)

Добавлено через 2 минуты
Кстати, доказательство было бы в два раза короче, если бы мы доказывали foldr1=foldl1

3