Skolemization

PropAst.scala

package logic

object PropAst {
  type Id = String
  sealed abstract class Term
  case class Const(name: Id) extends Term {
    override def toString = name
  }
  case class Var(name: Id) extends Term {
    override def toString = name
  }
  case class Fun(name: Id, args: List[Term]) extends Term {
    override def toString = name + (if (args.isEmpty) "" else "(" + args.mkString(",") + ")")
  }
  
  sealed abstract class Prop
  case class Pred(name: Id, args: List[Term]) extends Prop {
    override def toString = name + (if (args.isEmpty) "" else "(" + args.mkString(",") + ")")
  }
  case class All(x: Id, prop: Prop) extends Prop {
    override def toString = "forall " + x + ". " + prop.toString
  }
  case class Exist(x: Id, prop: Prop) extends Prop {
    override def toString = "exists " + x + ". " + prop.toString
  }
  case class Arrow(lhs: Prop, rhs: Prop) extends Prop {
    override def toString = lhs.toString + " -> " + rhs.toString
  }
  case class And(lhs: Prop, rhs: Prop) extends Prop {
    override def toString = lhs.toString + " and " + rhs.toString
  }
  case class Or(lhs: Prop, rhs: Prop) extends Prop {
    override def toString = lhs.toString + " or " + rhs.toString
  }
  case class Not(prop: Prop) extends Prop {
    override def toString = "not " + prop.toString
  }
}

PropParser.scala

package logic
import util.parsing.combinator._

object PropParser extends RegexParsers {
  import PropAst._
  
  lazy val id: Parser[Id] = """[a-zA-Z]+""".r
  lazy val pred: Parser[Prop] =
    (id ~ opt("(" ~ repsep(id, ",") ~ ")") ^^ {
      case name ~ Some("(" ~ args ~ ")") => Pred(name, args.map(Var.apply))
      case name ~ None => Pred(name, Nil)
    }) | "(" ~> quant <~ ")"
  lazy val quant: Parser[Prop] =
    rep("exists" ~ id <~ "." | "forall" ~ id <~ ".") ~ arrow ^^ {
      case Nil~prop => prop
      case xs~prop => xs.foldRight(prop){
        case ("exists" ~ v, prop) => Exist(v, prop)
        case ("forall" ~ v, prop) => All(v, prop)
      }
    }
  lazy val arrow: Parser[Prop] =
    repsep(and, "->") ^^ {
      case xs => xs.reduceLeft(Arrow.apply)
    }
  lazy val and: Parser[Prop] =
    repsep(or, "and") ^^ {
      case xs => xs.reduceLeft(And.apply)
    }
  lazy val or: Parser[Prop] =
    repsep(not, "or") ^^ {
      case xs => xs.reduceLeft(Or.apply)
    }
  lazy val not: Parser[Prop] =
    rep("not") ~ pred ^^ {
      case Nil~p => p
      case xs~p => xs.foldLeft(p)((p, _) => Not(p))
    }

  def parse(source: String) = parseAll(quant, source)
}

Skolemization.scala

package logic

object Skolemization {
  import PropAst._
  
  def subst(from: Term, to: Term, prop: Prop): Prop = 
    prop match {
      case Pred(name, args) =>
        Pred(name, args.map(arg => if (arg == from) to else arg))
      case All(x, prop) =>
        All(x, if (x == from) prop else subst(from, to, prop))
      case Exist(x, prop) =>
        Exist(x, if (x == from) prop else subst(from, to, prop))
      case Arrow(lhs, rhs) =>
        Arrow(subst(from, to, lhs), subst(from, to, rhs))
      case And(lhs, rhs) =>
        And(subst(from, to, lhs), subst(from, to, rhs))
      case Or(lhs, rhs) =>
        Or(subst(from, to, lhs), subst(from, to, rhs))
      case Not(prop) =>
        Not(subst(from, to, prop))
    }

  def freeVar(prop: Prop): List[Term] =
    prop match {
      case Pred(name, args) => args.collect { case v@Var(_) => v }
      case All(x, prop) => freeVar(prop).filterNot(Var(x) ==)
      case Exist(x, prop) => freeVar(prop).filterNot(Var(x) ==)
      case Arrow(lhs, rhs) => freeVar(lhs) ++ freeVar(rhs) distinct
      case And(lhs, rhs) => freeVar(lhs) ++ freeVar(rhs) distinct
      case Or(lhs, rhs) => freeVar(lhs) ++ freeVar(rhs) distinct
      case Not(prop) => freeVar(prop)
    }

  implicit def str2term(s: String): Term = Var(s)

  private def mkNameMaker(prefix: String) = {
    var count = BigInt(0)
    () => {
      count += 1
      prefix + count
    }
  }

  def closure(prop: Prop): Prop = {
    val fvs = freeVar(prop)
    fvs.foldRight(prop){
      case (Var(x), p) =>
        All(x, p)
      case _ =>
       sys.error("invalid variable")
    }
  }

  def prenex(prop: Prop): Prop = {
    val mkUniqVar = mkNameMaker("x")
    def isQuantified(prop: Prop) =
      prop match {
      case All(_, _) => true
      case Exist(_, _) => true
      case _ => false
    }
    def rec(prop: Prop): Prop = {
      def recOrId(props: Prop*): Prop => Prop = {
        if (props.exists(isQuantified)) rec _ else identity[Prop] _
      }
      prop match {
        case And(All(x, p1), p2)   =>
          val v = mkUniqVar()
          All(v, rec(And(subst(x, v, p1), p2)))
        case And(p1, All(x, p2))   =>
          rec(And(All(x, p2), p1))
        case And(Exist(x, p1), p2) =>
          val v = mkUniqVar()
          Exist(v, rec(And(subst(x, v, p1), p2)))
        case And(p1, Exist(x, p2)) =>
          rec(And(Exist(x, p2), p1))
        
        case Or(All(x, p1), p2)   =>
          val v = mkUniqVar()
          All(v, rec(Or(subst(x, v, p1), p2)))
        case Or(p1, All(x, p2))   =>
          rec(Or(All(x, p2), p1))
        case Or(Exist(x, p1), p2) =>
          val v = mkUniqVar()
          Exist(v, rec(Or(subst(x, v, p1), p2)))
        case Or(p1, Exist(x, p2)) =>
          rec(Or(Exist(x, p2), p1))

        case Not(All(x, p))   =>
          val v = mkUniqVar()
          Exist(v, rec(Not(subst(x, v, p))))
        case Not(Exist(x, p)) =>
          val v = mkUniqVar()
          All(v, rec(Not(subst(x, v, p))))
        
        case Arrow(lhs, All(x, rhs))   =>
          val v = mkUniqVar()
          All(v, rec(Arrow(lhs, subst(x, v, rhs))))
        case Arrow(All(x, lhs), rhs)   =>
          val v = mkUniqVar()
          Exist(v, rec(Arrow(subst(x, v, lhs), rhs)))
        case Arrow(lhs, Exist(x, rhs)) =>
          val v = mkUniqVar()
          Exist(v, rec(Arrow(lhs, subst(x, v, rhs))))
        case Arrow(Exist(x, lhs), rhs) =>
          val v = mkUniqVar()
          All(v, rec(Arrow(subst(x, v, lhs), rhs)))

        case All(x, p) => All(x, rec(p))
        case Exist(x, p) => Exist(x, rec(p))
        case Pred(_, _) =>
          prop
        case And(p1, p2) =>
          val _p1 = rec(p1)
          val _p2 = rec(p2)
          recOrId(_p1, _p2)(And(_p1, _p2))
        case Or(p1, p2) =>
          val _p1 = rec(p1)
          val _p2 = rec(p2)
          recOrId(_p1, _p2)(Or(_p1, _p2))
        case Arrow(p1, p2) =>
          val _p1 = rec(p1)
          val _p2 = rec(p2)
          recOrId(_p1, _p2)(Arrow(_p1, _p2))
        case Not(p) =>
          val _p = rec(p)
          recOrId(_p)(Not(_p))
        
      }
    }
    rec(prop)
  }

  def skolemization(prop: Prop): Prop = {
    val mkUniqC = mkNameMaker("c")
    val mkUniqF = mkNameMaker("f")
    def rec(prop: Prop, vars: List[Term]): Prop = {
      prop match {
        case All(x, p) =>
          if (vars.isEmpty) rec(subst(Var(x), Const(mkUniqC()), p), Nil)
          else rec(subst(Var(x), Fun(mkUniqF(), vars), p), Nil)
        case Exist(x, p) =>
          Exist(x, rec(p, x :: vars))
        case _ => prop
      }
    }
    rec(prop, Nil)
  }

  def apply(s: String) = skolemization(prenex(closure(PropParser.parse(s).get)))
}