Predicado de lógica en Haskell

data-structures context-free-grammar

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 es bienvenido.

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

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

Answer 1

Esto se conoce como sintaxis abstracta de orden superior .

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

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)

Puedes 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 The Monad Reader . Muy recomendable.

Segunda solución:

Use 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)

Entonces puedes escribir una fórmula como

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

La ventaja es que puede mostrar la fórmula fácilmente (es difícil 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, puede usar 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 los números para representar dónde está vinculada la variable, donde más baja significa más profunda. 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 que no soy un número, soy una variable gratuita .

Answer 2

Parece apropiado agregar aquí una respuesta para mencionar la perla funcional Utilizando programas circulares para la sintaxis de orden superior , por Axelsson y Claessen, que se presentó en ICFP 2013, y Chiusano describió brevemente en su 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 usaría un tipo de datos 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])