Lógica de Predicados en Haskell

Question

Lógica de Predicados en Haskell

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 la lógica de predicados FOL. ¿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 lo anterior, y versiones que se basan en gramáticas más clásicas libres de contexto. Hay alguna literatura sobre esto, que podría ser recomendado?

25

data-structures haskell context-free-grammar first-order-logic

Author: wen, 2010-07-12

Source

2 answers

Parece apropiado agregar una respuesta aquí para mencionar la perla funcional Usando Programas Circulares para Sintaxis de Orden Superior, por Axelsson y Claessen, que fue presentada en ICFP 2013, y brevemente descrita por Chiusano en su blog.

Esta solución combina perfectamente el uso ordenado de la sintaxis de Haskell (primera solución de@sdcvvc) con la capacidad de imprimir fórmulas fácilmente (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 as:

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

4

Author: wen,
Warning: date(): Invalid date.timezone value 'Europe/Kyiv', we selected the timezone 'UTC' for now. in /var/www/agent_stack/data/www/ajaxhispano.com/template/agent.layouts/content.php on line 61
2015-03-28 12:49:28

score 29 · Accepted Answer

Esto se conoce como sintaxis abstracta de orden superior.

Primera solución: Use la lambda de Haskell. Un tipo de datos podría verse como:

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

Segunda solución:

Utilice 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 tienes que escribir nombres cambiantes 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 : Utilice números para representar dónde está limitada la variable, donde menor significa más profundo. Por ejemplo, en ForAll (Exists (Equals (Num 0) (Num 1))) la primera variable se unirá a Exists, y la segunda a ForAll. Esto se conoce como de Bruijn numerals. Ver No soy un número - soy una variable libre .