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

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

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

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

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