Закон map через foldr

Для всех списков xs и функций f выполняется равенство:

map f xs = foldr g [] xs

where g y ys = f y: ys

при условии что правильно определены типы.

Вспомним, что

foldr + 0 [1,2,3] =(1+(2+(3+0)))

доказательсов, по списку xs

xs map f xs	foldr g [] xs
[] map f [] = (опр.map) []	foldr g [] [] = (опр.foldr) []
x: map f (x:xs) xs = (опр.map) f x : map f xs	foldr g [] (x:xs) =(опр.foldr) g x(foldr g [] xs) =(опр. g) f x : foldr g [] xs

Закон: композиция

map f . reverse –

Коммутативна

Пар.	Пар. (map f) . reverse	reverse . (map f)
[]	[] ((map f). reverse) [] =(опр.(.)) (map f) ( reverse [] ) =(опр. Reverse) (map f) [] =(опр.map) []	(reverse . (map f)) [] = (opred.(.)) (reverse (map f []) =(opred.map) reverse [] =(opred. Reverse) []
x:xs	((map f) . reverse) (x:xs) =(опр.(.)) map f (reverse (x:xs)) =(опр. Reverse) map f ((reverse xs)++[x]) =(закон “mapпосле (++)”) map f (reverse xs) ++ map f [x] =(опр.map) map f (reverse xs) ++ [f x] =(опр.(.)) ((map f) . reverse) xs ++ [f x]	(reverse . (map f)) (x:xs) =(опр.(.)) (reverse (map f (x:xs)) =(опр.map) (reverse (( f x) : (map f xs) ) =(опр.reverse) reverse (map f xs) ++ [f x] =(опр.(.)) (reverse . (map f)) xs ++ [f x]

Рассмотрим ее один закон

Дистрибутивность map относительно композиции:

map f . map g = map (f.g)

Пар.	Map f . map g	Map (f.g)
[]	(map f . map g) [] =(опр.(.)) map f (map g []) =(опр.map) (map f) [] =(опр.map) []	(map (f.g)) [] = (опр.map) []
x: xs	(map f . map g) (x:xs) =(опр.(.)) map f (map g (x:xs)) =(opred.map) map f (g x : (map g xs)) =(opred.map) f (g x) : (map f (map g xs)) (opred. (.) 2 raza) (f.g) x : (map f . map g) xs	map (f.g) (x:xs) =(opred.map) (f.g) x : map (f.g) xs

Преобразование программ

Трудно на практике написать программу правильную и эффективную. Но можно написать сначала правильную программу, а потом преобразовать ее к более эффективному виду.

Рассмотрим возможные шаги преобразования программы.

1 раскрыть определение (unfold)

Если заданы определения

А=А’ и B=B’

Тогда можно использовать определение

A=A’ [B/B’] // операция замены одного выражения на другое

Пример

map f [] = []

map f (x:xs) = f x : map f xs

z = map g (y:ys)

Можно использовать определение

z = g y : map g ys

2 свернуть по определению (fold)

Если заданы определения

A=A’ и B=B’

Тогда можно использовать определение

A=A’ [B’/B]

Пример

map f [] = []

map f (x:xs) = f x : map f xs

z = []

Можно использовать определение

z = map g []

3 введение нового определения

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

let

Нельзя ввести x=6

x=5

in let

y=10

in x+y

4 конкретизация

Если задано определение

A=A’

Содержащее связанную переменную х, тогда можно использовать определение

A[x/E] = A’ [x/E]

Пример

av l = (sum l, len l)

(l мы можем например заменить на пустой список)

Можно использовать определения

av [] = (sum [], len [])

av (n:ns) = (sum (n:ns), len(n:ns))

5 абстракция

Если задано определение

A=A’

Содержащее выражение E1,E2..En, тогда можно использовать определение

A=A’[E1/x1][E2/x2]…[En/xn]

where (x1,x2,..xn) = (E1, E2, …En)

Пример (среднее значение списка)

average l = sum l `div` len l

Можно использовать определение

average l = u `div` v

where (u,v) = (sum l, len l)

6 применение закона

Если задано определение

A=A’

И доказан закон

E=E’

Тогда можно использовать определение

A=A’[E/E’]

Пример

foo f xs ys = map f (xs++ys)

Можно использовать определение

foo f xs ys = map f xs ++ map f ys

(Закон map после (++))