búsqueda existencial y consulta sin el alboroto

Question

¿Existe una forma extensible y eficiente de escribir enunciados existenciales en Haskell sin implementar un lenguaje de programación lógica integrado? A menudo, cuando estoy poniendo en práctica algoritmos, quiero expresar declaraciones de primer orden existencialmente cuantificados como

∃x.∃y.x,y ∈ xs ∧ x ≠ y ∧ p x y 

donde ∈ está sobrecargado en las listas. Si estoy en un apuro, podría escribir código perspicaz que se parece a

find p []  = False 
find p (x:xs) = any (\y -> x /= y && (p x y || p y x)) xs || find p xs 

o

find p xs = or [ x /= y && (p x y || p y x) | x <- xs, y <- xs] 

Pero este enfoque no generaliza así a las preguntas valores o predicados o funciones de múltiples arities regresar . Por ejemplo, incluso una declaración simple como

∃x.∃y.x,y,z ∈ xs ∧ x ≠ y ≠ z ∧ f x y z = g x y z 

requiere escribir otro procedimiento de búsqueda. Y esto significa una cantidad considerable de código repetitivo. Por supuesto, lenguajes como Curry o Prolog que implementan estrechamiento o un motor de resolución permiten al programador escribir frases como:

find(p,xs,z) = x ∈ xs & y ∈ xs & x =/= y & f x y =:= g x y =:= z 

abusar de la notación considerablemente, lo que lleva a cabo tanto una búsqueda y devuelve un valor. Este problema surge a menudo cuando se implementan algoritmos formalmente especificados, y a menudo se resuelve mediante combinaciones de funciones como fmap, foldr y mapAccum, pero en su mayoría recursividad explícita. ¿Hay alguna manera más general y eficiente, o simplemente general y expresiva, de escribir código como este en Haskell?

Answer 1

Hay una transformación estándar que permite convertir

∃x ∈ xs : P 

a

exists (\x -> P) xs 

Si necesita para producir un testigo puede utilizar en lugar de findexists.

La verdadera molestia de hacer este tipo de abstracción en Haskell en lugar de un lenguaje lógico es que realmente debe pasar el "universo" set xs como parámetro. Creo que esto es lo que trae el "alboroto" al que se refiere en su título.

Por supuesto que puede, si lo prefiere, rellenar el conjunto universal (a través del cual está buscando) en una mónada. Luego puede definir sus propias versiones de exists o find para trabajar con el estado monádico. Para que sea eficiente, puede intentar Control.Monad.Logic, pero puede implicar romperse la cabeza contra los papeles de Oleg.

De todos modos, la codificación clásica consiste en reemplazar todas las construcciones de enlace, incluidos los cuantificadores existenciales y universales, con lambdas, y proceder con las llamadas de función apropiadas. Mi experiencia es que esta codificación funciona incluso para consultas anidadas complejas con mucha estructura, pero que siempre se siente torpe.

Answer 2

Tal vez no entiendo algo, pero ¿qué hay de malo con las listas de comprensión? Su segundo ejemplo se convierte en:

[(x,y,z) | x <- xs, y <- xs, z <- xs 
, x /= y && y /= z && x /= z 
, (p1 x y z) == (p2 x y z)] 

Esto le permite devolver valores; para verificar si la fórmula está satisfecha, solo use null (no evaluará más de lo necesario debido a la pereza).