Haskell - Как преобразовать максимум (xs ++ map (x+) xs) в max (максимум xs) (x + максимум xs)
Один из упражнений в "Мышление функционально с Haskell" о том, как сделать программу более эффективной с использованием закона слияния. У меня возникли проблемы при попытке повторить ответ.
Часть расчета требует, чтобы вы преобразовали maximum (xs ++ map (x+) xs) в max (maximum xs) (x + maximum xs) посредством эквалайзера.
maximum определяется как foldr1 max и так как я не знаю многих правил, касающихся foldr1, я застрял даже в первой части, которая должна преобразовать foldr1 max (xs ++ map (x+) xs) в max (foldr1 max xs) (foldr1 max (map (x+) xs)) так что это первое, что я хотел бы понять.
Как только мы преодолеем это, следующая часть кажется более сложной, т.е. foldr1 max (map (x+) xs) в x + foldr1 max xs, Интуитивно это имеет смысл; если вы находите максимальное значение группы чисел, к которым добавлен символ "x", то это то же самое, что найти максимум всех чисел до добавления "x" и добавить "x" к результату.
Единственное, что я нашел, чтобы помочь мне на этом втором этапе, - это ответ о переполнении стека, где ответ в основном дан вам (если вы предполагаете p = q) без отдельных простых для понимания шагов, которые вы обычно видите с помощью эквационального рассуждения.
Так, пожалуйста, может кто-нибудь показать мне шаги, чтобы сделать преобразование?
2 ответа
Это можно увидеть по индукции.
Предположим, xs == [], Оба выражения верны, так как оба дают error,
Предположим, xs == [y]
maximum([y]++map(x+)[y]) == -- by definition of map
== maximum([y]++[x+y])
-- by definition of ++
== maximum([y,x+y])
-- by definition of maximum
== foldr1 max [y,x+y]
-- by definition of foldr1
== max y (foldr1 max [x+y])
-- by definition of foldr1
== max y (x+y)
-- by definition of foldr1 and maximum [y]
== max (maximum [y]) (x+maximum [y])
Далее нам понадобится доказательство коммутативности maximum: maximum (xs++(y:ys)) == max y (maximum (xs++ys)) - вы заметите, что это необходимо, если вы пропустите это доказательство и сразу перейдете к доказательству maximum (y:ys ++ map(x+)(y:ys)) - Один шаг туда требует перемещения (x+y) с середины списка ys++(x+y):map(x+)ys,
Предположим, xs==[]:
maximum ([]++(y:ys)) == maximum (y:ys)
-- by definition of foldr1 and maximum
== max y (maximum ys)
== max y (maximum ([]++ys))
Предположим, xs==x:xx:
maximum(x:xx++(y:ys)) == maximum (x:(xx++(y:ys)))
-- by definition of foldr1 and maximum
== max x (maximum (xx++(y:ys)))
-- by induction
== max x (max y (maximum (xx++ys)))
-- by commutativity of max, max a (max b c) == max b (max a c)
== max y (max x (maximum (xx++ys)))
-- by definition of foldr1 and maximum
== max y (maximum (x:(xx++ys)))
-- by definition of ++
== max y (maximum ((x:xx) ++ ys))
Хорошо, теперь вернемся к доказательству исходного утверждения. Теперь предположим, xs == y:ys
maximum (y:ys ++ map(x+)(y:ys)) ==
-- by definition of map
== maximum(y:ys ++ (x+y):map(x+)ys)
-- by definition of foldr1 and maximum
== max y (maximum(ys ++ (x+y):map(x+)ys)
-- by commutativity of maximum
== max y (max (x+y) (maximum (ys++map(x+)ys)))
-- by induction, (maximum (ys++map(x+)ys)) == max (maximum ys) (x+maximum ys))
== max y (max (x+y)
(max (maximum ys) (x+maximum ys)))
-- by commutativity of max (ie max a (max b c) == max b (max a c))
== max y (max (maximum ys)
(max (x+y) (x+maximum ys)))
-- by associativity of max (is max a (max b c) == max (max a b) c)
== max (max y (maximum ys))
(max (x+y) (x+maximum ys)))
-- by definition of max, max (x+y) (x+z) == x+(max y z)
== max (max y (maximum ys))
(x + max y (maximum ys)))
-- by definition of foldr1 and maximum
== max (maximum (y:ys)) (x + maximum (y:ys))
Так как вы спрашивали также об индукции и о том, как увидеть определенную вещь, можно доказать с помощью индукции, вот еще кое-что.
Вы можете увидеть некоторые шаги "по определению" - мы знаем, что они верны, посмотрев, как написана функция. Например, maximum = foldr1 max а также foldr1 f (x:xs) = f x $ foldr1 f xs для непустых xs, Определение некоторых других вещей менее ясно - max y z определение max не показан; тем не менее, по индукции можно показать, что max (x+y)(x+z) == x+max y z, Здесь можно начать с определения max 0 y == yтогда как потренироваться max для большего x, (Тогда вам также необходимо покрыть дела для отрицательных x а также y Аналогичным образом.)
Например, натуральные числа равны нулю и любой преемник натурального числа. Видите ли, здесь у нас нет определенного сравнения, ничего. Итак, свойства сложения, вычитания, максимума и т. Д. Вытекают из определения функций:
data Nat = Z | S Nat -- zero and any successor of a natural number
(+) :: Nat -> Nat -> Nat -- addition is...
Z + x = x -- adding zero is neutral
(S x) + y = S (x + y) -- recursive definition of (1+x)+y = 1+(x+y)
-- here unwittingly we introduced associativity of addition:
-- (x+y)+z=x+(y+z)
-- so, let's see the simplest case:
-- x == Z
-- (Z+y)+z == -- by definition, Z+y=y -- see the first line of (+)
-- == y+z
-- == Z+(y+z) -- by definition, Z+(y+z)=(y+z)
--
-- ok, now try x == S m
-- (S m + y) + z == -- by definition, (S m)+y=S(m+y) -- see the second line of(+)
-- == S (m+y) + z
-- == S ((m+y)+z) -- see the second line of (+)
-- - S (m+y) + z = S ((m+y)+z)
-- == S (m+(y+z)) -- by induction, the simpler
-- case of (m+y)+z=m+(y+z)
-- is known to be true
-- == (S m)+(y+z) -- by definition, see second line of (+)
-- proven
Тогда, потому что у нас нет сравнения Натс, нужно определить max определенным образом.
max :: Nat -> Nat -> Nat
max Z y = y -- we know Z is not the max
max x Z = x -- and the other way around, too
-- this inadvertently introduced commutativity of max already
max (S x) (S y) = S (max x y) -- this inadvertently introduces the law
-- that max (x+y) (x+z) == x + (max y z)
Предположим, мы хотим доказать последнее. Предполагать x == Z
max (Z+y) (Z+z) == -- by definition of (+)
== max y z
== Z + (max y z) -- by definition of (+)
хорошо, теперь предположим x == S m
max ((S m) + y) ((S m)+z) == -- by definition of (+)
== max (S(m+y)) (S(m+z))
-- by definition of max
== S (max (m+y) (m+z))
-- by induction
== S (m+(max y z))
-- by definition of (+)
== (S m)+(max y z)
Итак, вы видите, важно знать определения, важно доказать простейший случай и важно использовать доказательство для более простого случая в немного более сложном случае.
Эскиз:
maximum (xs ++ map (x+) xs)
foldr1 max (xs ++ map (x+) xs)
foldr max (foldr1 max xs) (map (x+) xs)
foldr max (maximum xs) (map (x+) xs)
max (maximum xs) (foldr1 max (map (x+) xs))
max (maximum xs) (x + foldr1 max xs)
max (maximum xs) (x + maximum xs)
используя (могут быть более слабые предположения, я выбрал то, что работает)
0. xs, ys are nonempty
1. f is commutative and associative
A. foldr1 f (xs ++ ys) == foldr f (foldr1 f xs) ys
B. foldr f s xs = f s (foldr1 f xs)
C. foldr1 f (map g xs) = g (foldr1 f xs)
if f (g x) (g y) == g (f x y)
Доказательства леммат следуют по индукции. Во-первых, давайте вспомним наши определения:
foldr k z [] = z
foldr k z (x:xs) = k x (foldr k z xs)
foldr1 k [z] = z
foldr1 k (x:xs) = k x (foldr1 k xs)
map k [] = []
map k (x:xs) = k x : map k xs
Тогда для А:
To show: foldr1 f (xs ++ ys) == foldr f (foldr1 f xs) ys
Induction on xs.
Base case: xs = [x]
foldr1 f ([x] ++ ys) == f x (foldr1 f ys)
Induction on ys: ys = [y]
== f x (foldr f [y]) = f x y = f y x
== foldr f x [y] = foldr f (foldr1 f [x]) [y]
Step. ys = (y:yy)
== f x (foldr1 f (y:yy))
== f x (f y (foldr1 f yy)) -> associativity and commutativity
== f y (f x (foldr1 f yy)) -> induction assumption
== f y (foldr f x yy)
== foldr f (foldr1 f [x]) (y:yy)
Step: xs = (x:xx)
foldr1 f (x:xx ++ ys) = f x (foldr1 f (xx ++ yy))
== f x (fold f (foldr1 f xx) yy)
== fold f (foldr1 f xx) (x:yy)
Induction on ys.
Base case ys = [y]
== f x (f y (foldr1 f xx)) == f y (f x (foldr1 f (x:xx))
== fold f (foldr1 f xs) [y]
Step. ys = (y:yy)
== f x (f y (fold f (foldr1 f xx) yy) -> associativity, commutativity
== f y (f x (fold f (foldr1 f xx) yy) -> induction assumption
== f y (fold f (foldr1 f (x:xx) yy)
== fold f (foldr1 f xs) ys
И так далее, попробуйте сами.