Prädikatenlogik in Haskell

Question

Ich habe für die Darstellung der Aussagenlogik in Haskell folgende Datenstruktur unter Verwendung von:

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

Alle Kommentare zu dieser Struktur sind willkommen.

Allerdings möchte ich jetzt meine Algorithmen erweitern, um FOL - Prädikatenlogik zu behandeln. Was wäre eine gute Möglichkeit, FOL in Haskell zu repräsentieren?

Ich habe Versionen gesehen, die - ziemlich - eine Erweiterung des oben genannten sind, und Versionen, die auf mehr klassischen kontextfreien Grammatiken basieren. Gibt es dazu Literatur, die empfohlen werden könnte?

Answer 1

Dies ist bekannt als higher-order abstract syntax.

Erste Lösung: Verwenden Sie Haskells Lambda. Ein Datentyp könnte wie folgt aussehen:

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) 

Sie eine Formel schreiben können wie:

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

Dies in The Monad Reader Artikel im Detail beschrieben wird. Sehr empfehlenswert.

Zweite Lösung:

Verwenden Strings wie

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) 

Dann Sie eine Formel wie

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

Der Vorteil schreiben kann, ist, dass Sie die Formel leicht zeigen können (es ist schwer, um eine Obj -> Prop Funktion anzuzeigen). Der Nachteil ist, dass Sie Namen bei Kollision (~ Alpha-Konvertierung) und Substitution (~ Beta-Konvertierung) schreiben müssen.

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

Dritte Lösung: Verwenden Sie Ziffern darzustellen, wo die Variable gebunden ist, in denen geringere Mittel tiefer in beiden Lösungen können Sie GADT anstelle von zwei Datentypen verwenden. Zum Beispiel wird in ForAll (Exists (Equals (Num 0) (Num 1))) die erste Variable an Exists gebunden, und an ForAll. Dies ist bekannt als de Bruijn Ziffern. Siehe I am not a number - I am a free variable.

Answer 2

Es scheint angebracht, hier eine Antwort hinzuzufügen, um die funktionelle Perle Using Circular Programs for Higher-Order Syntax von Axelsson und Claessen zu erwähnen, die auf der ICFP 2013 vorgestellt wurde, und briefly described by Chiusano on his blog.

Diese Lösung kombiniert die saubere Verwendung der Haskell-Syntax (@ sdcvvc's erste Lösung) mit der Möglichkeit, Formeln einfach zu drucken (@ sdcvvc's zweite Lösung).

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 

Diese Lösung einen Datentyp wie verwenden würde:

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) 

Aber können Sie Formeln wie schreiben:

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