Функция форматирования числа

intString :: Int -> [Char]

intString = map digitChar

. reverse

. map (`rem` 10)

. takeWhile (\=0)

. iterate (/10)

IntString x = (f1,f2,..,f5) x / /вся композиция применяется к x.

Такое определение можно сократить.

intString = (f1,f2,…,f5)

эта операция называется c-редукция.

Законы функциональных программ

Подобно тому, как преобр в курсе школьной алгебры, такие же преобразования можно делать и в функц программе.

(a+b)² = a² + 2ab + b²

Функции в хаскелле похожи на функции в математике. Два выражения равны если они всегда вычисляют одинаковые значения. Равные выражения явл взаимозаменяемыми.

map f (x:xs) = x:

map f xs

замена левой части на правую назыв раскрытием по распределению.

Замена правой на левую – сверткой.

Есть термин fold(свернуть) /unfold(раскрытие определения)

n-редукция

Если

f x = g x

То

f = g

эти определения эквивалентны.

Начнем с применения законов функциональных программ. Вспомним фкотораяформ число

intString :: Int -> [Char]

intString = map digitChar

. reverse

. map ( `rem` 10)

. takeWhile(/=0)

. iterate (`div` 10)

Можно усовершенствовать если применить законы

1) еомпозиция map f . reverse – коммутативна

2) дистрибутивность map относительно композиции

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

intString’ :: Int -> [Char]

intString’ = map (digitChar . (`rem` 10))

. reverse

. takeWhile(/=0)

. iterate (`div` 10)

Теперь это быстрее и не создает промежуточный список.

Примеры законов и их доказательств

1) ассоциативность операторов композицийфункций

Для всех функций f,g,h, если правильно определены их типы, выоплняется равенство

f . ( g . h) = ( f . g). H

суть доказательства в том что обе части равенства приводятсяк одному и тому же виду.

f . ( g . h)	( f . g). h
x (f.(g.h)) x = (опр.(.)) f((g . h) x) =(опр.(.)) f (g (h x))	(( f . g). h) x = (опр.(.)) (f.g) (h x) = (опр.(.)) f (g (h x))

Закон “map после (:)”

Для всех значений x и функций f, если правильно определены их типы, выполняется равенство:

map f . ( x: ) = ((f x) :) . map f

map f . ( x: )	((f x) :) . map f
Xs (map f . (x:)) xs =(опр.(.)) Map f ((x:) xs) =(опр.сечения) Map f (x:xs) = (опр. Map) F x :map f xs	((( f x) :) . map f

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

Мат индукция

P (n) n прин N

1 P(0) доказать

2 P(n) => P(n+1)

Эти два утверждения позв рекурсивно пробежать все натур числа.

Метод структурной индукции.

Конструктор арности 0

Потом для succ /1

Если брать список то его можно определить подобным образом

data list a

= Nil

| Cons a (list a)

Для списков можно строить доказательство по индукции след образом.

1) нужно доказать свойство для пустого списка

P([])

2) предполагая свойства для списка xs доказанным, надо показать что оно вып для x:xs

P(xs) => P(x:xs)

Мы будем доказывать свойство P для списка x:xs предполагая что свойство вып для хвоста xs. Это утв назыв индуктивная гипотеза.

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

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

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

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

Xs map f (xs++ys)	map f xs ++ map f ys
[] map f ([]++ys) =(опр.(++)) map f ys	map f[] ++ mapf ys =(опр.map) []++map f ys =(опр.(++)) map f ys
x: map f ((x:xs)++ys) xs =(опр.(++)) map f (x:(xs++ys) = (опр.map) f x:map f (xs++ys)	map f (x:xs) ++map f ys =(опр.map) (f x:map f xs) ++map f ys =(опр.(++)) f x: map f xs ++ map f ys

На основании индуктивной гипотезы мы эти подчеркнутые гипотезы можем считать равными.