2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки


Правила форума


В этом разделе нельзя создавать новые темы.

Если Вы хотите задать новый вопрос, то не дописывайте его в существующую тему, а создайте новую в корневом разделе "Помогите решить/разобраться (М)".

Если Вы зададите новый вопрос в существующей теме, то в случае нарушения оформления или других правил форума Ваше сообщение и все ответы на него могут быть удалены без предупреждения.

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

Обязательно просмотрите тему Правила данного раздела, иначе Ваша тема может быть удалена или перемещена в Карантин, а Вы так и не узнаете, почему.



Начать новую тему Ответить на тему На страницу 1, 2  След.
 
 Моноид в аппликативном функторе - моноид?
Сообщение16.10.2015, 16:33 


05/09/12
2587
При решении одной задачки возникло такое предположение, и частично я вроде даже провел некоторые правдоподобные рассуждения, чтобы попытаться его доказать. Собственно, утверждение:
Мы имеем некоторый моноид. Применяем к нему аппликативный функтор. Получаем структуру, которая предположительно также является моноидом, с нейтральным элементом - нейтральным элементом исходного моноида при применении к нему этого функтора, и бинарной операцией - операцией исходного моноида, погруженной в контекст этого функтора, то есть:
Используется синтаксис Haskell
1) mempty' = pure mempty
2) mappend' a b = fmap mappend a <*> b (или mappend' = liftA2 mappend)

Таким образом можно неограниченно оборачивать моноиды в любое количество любых аппликативных функторов, сохраняя моноидальность результата. Я попробовал доказать выполнение условий левой и правой единиц образованного таким образом моноида, ассоциативность бинарной операции пока не осилил. Выкладки (после знаков равенства записаны номера тождеств, которые применялись при преобразованиях, тождества выписаны не все, а только которые потребовались для доказательства):
код: [ скачать ] [ спрятать ]
Используется синтаксис Haskell
Моноид:
m1) mappend mempty = id

Функтор:
f1) fmap id = id
f2) fmap (f . g) = fmap f . fmap g

Аппликативный функтор:
a1) pure f <*> pure x = pure (f x)
a2) u <*> pure y = pure ($ y) <*> u
a3) pure f <*> x = fmap f x

Новый моноид:
1) mempty' = pure mempty
2) mappend' a b = fmap mappend a <*> b (mappend' = liftA2 mappend)

Левая единица:
mappend' mempty' x = (1,2)
fmap mappend (pure mempty) <*> x = (a3)
(pure mappend) <*> (pure mempty) <*> x = (a1)
pure (mappend mempty) <*> x = (a3)
fmap (mappend mempty) x = (m1)
fmap id x = (f1)
x

Правая единица:
mappend' x mempty' = (1,2)
fmap mappend x <*> (pure mempty) = (a2)
pure ($ mempty) <*> (fmap mappend x) = (a3)
fmap ($ mempty) (fmap mappend x) = (f2)
fmap ($ mempty . mappend) x =
fmap (mappend mempty) x = (m1)
fmap id x = (f1)
x

Собственно, у меня несколько вопросов:
1) Не ошибся ли я в своих выкладках?
2) Натолкнёте на идею доказательства/опровержения последнего закона моноида - ассоциативности новой бинарной операции?
3) Справедливо ли вообще мое предположение о том, что это моноид?

ЗЫ пишу в этот раздел, т.к. вопрос теоретический, а не практического программирования.

 Профиль  
                  
 
 Re: Моноид в аппликативном функторе - моноид?
Сообщение16.10.2015, 21:12 
Заслуженный участник


27/04/09
28128
Я щас предложу ерунду, так что не бейте. По непроверенному ощущению, если взять свободный моноид на трёх образующих $a, b, c$ и обработать подобным образом, то если в «функторном моноиде» $a'(b'c') = (a'b')c'$, всё в порядке. Это выглядит как какая-то ересь, но если верно, можно просто взять немного кода и напрямую это проверить. В качестве образующих можно взять "1", "2", "3" (а моноид, соответственно, String). Буду рад опровержению, а сам что-то не додумаюсь.

 Профиль  
                  
 
 Re: Моноид в аппликативном функторе - моноид?
Сообщение16.10.2015, 23:22 


05/09/12
2587
Вот немного кода и проверка ассоциативности напрямую - на примере трех аппликативных функторов: Maybe, [] и их композиции:
код: [ скачать ] [ спрятать ]
Используется синтаксис Haskell
import Data.Monoid
import Data.Functor
import Control.Applicative

newtype NT m a = NT (m a) deriving (Eq,Show)

instance (Monoid a, Applicative m) => Monoid (NT m a) where
    mempty = NT $ pure mempty
    mappend (NT a) (NT b) = NT $ mappend <$> a <*> b

main = do
    print $ (NT (Just "a") <>  NT (Just "b")) <> NT (Just "c")
    print $  NT (Just "a") <> (NT (Just "b")  <> NT (Just "c"))
    print $ (NT ["a"] <>  NT ["b"]) <> NT ["c"]
    print $  NT ["a"] <> (NT ["b"]  <> NT ["c"])
    print $ (NT (Just $ NT ["a"]) <>  NT (Just $ NT ["b"])) <> NT (Just $ NT ["c"])
    print $  NT (Just $ NT ["a"]) <> (NT (Just $ NT ["b"])  <> NT (Just $ NT ["c"]))
 

Используется синтаксис Haskell
NT (Just "abc")
NT (Just "abc")
NT ["abc"]
NT ["abc"]
NT (Just (NT ["abc"]))
NT (Just (NT ["abc"]))
https://ideone.com/OXkl6d

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

 Профиль  
                  
 
 Re: Моноид в аппликативном функторе - моноид?
Сообщение16.10.2015, 23:39 
Заслуженный участник


27/04/09
28128
_Ivana в сообщении #1063543 писал(а):
Но одно дело - проверить на нескольких конкретных аппликативных функторах, а совсем другое - строго доказать для любых.
Так если теперь применить equational reasoning? (то проблема сводится в точности к исходной, вижу свой ляп).

-- Сб окт 17, 2015 02:39:17 --

Кажется, соотношения

Используется синтаксис Haskell
pure (.) <*> u <*> v <*> w = u <*> (v <*> w)
fmap f x = pure f <*> x

приводят обе штуки к

Используется синтаксис Haskell
pc <*> pc <*> pc <*> pma <*> pma <*> a <*> b <*> c where
    pc = pure (.)
    pma = pure mappend

Одну из них (левоассоциативную) — точно, а другую стало лень доделывать.

P. S. Вот первая, если вдруг что (app = mappend) — перепроверьте:

Используется синтаксис Haskell
[1] = pure app <*> (pure app <*> a <*> b) <*> c
[1] = pure (.) <*> pure app <*> (pure app <*> a) <*> b <*> c
[1] = pure (.) <*> (pure (.) <*> pure app) <*> pure app <*> a <*> b <*> c
[1] = pure (.) <*> pure (.) <*> pure (.) <*> pure app <*> pure app <*> a <*> b <*> c

 Профиль  
                  
 
 Re: Моноид в аппликативном функторе - моноид?
Сообщение17.10.2015, 01:13 


05/09/12
2587
arseniiv, большое спасибо, вы мне показали очевидные вещи, которые я до сего момента почему-то не замечал - левоассоциативность <*> приводит к очевидному
Используется синтаксис Haskell
a<*>b<*>c<*>d == (a<*>b)<*>c<*>d
из чего с применение упомянутого вами закона аппликативного функтора я получил тот же результат при раскрытии скобок. Второй вариант пока не раскрывал, но очень сильно подозреваю, что он раскроется в то же самое! Спасибо вам! Это именно то, что было надо! 8-)

-- 17.10.2015, 01:28 --

UPD мой первоначальный оптимизм немножко поутих, т.к. раскрытие выражения с правой скобкой пока приводит к несколько другому, более громоздкому, выражению, которое, впрочем, может быть эквивалентно требуемому. На первый взгляд выглядит очень похоже на трюк с
Используется синтаксис Haskell
($ a) . b == b a
, который потребовался для доказательства правой единицы.

-- 17.10.2015, 01:45 --

Второе выражение раскрывается в
Используется синтаксис Haskell
pc <*> pc <*> pc <*> pc <*> pc <*> pc <*> pc <*> pa <*> a <*> pa <*> b <*> c
app = mappend
pc = pure (.)
pa = pure app
 
, которое компилируется и выдает правильный результат :lol: Осталось его немножко редуцировать до удобоваримой формы :-)

 Профиль  
                  
 
 Re: Моноид в аппликативном функторе - моноид?
Сообщение17.10.2015, 02:10 
Заслуженный участник


27/04/09
28128
_Ivana в сообщении #1063572 писал(а):
Спасибо вам! Это именно то, что было надо! 8-)
Не за что! Надеюсь, оно действительно эквивалентно! :-)

А попробуйте собрать px <*> py <*> pz = pure (x y z), чего-то я зря не собрал у себя:

Используется синтаксис Haskell
[1] = pure (.) <*> pure (.) <*> pure (.) <*> pure app <*> pure app <*> a <*> b <*> c
[1] = pure ((.) (.) (.) app app) <*> a <*> b <*> c
[1] = pure ((.) . (.) app app) <*> a <*> b <*> c
[1] = pure (\a b c -> (a `app` b) `app` c) <*> a <*> b <*> c

Это даже выглядит весьма знакомо… :mrgreen:

 Профиль  
                  
 
 Re: Моноид в аппликативном функторе - моноид?
Сообщение17.10.2015, 02:15 


05/09/12
2587
Сборка трех точек и двух аппендов, когда все аргументы подряд и справа, действительно знакома. Я сейчас пытаюсь собрать свои 7 точек и 2 аппенда когда еще аргументы не подряд... Или не собирать а вашу первую форму привести к моей страшной или их обе привести к третьей еще более страшной, но одинаковой :-)

-- 17.10.2015, 02:23 --

arseniiv у меня есть онлайн-лямбдабот - он например мне редуцировал сейчас
Используется синтаксис Haskell
(((((((.) (.)) (.)) (.)) (.)) (.)) (.))
в
Используется синтаксис Haskell
(((.) . (.)) .)
- щас с ним попробую поиграться...

 Профиль  
                  
 
 Re: Моноид в аппликативном функторе - моноид?
Сообщение17.10.2015, 02:33 
Заслуженный участник


27/04/09
28128
Хм, а вот теперь мне уже во второй раз показалось, что может существовать функтор-контрпример такой, что образ моноида при нём хотя и будет моноидом (заменим a на pure a и ассоциативность получится сразу же), но все элементы — нет.

Как можно видеть, (c c c c c c c app) x f y z = app x (f y z), где c = (.), и чего-то я тоже не вижу, как x и f можно было бы поменять местами. Возможно, это нужное дополнительное ограничение на функтор. Или я плохо соображаю. (Ого, скоро утро. Конечно!)

-- Сб окт 17, 2015 04:35:55 --

_Ivana в сообщении #1063580 писал(а):
он например мне редуцировал сейчас
А ghci на что же? Я вот щас с TupleSections как летаю:

Используется синтаксис Haskell
> :t com com com com com com com (,)
com com com com com com com (,) :: a -> (a1 -> a2 -> b) -> a1 -> a2 -> (a, b)
> :set -XTupleSections
> com com com com com com com (1,,) '1' (2,,) '2' '3'
(1,'1',(2,'2','3'))

 Профиль  
                  
 
 Re: Моноид в аппликативном функторе - моноид?
Сообщение17.10.2015, 02:37 


05/09/12
2587
Мы с вами одновременно подобрались к одному и тому же. И я тоже пока не готов сказать, при каких условиях будет эквивалентность. Может всегда в теории, а может всегда в хаскеле, а может и там не всегда. Но мне интересен этот вопрос.

Либо уже ночь и я туплю, либо я таки поменял порядок и собрал все 3 аргумента подряд в конце :-) Привел к виду
Используется синтаксис Haskell
pc <*> p ($ a) <*> p (((((((c c) c) c) c) c) c) a) <*> x <*> y <*> z
и это компилируется и правильно считается! Мне кажется, мы на финишной прямой :-)

Последнее выражение (а значит и исходное с правой скобкой) привел к
Используется синтаксис Haskell
p ((. a) . (.) . a) <*> x <*> y <*> z
сейчас первое к нему если (надеюсь) приведу - то вроде пасьянс сойдется всегда в теории :-)

Или я опять ошибся, и это просто бесточечная нотация правого применения апенда - что и было в самом начале )....

 Профиль  
                  
 
 Re: Моноид в аппликативном функторе - моноид?
Сообщение17.10.2015, 03:09 
Заслуженный участник


27/04/09
28128
arseniiv в сообщении #1063582 писал(а):
функтор-контрпример
Никак не соображу, что от него требуется. Не перебирать же их. К тому же, не вижу никаких причин, почему он должен быть: какая разница, в каком порядке выполнять чистые действия? А порядок потенциально гразных a, …, c не меняется.

-- Сб окт 17, 2015 05:10:25 --

_Ivana в сообщении #1063583 писал(а):
сейчас первое к нему если (надеюсь) приведу - то вроде пасьянс сойдется всегда в теории :-)
О, покажьте потом магию. :-)

 Профиль  
                  
 
 Re: Моноид в аппликативном функторе - моноид?
Сообщение17.10.2015, 03:14 


05/09/12
2587
Моя магия оказалась шарлатанством - я с помощью законов функторов привел левую и правую порядки вычислений соответственно к
Используется синтаксис Haskell
p ((a .) . a) <*> x <*> y <*> z
p ((. a) . (.) . a) <*> x <*> y <*> z
, а это похоже те же наши левые/правые аппенды в бесточечной нотации...

-- 17.10.2015, 03:27 --

Я лохЪ! Это же свойства ВНУТРЕННЕГО моноида 8-) А он моноид и у него честная ассоциативность! И на нее мы опираемся, чтобы доказать ассоциативность внешнего - или я совсем отупел в пол-четвертого ночи :-) Или магия сошлась.

 Профиль  
                  
 
 Re: Моноид в аппликативном функторе - моноид?
Сообщение17.10.2015, 03:48 
Заслуженный участник


27/04/09
28128
Considered as left-to-right rewrite rules, the homomorphism, interchange, and composition laws actually constitute an algorithm for transforming any expression using pure and (<*>) into a canonical form with only a single use of pure at the very beginning and only left-nested occurrences of (<*>). Composition allows reassociating (<*>); interchange allows moving occurrences of pure leftwards; and homomorphism allows collapsing multiple adjacent occurrences of pure into one.
Я сейчас потому проверю ваш вывод. :-) [UPD: ага, не буду.]

-- Сб окт 17, 2015 05:50:40 --

_Ivana в сообщении #1063587 писал(а):
И на нее мы опираемся, чтобы доказать ассоциативность внешнего - или я совсем отупел в пол-четвертого ночи :-) Или магия сошлась.
А, и правда, если левые штуки совпадают. Я тоже вам на слово поверил. :-)

 Профиль  
                  
 
 Re: Моноид в аппликативном функторе - моноид?
Сообщение17.10.2015, 03:51 


05/09/12
2587
Я навскидку не понял что там написано, сейчас оформляю пошаговое доказательство аналогично первому посту... Как будет готово - выложу. Если в нем будут ошибки, интересно будет их увидеть :-)

 Профиль  
                  
 
 Re: Моноид в аппликативном функторе - моноид?
Сообщение17.10.2015, 03:58 
Заслуженный участник


27/04/09
28128
Надо просто вовремя применить zzz <*> pure g = pure ($ g) <*> zzz, если выдастся возможность. Это если вы будете повторять вывод с самого начала, с pa <*> a <*> (pa <*> b <*> c).

-- Сб окт 17, 2015 06:20:34 --

Всё сходится, подтверждаю!

Используется синтаксис Haskell
pa <*> a <*> (pa <*> b <*> c)
(pa <*> a) <*> ((pa <*> b) <*> c)
pc <*> (pa <*> a) <*> (pa <*> b) <*> c
pc <*> (pc <*> (pa <*> a)) <*> pa <*> b <*> c
pc <*> (pc <*> pc <*> pa <*> a) <*> pa <*> ...
pc <*> (p (c c app) <*> a) <*> pa <*> ...
pc <*> pc <*> p (c c app) <*> a <*> pa <*> ...
p (c c (c c app)) <*> a <*> pa <*> ...
p ($ app) <*> (p (c c (c c app)) <*> a) <*> ...
pc <*> p ($ app) <*> p (c c (c c app)) <*> a <*> ...
p (c ($ app)) <*> p (c c (c c app)) <*> ...
p ((c ($ app)) (c c (c c app))) <*> ...
[ghci] ((c ($ (,))) (c c (c c (,)))) 1 2 3 = (1,(2,3))
p (\a b c -> app a (app b c)) <*> ...
p (\a b c -> app (app a b) c) <*> ...

 Профиль  
                  
 
 Re: Моноид в аппликативном функторе - моноид?
Сообщение17.10.2015, 04:33 


05/09/12
2587
Не оптимизировал, просто аккуратно повторил весь путь преобразований полностью. Зато все сходится. Выдам себе шоколадную медаль :-) И вам тоже :D
код: [ скачать ] [ спрятать ]
Используется синтаксис Haskell
Моноид:
m1) mappend mempty = id
m2) mappend (mappend x y) z = mappend x (mappend y z)

Функтор:
f1) fmap id = id
f2) fmap (f . g) = fmap f . fmap g

Аппликативный функтор:
a1) pure f <*> pure x = pure (f x)
a2) u <*> pure y = pure ($ y) <*> u
a3) pure f <*> x = fmap f x
a4) pure (.) <*> u <*> v <*> w = u <*> (v <*> w)

Новый моноид:
1) mempty' = pure mempty
2) mappend' a b = fmap mappend a <*> b (mappend' = liftA2 mappend)

Левая единица:

mappend' mempty' x = (1,2)
fmap mappend (pure mempty) <*> x = (a3)
(pure mappend) <*> (pure mempty) <*> x = (a1)
pure (mappend mempty) <*> x = (a3)
fmap (mappend mempty) x = (m1)
fmap id x = (f1)
x

Правая единица:

mappend' x mempty' = (1,2)
fmap mappend x <*> (pure mempty) = (a2)
pure ($ mempty) <*> (fmap mappend x) = (a3)
fmap ($ mempty) (fmap mappend x) = (f2)
fmap ($ mempty . mappend) x =
fmap (mappend mempty) x = (m1)
fmap id x = (f1)
x

Ассоциативность бинарной операции:

Левый порядок:
mappend' (mappend' x y) z = (1,2)
fmap mappend (fmap mappend x <*> y) <*> z = (a3)
pure mappend <*> (pure mappend <*> x <*> y) <*> z = (a4)
pure (.) <*> pure mappend <*> (pure mappend <*> x) <*> y <*> z = (a4)
pure (.) <*> (pure (.) <*> pure mappend) <*> pure mappend <*> x <*> y <*> z = (a4)
pure (.) <*> pure (.) <*> pure (.) <*> pure mappend <*> pure mappend <*> x <*> y <*> z = (a1)
pure (((((.) (.)) (.)) mappend) mappend) <*> x <*> y <*> z = (lambdabot pl)
pure ((mappend .) . mappend) <*> x <*> y <*> z = (lambdabot unpl)
pure (\ x y z -> mappend (mappend x y) z) <*> x <*> y <*> z =
pure f <*> x <*> y <*> z where f = \ x y z -> mappend (mappend x y) z

Правый порядок:
mappend' x (mappend' y z) = (1,2)
fmap mappend x <*> (fmap mappend y <*> z) = (a3)
pure mappend <*> x <*> (pure mappend <*> y <*> z) = (a4)
pure (.) <*> (pure mappend <*> x) <*> (pure mappend <*> y) <*> z = (a4)
pure (.) <*> (pure (.) <*> (pure mappend <*> x)) <*> pure mappend <*> y <*> z = (a4)
pure (.) <*> pure (.) <*> pure (.) <*> (pure mappend <*> x) <*> pure mappend <*> y <*> z = (a4)
pure (.) <*> (pure (.) <*> pure (.) <*> pure (.)) <*> pure mappend <*> x <*> pure mappend <*> y <*> z = (a4)
pure (.) <*> pure (.) <*> (pure (.) <*> pure (.)) <*> pure (.) <*> pure mappend <*> x <*> pure mappend <*> y <*> z = (a4)
pure (.) <*> (pure (.) <*> pure (.)) <*> pure (.) <*> pure (.) <*> pure (.) <*> pure mappend <*> x <*> pure mappend <*> y <*> z = (a4)
pure (.) <*> pure (.) <*> pure (.) <*> pure (.) <*> pure (.) <*> pure (.) <*> pure (.) <*> pure mappend <*> x <*> pure mappend <*> y <*> z = (a1)
pure ((((((((.) (.)) (.)) (.)) (.)) (.)) (.)) mappend) <*> x <*> pure mappend <*> y <*> z = (a2)
pure ($ mappend) <*> (pure ((((((((.) (.)) (.)) (.)) (.)) (.)) (.)) mappend) <*> x) <*> y <*> z = (lambdabot pl)
pure ($ mappend) <*> (pure ((((.) . (.)) .) mappend) <*> x) <*> y <*> z = (a4)
pure (.) <*> pure ($ mappend) <*> pure ((((.) . (.)) .) mappend) <*> x <*> y <*> z = (lambdabot pl)
pure ((. mappend) . (.) . mappend) <*> x <*> y <*> z = (lambdabot unpl)
pure (\ x y z -> mappend x (mappend y z)) <*> x <*> y <*> z =
pure g <*> x <*> y <*> z where g = \ x y z -> mappend x (mappend y z)

f = g (m2) => ч.т.д.

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 19 ]  На страницу 1, 2  След.

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group