Tự động và xác định thử nghiệm một chức năng cho tính kết hợp, tính tương giao, vv

Question

Có thể xây dựng hàm bậc cao hơn isAssociative có chức năng khác của hai đối số và xác định xem hàm đó có liên kết không?

Câu hỏi tương tự nhưng đối với các thuộc tính khác chẳng hạn như tính tương giao.

Nếu điều này là không thể, có cách nào để tự động hóa nó bằng bất kỳ ngôn ngữ nào không? Nếu có một giải pháp Agda, Coq hoặc Prolog tôi quan tâm.

Tôi có thể hình dung giải pháp bạo lực kiểm tra mọi kết hợp đối số có thể có và không bao giờ chấm dứt. Nhưng "không bao giờ chấm dứt" là một tài sản không mong muốn trong bối cảnh này.

Answer 1

Tôi đoán Haskell không phù hợp với những thứ như vậy. Thông thường bạn hoàn toàn ngược lại để kiểm tra. Bạn tuyên bố rằng đối tượng của bạn có một số thuộc tính và do đó có thể được sử dụng theo một số cách đặc biệt (xem Data.Foldable). Đôi khi bạn có thể muốn quảng bá hệ thống của mình:

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 

Nếu bạn thực sự muốn có hệ thống chứng minh bạn có thể muốn xem xét những trợ lý chứng minh bạn đã đề cập. Prolog - là ngôn ngữ logic và tôi không nghĩ rằng nó cũng rất phù hợp với điều đó. Nhưng nó có thể được sử dụng để viết một số trợ lý đơn giản. I E. áp dụng quy tắc kết hợp và thấy rằng ở các cấp thấp hơn, không thể lấy được sự bình đẳng.

Answer 2

Giải pháp đầu tiên xuất hiện trong đầu tôi là sử dụng QuickCheck.

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

trong đó f là hàm chúng tôi đang thử nghiệm. Nó sẽ không chứng minh cả sự kết hợp lẫn tính giao hoán; nó chỉ đơn giản là cách đơn giản nhất để viết một giải pháp bạo lực bạn đã suy nghĩ. Lợi thế của QuickCheck là khả năng chọn các tham số của các bài kiểm tra mà hy vọng là các trường hợp góc cho mã thử nghiệm.

Một isAssociative bạn đang yêu cầu cho có thể được định nghĩa là

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 

Đó là trong IO như QuickCheck chọn trường hợp thử nghiệm bằng cách ngẫu nhiên.