Semantic Tableaux in Less than 90 Lines of Scala

This week challenge for me was to write a code that can check a propositional logic formula like
(¬(p ⋀ q) ↔ (¬p  ∨ ¬q)) ∧ ( ¬r ∧ q)  and check if the formula is valid or satisfiable. A formula is valid when it is always true under any interpretations of all its atoms. A formula is satisfiable when there is some interpretation of its atoms that can make the proposition true.

The complete code for this post is available here.

Semantic Tableaux
For example, p ⋀ q is satisfiable, since if p and q are both true, then the formula is true. (p  ∨ ¬p)  ⋀ (q ∨ ¬q) is valid, because regardless the interpretation of p and q, the formula is always true.

One way to implement the satisfiability and validity check is by creating truth table. But, the use of truth table is always exponential in number of atoms. There is fortunately a simple technique to check the validity and satisfiability a propositional logic formula. The technique is called Semantic Tableaux. I need to get my logic book I used back to the time of 2nd year of university (Ben-Ari, 1992 ) to remind me how it works. Basically, there are 9 rules, 5 α rules, and 4 β rules.

The following are the 9 rules:

α Rules

α	α1	α2
¬ ¬A	A
A1 ∧ A2	A1	A2
¬(A1 ∨ A2)	¬A1	¬A2
¬(A1 → A2)	A1	¬A2
(A1 ↔ A2)	A1 → A2	A2 → A1

β Rules

β	β1	β2
B1 ∨ B2	B1	B2
¬(B1 ∧ B2)	¬B1	¬B2
B1 → B2	¬B1	B2
¬(B1 ↔ B2)	¬(B1 → B2)	¬(B2 → B1)

I will not explain the Semantic Tableaux algorithms in detail. You can check a more detail in (Ben-Ari ) or in (Issawi, 92). Here is an example of tableau creation for ¬(p ⋀ q) ↔ (¬p  ∨ ¬q) :

Code 
Ok, let's start coding now.  The target is to have the following application working:

object Run { 
    def main(args:Array[String]):Unit = { 
      import Formulas._ 
      val formula1 = (¬('r) ∧ 'q) ∧ (¬('p ∧ 'q) ↔ (¬('p) ∨ ¬('q) )) 
      println(isSatisfiable(formula1) + "," + isValid(formula1)) // true, false 
 
      val formula2 = ¬('p ∧ 'q) ↔ (¬('p) ∨ ¬('q) ) 
      println(isSatisfiable(formula2) + "," + isValid(formula2)) // true, true 
    } 
  }

I used a sealed class Formula to represent all formulas. Atom, Conjunction, Disjunction, Implication, Equivalence, and Xor are classes that extends the trait. In addition, I introduced class  ¬ to represent the negation. Here is how it looks like.

sealed abstract class Formula  
case class Atom(symbol:Symbol) extends Formula 
case class Conjunction(p:Formula, q:Formula) extends Formula 
case class Disjunction(p:Formula, q:Formula) extends Formula 
case class Implication(p:Formula, q:Formula) extends Formula 
case class Equivalence(p:Formula, q:Formula) extends Formula 
case class Xor(p:Formula,q:Formula) extends Formula 
case class ¬(p:Formula) extends Formula

Note that Atom class takes a symbol as its property, so that it allows us to write Atom('p) for example.

I let the Formula class empty in the example above just to make the examples clear. The content of the class is actually the boolean operation to a formula, like ∧,∨, →, ↔, and ⊕. I benefit from Scala that allows special characters to be used as function name. Here is the class Formula looks like:

sealed abstract class Formula { 
  def ∧(q:Formula) = Conjunction(this, q) 
 
  def ∨(q:Formula) = Disjunction(this,q) 
 
  def →(q:Formula) = Implication(this,q) 
 
  def ↔(q:Formula) = Equivalence(this,q) 
 
  def ⊕(q:Formula) = Xor(this, q) 
}

With this, we can write(Atom('p) → Atom('q)) ∨ Atom(r). Not bad, but better to have directly ('p → 'q) ∨ r . For that purpose, implicit comes to rescue:

implicit def symbolToAtom(sym:Symbol) = Atom(sym)

We can now define how the validity and satisfiability work. This code illustrates the example of the application for testing our program:

object Run { 
    def main(args:Array[String]):Unit = { 
      import Formulas._ 
      val formula1 = (¬('r) ∧ 'q) ∧ (¬('p ∧ 'q) ↔ (¬('p) ∨ ¬('q) )) 
      println(isSatisfiable(formula1) + "," + isValid(formula1)) // true, false 
 
      val formula2 = ¬('p ∧ 'q) ↔ (¬('p) ∨ ¬('q) ) 
      println(isSatisfiable(formula2) + "," + isValid(formula2)) // true, true 
    } 
  }

Now let's see the implementation of the 9 rules (you remember 5 α rules, and 4 β rules ?). It's quite simple actually. An application of rule actually retuns a list of leaf, and a leaf is actually a list of formula. Here it is:

  type Leaf = Set[Formula] 
 
  def applyRule(f:Formula):List[Leaf] = 
    f match { 
      case f if isLiteral(f) => List(Set(f)) 
 
      case ¬(¬(a)) => List(Set(a)) 
 
      case Conjunction(a,b) => List(Set(a,b)) 
 
      case ¬(Disjunction(a,b)) => List(Set(¬(a), ¬(b))) 
 
      case ¬(Implication(a,b)) => List(Set(a, ¬(b))) 
 
      case Disjunction(a,b) => List(Set(a), Set(b)) 
 
      case ¬(Conjunction(a,b)) => List(Set(¬(a)), Set(¬(b))) 
 
      case (Implication(a,b)) => List(Set(¬(a)), Set(b)) 
 
      case Equivalence(a,b) => List( Set(a,b) , Set(¬(a), ¬(b))) 
 
      case ¬(Equivalence(a,b)) => List(Set(a,¬(b)),Set(¬(a), b)) 
  }

Nothing should be surprising except the case f if isLiteral(f) => List(Set(f)).  Just disregard this line at the moment, it's only useful in semantic tableau generation. Another surprise maybe for the equivalence rules.  The two equivalence rules in the code above are actually equivalent to the one in the rule table (leave as an exercise :-) ). Note how close the rules definition to its coding implementation. Isn't it nice ?

The most interesting part is of course the implementation of semantic tableau generation. In this naive implementation, the semantic tableau generation is embarrassingly simple, barely 10 lines of codes.

    def semanticTableau(f:Formula):List[Leaf] = { 
 
      def combine(rec:List[Leaf], f:Formula):List[Leaf] = 
               for ( a <- applyRule(f); b <- rec) yield (a ++ b) 
 
      def openLeaf(leaf:Leaf):List[Leaf] = 
        if (leaf forall isLiteral) 
          List(leaf) 
        else 
          leaf.foldLeft(List(Set.empty:Leaf))(combine) flatMap(openLeaf) 
 
      openLeaf(Set(f)) 
    }

Although short, the code is actually very dense. As you can see, the generation of semantic tableau above uses an auxiliary method openLeaf that does exactly that: opening a leaf. Opening a leaf is a recursive function that stops when all formulas in the leaf is a literal. A literal is either an atom or a negation of an atom. The else part is much more complex. But here is the idea: for each formula in a leaf, we apply one of the 9 rules defined above. The result of the application is combined using the combine function above. This will end up with a list of Leaf. For each leaf, then we recursively calls openLeaf using flatMap. This may be unclear, but try to play with the codes, hopefully it'll be clearer.

Finally, we need to implement validity and satisfiability check. A formula is f said to be valid if the semantic tableau for ¬f is closed. A semantic tableau is closed when all its leaves are closed, and finally a leaf is closed when it contains a formula in form of p and ¬p. Here is the implementation:

    def isClosedLeaf(f:Leaf):Boolean = 
      if (f.isEmpty) false 
      else { 
        (f.head match { 
           case Atom(_)    => f.tail.exists( _ == ¬(f.head)) 
           case ¬(Atom(a)) => f.tail.exists( _ == Atom(a)) 
           case _ => false 
         })  || isClosedLeaf(f.tail) 
      } 
 
    def isOpenLeaf(f:Leaf) = !isClosedLeaf(f) 
 
    def isValid(f:Formula):Boolean = semanticTableau(¬(f)) forall isClosedLeaf 
 
    def isSatisfiable(f:Formula):Boolean = semanticTableau(f) exists isOpenLeaf

We're done.

Summary
In this post, I showed my weekend hacking to implement naive satisfiability and validity checking of a propositional formula using semantic tableau. The implementation uses intensively Scala concepts like operator overriding, implicit, and fold and flatMap. All this concepts are helpful to implement the semantic tableaux techniques in relatively short Scala codes (less than 90 lines).  The use of operator helps readibility of the implementation (imagine how it looks like if I didn't use operators ∧,∨, →, ↔, and ⊕).

Reference
Ben-Ari, M (1992) Mathematical Logic for Computer Science. Prentice Hall.

Fix from Fold

My two previous posts, Fold Right from Fold Left and Folding Stream with Scala are actually my interpretation to (Hutton, 1999) paper. Now, I would like to continue with another paper (Pope, 2010 ?) that also talks about fold. Note that, Pope's work cites of  Hutton's work.

This post ends my fold trilogy. It has been an exciting and fun to play with.  I would love to continue with scalaz Fold (Foldr, Foldl, FoldMap Foldable are interesting), but I think I have to stop having fun :-)

Yet Another dropWhile Implementation

In Folding Stream with Scala , I implemented dropWhile using fold using (Hutton, 1999) paper. Pope proposes two more implementations, both work very well with infinite stream.

First, a reminder of fold implementation:

def foldr[A, B](combine:(A, =>B) => B, base:B)(xs:Stream[A]): B = { 
    if (xs.isEmpty) base 
    else combine(xs.head, foldr(combine, base)(xs.tail)) 
  } 

And here is the solution:

  def dwHo[A](pred:A=>Boolean, xs:Stream[A]):Stream[A]=>Stream[A] = { 
    val id =(s:Stream[A])=>s 
    val tail= (s:Stream[A])=>s.tail 
 
    def combine(next:A, rec: =>Stream[A]=>Stream[A]) = { 
     if (pred(next)) (rec compose tail) 
     else id 
    } 
    foldr(combine, id)(xs) 
  }

Example:

  scala> val xs = Stream.range(20, 120) 
  xs: scala.collection.immutable.Stream[Int] = Stream(20, ?) 
  scala> dwHo( (_:Int)<100, xs)(xs).toList 
  res33: List[Int] = List(100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119) 

It also works with infinite Stream:

scala> val ys = Stream.from(1) 
ys: scala.collection.immutable.Stream[Int] = Stream(1, ?) 
scala> dwHo( (_:Int)<5, ys)(ys).take(10).toList 
res38: List[Int] = List(5, 6, 7, 8, 9, 10, 11, 12, 13, 14)

Under the hood, here is what happen:

foldr combine id [1..] 
 =combine 1 (foldr combine id [2..]) = 
 =(foldr combine id [2..]) . tail 
 =(combine 2 (foldr combine id [3..]) . tail 
 =(foldr combine id [3..]) .tail . tail 
 =(combine 3 (foldr combine id [4..]) . tail . tail 
 =(foldr combine id [4..]) .tail . tail . tail 
 =(combine 4 (foldr combine id [5..]) . tail . tail . tail 
 =(foldr combine id [5..]) . tail . tail . tail . tail 
 =(combine 5 (foldr combine id [6..]) . tail . tail . tail 
 =id . tail . tail . tail . tail

And (id.tail.tail.tail.tail)[1..] = [5..].

Fix from Fold
The most interesting part of the (Pope, 2010) is not on dropWhile though, but on an implementation of a function using fold. The function is called fix, also known as Y combinator. Check this page to have an idea of what fix function is.

Basically, using fix, we can encode recursion function. The following is an example of factorial function using fix in haskell:

Prelude> :m Control.Monad.Fix 
Prelude Control.Monad.Fix> fix (\rec n -> if n == 0 then 1 else n * rec (n-1)) 5  

120
In Scala, fix function is implemented in a much trickier way. The difficulties come from the Scala strictness. Here is the implementation of fix I found after googling a little bit:

def fix[A](f: (A=>A)=>(A=>A)): A=>A = f(fix(f))(_)

Example:
scala> fix[Long](f=>x=> if (x == 0) 1 else x * f(x - 1))(5)

res5: Long = 120

One question that may arise is whether fold can be implemented using fix. Well, apparently, yes, after all, it's a recursion, but I haven't tried it yet. A more interesting question would be if fix can be implemented using fold. The answer is yes, and that's the essence of (Pope, 2010) article. Here is the implementation of fix using foldr in Scala:

def fix[A](f: (A=>A)=>(A=>A)): A=>A = { 
  def combine( a:(A=>A)=>(A=>A), b: =>A=>A):A=>A = f(b)(_) 
  foldr(combine, null)(Stream.continually(null)) 
}

Give a try:

scala> fix[Long](f=>x=> if (x == 0) 1 else x * f(x - 1))(5) 
res6: Long = 120

Youpi..., isn't it awesome? This shows how expressive fold is, since it can now be used to implement (any?) recursion functions.

References

• Hutton G (1999) A tutorial on the universality and expressiveness of fold. Available from http://www.cs.nott.ac.uk/~gmh/fold.pdf 

• Pope B (2010 ?)  Getting a Fix from the Right Fold. Available from: http://www.haskell.org/wikiupload/1/14/TMR-Issue6.pdf . There is one other dropWhile solution in this paper that I dumped here: https://gist.github.com/1195982.