연관성, commutativity 등에 대한 함수를 자동적으로 결정 론적으로 테스트

Question

두 개의 인수의 또 다른 함수를 취하여 그 함수가 연관 적인지 여부를 결정하는 더 높은 차수 함수을 구성 할 수 있습니까?

비슷한 질문이지만 commutativity와 같은 다른 속성에 대해서도 마찬가지입니다.

불가능할 경우 모든 언어로 자동화 할 수있는 방법이 있습니까? Agda, Coq 또는 Prolog 솔루션이있는 경우 관심이 있습니다.

모든 가능한 인수 조합을 확인하고 종료하지 않는 무차별 대처법을 구상 할 수 있습니다. 그러나 "종료하지 마십시오"는 이러한 맥락에서 바람직하지 않은 자산입니다.

Answer 1

나는 하스켈이 그러한 것들에 적합하지 않다고 생각한다. 보통 당신은 수표와 완전히 정반대입니다. 당신은 당신의 객체가 어떤 속성들을 가지고 있다고 선언하므로 어떤 특별한 방법으로 사용될 수 있습니다 (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 

당신이 정말로 당신이 언급 한 증거 조수로도 볼 수도 증거 시스템을합니다. 프롤로그 - 논리적 인 언어이고 나는 그것도 매우 적합하다고 생각하지 않습니다. 하지만 간단한 비서 작성에 사용될 수 있습니다. 나는. 연관성 규칙을 적용하고 낮은 수준에서 평등을 도출하는 것이 불가능하다는 것을 확인하십시오.

Answer 2

내 마음에 오는 첫 번째 해결책은 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 

QuickCheck 무작위로 테스트 케이스를 선택으로 그것은 IO에서의로 정의 될 수있다 요구하고 있습니다.