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

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

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

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

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


higher-order-functions haskell commutativity halting-problem associativity
person TheIronKnuckle    schedule 28.12.2011    source источник
comment
Это зависит от: компактно ли пространство поиска?   -  person Daniel Wagner    schedule 28.12.2011

Ответы (2)


arrow_upward
3
arrow_downward

Я думаю, что Haskell не очень подходит для таких вещей. Обычно вы делаете все наоборот, чтобы проверить. Вы заявляете, что ваш объект имеет некоторые свойства и, следовательно, может использоваться каким-то особым образом (см. html" rel="nofollow">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

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

person ony    schedule 28.12.2011

arrow_upward
9
arrow_downward

Первое решение, которое приходит мне на ум, это использование 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 выбирает тестовые примеры случайным образом.

person Jan    schedule 28.12.2011
comment
Я не хочу проверять это эвристически, я хочу доказать это детерминистически. Это означает отсутствие случайных тестов. Тем не менее, я голосую за то, что познакомил меня с потрясающей функцией. Эта функция звучит как находка для модульных тестов. - person TheIronKnuckle; 29.12.2011