Автоматическое и детерминированное тестирование функции на ассоциативность, коммутативность и т. Д. - PullRequest
Новая
       39

Автоматическое и детерминированное тестирование функции на ассоциативность, коммутативность и т. Д.

7 голосов
/ 28 декабря 2011

Можно ли построить функцию более высокого порядка isAssociative, которая принимает другую функцию из двух аргументов и определяет, является ли эта функция ассоциативной?

Аналогичный вопрос, но и для других свойств, таких как коммутативность.

Если это невозможно, есть ли способ автоматизировать его на каком-либо языке?Если есть интересующее меня решение Agda, Coq или Prolog.

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

Ответы [ 2 ]

9 голосов
/ 28 декабря 2011

Первое решение, которое приходит мне в голову, это использование QuickCheck . 

quickCheck $ \(x, y, z) -> f x (f y z) == f (f x y) z
quickCheck $ \(x, y) -> f x y == f y x

, где f - это функция, которую мы тестируем.Это не докажет ни ассоциативность, ни коммутативность;это просто самый простой способ написать решение о грубой силе, о котором вы думали.Преимущество QuickCheck в том, что он позволяет выбирать параметры тестов, которые, будем надеяться, будут угловыми для тестируемого кода.

isAssociative, который вы запрашиваете, можно определить как 

isAssociative
  :: (Arbitrary t, Show t, Eq t) => (t -> t -> t) -> IO ()
isAssociative f = quickCheck $ \(x, y, z) -> f x (f y z) == f (f x y) z

Он находится вIO, поскольку QuickCheck выбирает тестовые наборы случайным образом.

3 голосов
/ 28 декабря 2011

Думаю, Хаскелл не очень подходит для таких вещей. Обычно вы делаете абсолютно противоположную проверку. Вы заявляете, что ваш объект имеет некоторые свойства и, таким образом, может использоваться особым образом (см. Data.Foldable ). Иногда вы можете рекламировать свою систему: 

import Control.Parallel
import Data.Monoid

pmconcat :: Monoid a => [a] -> a
pmconcat [x] = x
pmconcat xs = pmconcat (pairs xs) where
    pairs [] = []
    pairs [x] = [x]
    pairs (x0 : x1 : xs') = y `par` (y : ys) where
        y = x0 `mappend` x1
        ys = pairs xs'

data SomeType

associativeSlowFold = undefined :: SomeType -> SomeType -> SomeType

data SlowFold = SlowFoldId
              | SlowFold { getSlowFold :: SomeType }

instance Monoid SlowFold where
    mempty = SlowFoldId
    SlowFoldId `mappend` x = x
    x `mappend` SlowFoldId = x
    x0 `mappend` x1 = SlowFold y where
        y = (getSlowFold x0) `associativeSlowFold` (getSlowFold x1)
    mconcat = pmconcat

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

...