Ассоциативность монад

Question

newtype Set a = Set [a] 

Новый набор типов, содержащий список. пустой :: Установить пустой = Set []

sing :: a -> Set a 
sing x = Set [x] 

Функции для Creat набора.

memSet :: (Eq a) => a -> Set a -> Bool 
memSet _ (Set []) = False 
memSet x (Set xs) 
    | elem x xs = True 
    | otherwise = False 

{- 
makeSet :: (Eq a) => [a] -> Set a 
makeSet [] = empty 
makeset (x:xs) = union (sing x) (makeSet xs) 
-- etc 
-- we need the obvious stuff: 

union  :: Set a -> Set a -> Set a 
unionMult :: [ Set a ] -> Set a 
intersection :: Set a -> Set a -> Set a 
subSet  :: Set a -> Set a -> Bool 
mapSet  :: (a -> b) -> Set a -> Set b 
mapset f (Set xs) = makeSet (map f xs) 
-} 

-- now making it a monad: 
instance Monad Set where 
    return = sing 
    (Set x) >>= f = unionMult (map f x) 

Проверка:

Левая идентичность:

return a >>= f ≡ f a 

Право личности:

m >>= return ≡ m 

Ассоциативность:

(m >>= f) >>= g ≡ m >>= (\x -> f x >>= g) 

слева

return x >>= f 
(Set [x]) >>= f 
unionMult (map f [x]) 
unionMult [ (f x) ] = f x 

право:

(Set [xs]) >>= return 
unionMult (map return [xs]) 
unionMult [ys] 
Set [xs] 

Нужна помощь с последней.

Answer 1

unionConcat уже определена в Data.Set .... Для того, чтобы быть конкретным, я буду использовать следующие definiitions в этом доказательстве

unionConcat = Data.Set.unions 
return = Data.Set.fromList [a] 

(я буду использовать другие функции, определенные в Data.Set здесь, некоторые может потребовать «Ord a», по-видимому, это не будет проблемой).

Я также использовать следующие свойства

union x y = fromList (toList x ++ toList y) 
concat . map (:[]) = id 

Первые утверждает, что объединение двух множеств можно получить, взяв список элементов в наборе, concatinating их, а затем удаление повторы .. .. Это следует из определения того, что такое набор

Второе свойство только утверждает, что concat и map (: []) являются обратными друг другу. Это также должно быть очевидно из определения CONCAT

map (:[]) [a, b, c, ....] = [[a], [b], [c], ....] 
concat [[a], [b], [c], ....] = [a, b, c, ....] 

(Для того, чтобы действительно закончить это доказательство, я бы показать, что эти свойства следуют из определений Haskell из (: []), CONCAT и объединения, но это более подробно, что, я думаю, вы хотите, и фактические определения могут меняться от версии к версии, поэтому мы просто должны предположить, что авторы этих функций следовали духу того, как должны работать и должны выполняться concat).

(Если это не очевидно, помните, что оператор обезьяны (: []) обертывает отдельные элементы в скобках - (: []) x = [x]).

С «союзами» только кратна из смартфона как «союз» и «CONCAT» просто многократное применение (++), первый propterty может быть обобщена на

unions sets = fromList (concat $ map toLists sets) 

Теперь для proof-

y >>= return 
= unions $ map return (toList y) 
= unions $ map (fromList . (:[])) (toList y) 
= unions $ map fromList $ map (:[]) (toList y) 
= unions $ map fromList $ map (:[]) $ toList y 
= fromList $ concat $ map toList $ map fromList $ map (:[]) (toList y) 
= fromList $ concat $ map (:[]) (toList y) 
= fromList $ toList y 
= y 

QED

---

Edit- См обсуждение ниже, я сделал ошибку, и доказал, тыс e неправильный закон (d'oh, я должен был просто прочитать название вопроса :)), поэтому я добавляю правильный (ассоциативность) ниже.

Два доказать ассоциативность, нам нужно использовать два свойства ....

property 1 - toList (x >>= f) = su (toList x >>=' toList . f) 
property 2 - su (x >>=' f) = su (su x >>=' f) 

где это су сорта и uniqs список, IE-

su [4,2,4,1] = [1,2,4], 

и >> =»является массив оператор связи,

x >>=' f = concat . map f x 

Первое свойство должно быть очевиден ... Он просто утверждает, что вы можете получить результат x >> = f в два раза различными способами, либо путем применения f к значениям в наборе x, либо к объединению, либо к тем же самым значениям в соответствующем списке, и к согласованию значений. Единственное затруднение состоит в том, что вы можете получить повторяющиеся значения в списке (набор не мог даже этого допускать), поэтому вы применяете функцию su справа, чтобы канонизировать результат (обратите внимание, что toList также выводится в той же форме).

Второе свойство утверждает, что если вы отсортируете/uniq результат в конце конвейера связок, вы также можете выполнить его ранее в конвейере без изменения ответа. Опять же, это должно быть очевидно .... Добавление/удаление дубликатов или переупорядочение значений в исходном списке только добавляет/удаляет дубликаты или переупорядочивает конечный результат. Но в любом случае мы собираемся удалить дубликаты и переупорядочить в конце, так что это не имеет значения.

(Более строгое доказательство этих двух свойств может быть дано на основе определений map/concat, toList и т. Д., Но это взорвало бы размер этой публикации .... Я предполагаю, что интуиция каждого является достаточно сильным и продолжается ....)

Используя это, теперь я могу показать вам доказательства. Общий план состоит в том, чтобы использовать известную ассоциативность оператора привязки массива и отношение массивов с наборами, чтобы показать, что оператор связывания набора также должен быть ассоциативным.

С

toList set1 == toList set2 

означает, что

set1 == set2 

Я могу доказать

toList ((y >>= f) >>= g) = toList (y >>= (\x -> f x >>= g)) 

, чтобы получить желаемый результат.

toList ((y >>= f) >>= g) 
su (toList (y >>= f) >>=' toList . g) --by property 1 
su (su (toList y >>=' toList . f) >>=' toList . g) --by property 1 
su ((toList y >>=' toList . f) >>=' toList . g) --by property 2 
su (toList y >>=' (\x -> (toList . f) x >>=' toList . g)) --by the associativity of the array bind operator 
su (toList y >>=' (\x -> su (toList (f x) >>=' toList . g))) --by property 2 and associativity of (.) 
su (toList y >>=' (\x -> toList (f x >>= g))) --by property 1 
su (toList y >>=' toList (\x -> f x >>= g)) --by associativity of (.) 
su (su (toList y >>=' toList (\x -> f x >>= g))) --by property 2 
su (toList (y >>= (\x -> f x >>= g))) --by property 1 
toList (y >>= (\x -> f x >>= g)) --because toList is already sorted/uniqued 

QED

Answer 2

Поскольку Set a просто newtype вокруг [a] позволяет использовать [] непосредственно. Доказательства будут одинаковыми, пока мы используем экземпляры Set; мы сможем напрямую использовать конструкторы []. Это хорошо, потому что тогда мы можем доказать что-то индуктивно.

Мы хотим показать, что для всех . Предположим сначала, что xs == [].

[] >>= return 
unionConcat (map return []) 
unionConcat [] 
[] 

unionConcat Без определения мы можем использовать это, чтобы показать, что если unionConcat [] = [] не держится, мы не можем получить ассоциативность. Мы будем помнить об этом позже.

Теперь мы сделаем индуктивный шаг, предполагая, что у нас есть определенный xs :: [a], где xs >>= return == xs, можем ли мы показать, что (x:xs) >>= return == x:xs?

(x:xs) >>= return 
unionConcat (map return (x:xs)) 
unionConcat (return x : map return xs) 
... 
x : unionConcat (map return xs) 
x : (xs >>= return) 
x:xs         -- working upward from the bottom here 

Предоставление еще одно свойство unionConcat ---

unionConcat (return x : xs) = x : unionConcat xs 

Таким образом, даже прежде, чем мы имеем определение unionConcat мы уже можем сказать, что наши свойства будут держать контингент на ней по некоторым свойствам его собственного , Однако мы должны перевести конструктор (:) обратно в понятие для наборов.

unionConcat (return x : xs) = insert x (unionConcat xs) 

Answer 3

> U :: [Setx] --> Set x 
> 
> (m >>= f) >>= g ≡ m >>= (\x -> f x >>= g) 
> VL(leftSide) 
> (m >>= f) >>= g 
> (Set x >>= f) >>=g <=> 
> (U(map f x)) >>=g <=> (U(map f x)=Set y) 
> Set y >>= g   <=> 
> 
> 
> HL:(right Side) 
> m >>= (\x -> f x >>= g)  <=> 
> Set x >>=(\x -> f x >>= g) (funktionen \x -> f x gives a Set y it will consume value of x.) 

Но это prrof я неправильно. (U = UnionMult.) Мне сказали, что я должен попытаться создать структуру функций для левой и правой сторон. Это поможет показать, что правая и левая стороны равны. HL: RightSide VL LeftSide хотят показать VL == HL