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

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

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

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

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

2 7
haskell associativity halting-problem higher-order-functions

2 ответа:

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

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

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

3

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

9