Почему это сжатое дерево выглядит так, как при использовании фильтра - PullRequest
Новая
       73

Почему это сжатое дерево выглядит так, как при использовании фильтра

0 голосов
/ 29 января 2019

Я пытаюсь понять, какой эффект оказывает фильтр в дереве сжатия генератора при использовании hedgehog встроенного сжатия .

Рассмотрим следующую функцию: 

{-# LANGUAGE OverloadedStrings #-}

import Hedgehog
import qualified Hedgehog.Gen as Gen

aFilteredchar:: Gen Char
aFilteredchar =
  Gen.filter (`elem` ("x" :: String)) (Gen.element "yx")

При печати усадочного дерева: 

>>>  Gen.printTree aFilteredchar

Я получу усадочные деревья, которые выглядят следующим образом: 

'x'
 └╼'x'
    └╼'x'
       └╼'x'
               ...

                   └╼<discard>

это очень глубокое деревосодержит только x и discard в конце.

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

Ответы [ 2 ]

0 голосов
/ 29 апреля 2019

Хотя подробный ответ Ли-яо Ся правильно описывает как это происходит, он не относится к почему ; почему перезапускает генератор после каждого сжатия?Ответ заключается в том, что это не должно;это ошибкаСм. Отчет об ошибке Улучшение фильтра на GitHub.

0 голосов
/ 29 января 2019

Gen - это, по сути, композиция монады вероятностей и древовидной монады, и наблюдаемое вами поведение в основном возникает из древовидной монады и определения Gen.filter.

По сути, Gen.filter p g - это простой монадический цикл, try 0 где: 

-- simplified body of filter
try k =
  if k > 100 then
    discard  -- empty tree
  else do
    x <- g
    if p x then
      pure x  -- singleton tree
    else
      try (k + 1)  -- keep looping

Таким образом, чтобы понять дерево, которое вы получили, вы должны понимать монаду дерева под нотацией do.

Монада дерева

Тип Tree для ежа , который внутренне используется Gen, выглядит примерно так (если вы смотрите на связанную реализацию в еже, установитеm ~ Maybe): 

data Tree a = Empty | Node a [Tree a]  -- node label and children

Существует много других Tree -подобных типов, которые являются монадами, и монадное связывание (>>=) обычно принимает форму подстановки деревьев.

Допустим, у вас есть дерево t = Node x [t1, t2, ...] :: Tree a и продолжение / замена k :: a -> Tree b, которое заменяет каждый узел / переменную x :: a на дерево k x :: Tree b.Мы можем описать t >>= k в два этапа, fmap, затем join, следующим образом.Сначала fmap применяет подстановку к каждой метке узла.Таким образом, мы получаем дерево, где каждый узел помечен другим деревом.Для конкретности, скажем k x = Node y [u1, u2, ...]: 

fmap k t
=
Node
  (k x)                        -- node label
  [fmap k t1, fmap k t2, ...]  -- node children
=
Node
  (Node y [u1, u2, ...])       -- node label
  [fmap k t1, fmap k t2, ...]  -- node children

Затем шаг join сглаживает структуру вложенного дерева, объединяя дочерние элементы изнутри метки с внешними: 

t >>= k
=
join (fmap k t)
=
Node
  y
  ([join (fmap k t1), join (fmap k t2), ...] ++ [u1, u2, ...])

завершите экземпляр Monad, обратите внимание, что у нас есть pure x = Node x [].

Цикл try

Теперь, когда у нас есть некоторая интуиция для монады дерева, мы можем обратиться к вашему конкретному генератору.Мы хотим оценить try k выше, где p = (== 'x') и g = elements "yx".Я машу здесь руками, но вы должны представить, что g оценивает случайным образом либо дерево Node 'y' [] (генерирует 'y' без усадок), иначе.pure 'y' или Node 'x' [Node 'y' []] (генерировать 'x' и сжиматься до 'y'; действительно, "elements сжимается влево"), и что каждое вхождение g не зависит от других, поэтому мы получаемдругой результат при повторной попытке.

Давайте рассмотрим каждый случай отдельно.Что будет, если g = pure 'y'?Предположим, k <= 100, что мы находимся в else ветви верхнего уровня if, уже упрощенной ниже: 

-- simplified body of filter
try k = do
    c <- pure 'y'     -- g = pure 'y'
    if c == 'x' then  -- p c = (c == 'x')
      pure c
    else
      try (k + 1)

-- since   (do c <- pure 'y' ; s c) = s 'y'  (monad law)   and   ('y' == 'x') = False

try k = try (k + 1)

Так что все времена, когда g оценивается как pure 'y', заканчиваютсяупростится как рекурсивный термин try (k + 1), и мы останемся со случаями, когда g оценивает другое дерево Node 'x' [Node 'y' []]: 

try k = do
  c <- Node 'x' [Node 'y' []]  -- g
  if c == 'x' then
    pure c
  else
    try (k + 1)

Как показано в предыдущем разделе, монадное связываниеэквивалентно следующему, и мы заканчиваем с некоторыми эквациональными рассуждениями. 

try k = join (Node (s 'x') [Node (s 'y') []])
  where
    s c = if c == 'x' then pure c else try (k + 1)

try k = join (Node (pure 'x') [Node (try (k + 1)) []])
try k = join (Node (pure 'x') [pure (try (k + 1))]  -- simplifying join
try k = Node 'x' [join (pure (try (k + 1)))]        -- join . pure = id
try k = Node 'x' [try (k + 1)]

В итоге, начиная с try 0, с половиной вероятности try k = try (k + 1) и с другой половиной try k = Node 'x' [try (k + 1)], наконец, мы остановимсяна try 100.Это объясняет дерево, которое вы наблюдаете. 

try 0 = Node 'x' [Node 'x' [ ... ]]  -- about 50 nodes

(Я полагаю, что это также дает хотя бы частичный ответ на ваш другой вопрос , поскольку это показывает, насколько сокращается Gen.filterчасто сводится к повторному запуску генератора с нуля.)

...