Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Predicate Logic in Haskell

Tags:

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?

like image 499
wen Avatar asked Jul 12 '10 13:07

wen


People also ask

What is predicate in Haskell?

A predicate is a function of some value of type a to a Result , i.e. a Bool -like value with Okay as True and Fail as False , which carries additional data in each branch.

What is predicate logic example?

Example: P(x,y): “x + 2 = y” is a predicate. It has two variables x and y; Universe of Discourse: x is in {1,2,3}; y is in {4,5,6}. P(1,4) : 1 + 2 = 4 is a proposition (it is F); P(2,4) : 2 + 2 = 4 is a proposition (it is T);

What is predicate logic explain with example of Prolog?

Prolog is a programming language based on predicate logic. A Prolog program attempts to prove a goal, such as brother(Barney,x), from a set of facts and rules.


1 Answers

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.

like image 93
sdcvvc Avatar answered Sep 19 '22 06:09

sdcvvc