Probar automáticamente y determinísticamente una función para asociatividad, conmutatividad, etc.

Question

¿Es posible construir una función de orden superior isAssociative que adopta otra función de dos argumentos y determina si esa función es asociativa?

Pregunta similar pero para otras propiedades como la conmutatividad también.

Si esto es imposible, ¿hay alguna forma de automatizarlo en cualquier idioma? Si hay una solución Agda, Coq o Prolog, estoy interesado.

Puedo imaginar una solución de fuerza bruta que verifique todas las posibles combinaciones de argumentos y nunca termine. Pero "nunca termina" es una propiedad indeseable en este contexto.

Answer 1

Supongo que Haskell no es muy adecuado para este tipo de cosas. Por lo general, haces todo lo contrario al control. Usted declara que su objeto tiene algunas propiedades y, por lo tanto, podría usarse de alguna manera especial (consulte Data.Foldable). A veces es posible que desee promover su sistema:

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 

Si realmente quiere sistemas de pruebas que usted podría querer mirar también a los asistentes a prueba de que usted ha mencionado. Prolog - es un lenguaje lógico y no creo que también sea muy adecuado para eso. Pero podría usarse para escribir un asistente simple. Es decir. aplicar la regla de asociatividad y ver que a niveles más bajos es imposible derivar la igualdad.

Answer 2

La primera solución que me viene a la mente es usar QuickCheck.

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

donde f es una función que estamos probando. No demostrará ni la asociatividad ni la conmutatividad; es simplemente la forma más simple de escribir una solución de fuerza bruta en la que has estado pensando. La ventaja de QuickCheck es su capacidad para elegir los parámetros de las pruebas que, con suerte, serán casos de esquina para el código probado.

Un isAssociative que está pidiendo que podría definirse como

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 

Está en IO como QuickCheck opta por casos de prueba al azar.