Predicate Logic in Haskell

Question

I've been using the following data structure for the representation of propositional logic in Haskell:

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

Any comments on this structure are welcome.

However, now I want to extend my algoritms to handle FOL - predicate logic. What would be a good way of representing FOL in Haskell?

I've seen versions that are - pretty much - an extension of the above, and versions that are based on more classic context-free grammars. Is there any literature on this, that could be recommended?

Invert

Answer 1

This is known as higher-order abstract syntax.

First solution: Use Haskell's lambda. A datatype could look like:

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)

You can write a formula as:

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

This is described in detail in in The Monad Reader article. Highly recommended.

Second solution:

Use strings like

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)

Then you can write a formula like

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

The advantage is that you can show the formula easily (it's hard to show a Obj -> Prop function). The disadvantage is that you have to write changing names on collision (~alpha conversion) and substitution (~beta conversion). In both solutions, you can use GADT instead of two datatypes:

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

Third solution: Use numerals to represent where the variable is bound, where lower means deeper. For example, in ForAll (Exists (Equals (Num 0) (Num 1))) the first variable will bind to Exists, and second to ForAll. This is known as de Bruijn numerals. See I am not a number - I am a free variable.

Septempartite

I guess I have some reading to do.. thank you! I'll get back here after I finish the articles. – Invert

Just nitpicking, but it's still alpha conversion, even if it happens at substitution time. – Adornment

I believe the term "Higher-order abstract syntax" applies only to the first solution. Your answer seems to say the problem itself (or all three solutions) is known as HOAS. – Kierakieran

@dfeuer: I've fixed the link. – Septempartite

Answer 2

It seems appropriate to add an answer here to mention the functional pearl Using Circular Programs for Higher-Order Syntax, by Axelsson and Claessen, which was presented at ICFP 2013, and briefly described by Chiusano on his blog.

This solution neatly combines the neat usage of Haskell's syntax (@sdcvvc's first solution) with the ability to easily print formulas (@sdcvvc's second solution).

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

This solution would use a datatype such 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)

But allows you to write formulas as:

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

Invert