lógica de predicados en Haskell

Question

He estado usando la siguiente estructura de datos para la representación de la lógica proposicional en Haskell:

data Prop 
    = Pred String 
    | Not Prop 
    | And Prop Prop 
    | Or Prop Prop 
    | Impl Prop Prop 
    | Equiv Prop Prop 
    deriving (Eq, Ord) 

Cualquier comentario sobre esta estructura son bienvenidos.

Sin embargo, ahora quiero extender mis algoritmos para manejar FOL - lógica de predicado. ¿Cuál sería una buena manera de representar a FOL en Haskell?

He visto versiones que son, más o menos, una extensión de las anteriores y versiones basadas en gramáticas más libres de contexto. ¿Hay literatura sobre esto, que podría recomendarse?

Answer 1

Esto se conoce como higher-order abstract syntax.

Primera solución: Usa la lambda de Haskell. Un tipo de datos podría ser:

data Prop 
    = Not Prop 
    | And Prop Prop 
    | Or Prop Prop 
    | Impl Prop Prop 
    | Equiv Prop Prop 
    | Equals Obj Obj 
    | ForAll (Obj -> Prop) 
    | Exists (Obj -> Prop) 
    deriving (Eq, Ord) 

data Obj 
    = Num Integer 
    | Add Obj Obj 
    | Mul Obj Obj 
    deriving (Eq, Ord) 

Se puede escribir una fórmula como:

ForAll (\x -> Exists (\y -> Equals (Add x y) (Mul x y)))) 

Esto se describe en detalle en el artículo de The Monad Reader. Muy recomendable.

Segunda solución:

utilizar cadenas como

data Prop 
    = Not Prop 
    | And Prop Prop 
    | Or Prop Prop 
    | Impl Prop Prop 
    | Equiv Prop Prop 
    | Equals Obj Obj 
    | ForAll String Prop 
    | Exists String Prop 
    deriving (Eq, Ord) 

data Obj 
    = Num Integer 
    | Var String 
    | Add Obj Obj 
    | Mul Obj Obj 
    deriving (Eq, Ord) 

A continuación, puede escribir una fórmula como

ForAll "x" (Exists "y" (Equals (Add (Var "x") (Var "y"))) 
           (Mul (Var "x") (Var "y")))))) 

La ventaja es que se puede mostrar la fórmula fácilmente (es difícil para mostrar una función Obj -> Prop). La desventaja es que debe escribir el cambio de nombres en colisión (~ conversión alfa) y sustitución (~ conversión beta). En ambas soluciones, se puede utilizar GADT en lugar de dos tipos de datos:

data FOL a where 
    True :: FOL Bool 
    False :: FOL Bool 
    Not :: FOL Bool -> FOL Bool 
    And :: FOL Bool -> FOL Bool -> FOL Bool 
    ... 
    -- first solution 
    Exists :: (FOL Integer -> FOL Bool) -> FOL Bool 
    ForAll :: (FOL Integer -> FOL Bool) -> FOL Bool 
    -- second solution 
    Exists :: String -> FOL Bool -> FOL Bool 
    ForAll :: String -> FOL Bool -> FOL Bool 
    Var :: String -> FOL Integer 
    -- operations in the universe 
    Num :: Integer -> FOL Integer 
    Add :: FOL Integer -> FOL Integer -> FOL Integer 
    ... 

tercera solución: Use números para representar al que se dirige la variable, donde los medios más bajos profundos. Por ejemplo, en ForAll (Existe (Igual (Num 0) (Num 1))), la primera variable se vinculará a Exists, y la segunda a ForAll. Esto se conoce como numerales de Bruijn. Ver I am not a number - I am a free variable.

Answer 2

Parece apropiado agregar una respuesta aquí para mencionar la perla funcional Using Circular Programs for Higher-Order Syntax, por Axelsson y Claessen, que se presentó en ICFP 2013, y briefly described by Chiusano on his blog.

Esta solución combina perfectamente el uso ordenado de la sintaxis de Haskell (la primera solución de @ sdcvvc) con la capacidad de imprimir fórmulas fácilmente (la segunda solución de @ sdcvvc).

forAll :: (Prop -> Prop) -> Prop 
forAll f = ForAll n body 
    where body = f (Var n) 
     n = maxBV body + 1 

bot :: Name 
bot = 0 

-- Computes the maximum bound variable in the given expression 
maxBV :: Prop -> Name 
maxBV (Var _ ) = bot 
maxBV (App f a) = maxBV f `max` maxBV a 
maxBV (Lam n _) = n 

Esta solución sería utilizar un tipo de datos tales como:

data Prop 
    = Pred String [Name] 
    | Not Prop 
    | And Prop Prop 
    | Or  Prop Prop 
    | Impl Prop Prop 
    | Equiv Prop Prop 
    | ForAll Name Prop 
    deriving (Eq, Ord) 

Pero le permite escribir fórmulas como:

forAll (\x -> Pred "P" [x] `Impl` Pred "Q" [x])