CombinatoryLogic.scala

/**
  * The following is an implementation of Combinatory Logic as a scala DSL. It
  * is evaluated using head-first graph reduction, as described in "Compiling
  * Functional Languages" by Antoni Diller. This particular gist is adapted from
  * https://github.com/drivergroup/spn-combinatory-logic which I wrote for Scala
  * Puzzle Night, a meetup that I run occasionally. See the README.md in that
  * project for more information.
  *
  * The interesting bits of this are eval, reduce, and extract. The second half
  * of this file is a demonstration. It's written so as to be easy to `:paste`
  * in the Scala REPL. It has no external dependencies; you can save it to a new
  * directory and run it with `sbt run`.
  *
  * More Combinatory Logic Background:
  *  - https://en.wikipedia.org/wiki/SKI_combinator_calculus
  *  - http://people.cs.uchicago.edu/~odonnell/Teacher/Lectures/Formal_Organization_of_Knowledge/Examples/combinator_calculus/
  *  - http://www.cantab.net/users/antoni.diller/brackets/intro.html
  */
object comblogic {
  import annotation.tailrec

  /**
    * A Term is either an Atom or a Combination (*) of two atoms Atoms.
    * An Atom is either a VARiable representing a primitive
    * or a CONstant representing one of the various combinators.
    */
  sealed trait Term {
    def *(that: Term) = comblogic.*(this, that)

    /**
      * Given a term M and variable x, M.extract(x) returns a term Mp
      * not containing x such that (Mp * x) evaluates the same way as M
      */
    def extract(x: Var): Term = this match {
      case t: Term if !t.contains(x) => K * t
      case v: Var if v == x => I
      case t * (v: Var) if !t.contains(x) && (v == x) => t
      case l * r if !l.contains(x) && r.contains(x) => B * l * r.extract(x)
      case l * r if l.contains(x) && !r.contains(x) => C * l.extract(x) * r
      case l * r => S * l.extract(x) * r.extract(x)
    }

    def contains(x: Var): Boolean = this match {
      case a: Atom => a == x
      case (a * b) => a.contains(x) || b.contains(x)
    }

    private[comblogic] def appendTerms(terms: List[Term]): Term =
      terms.foldLeft(this)((acc, t) => acc * t)
  }

  sealed trait Atom extends Term
  sealed trait Con extends Atom
  case object S extends Con
  case object K extends Con
  case object I extends Con  // SKK
  case object B extends Con  // S(KS)K
  case object C extends Con  // S(BBS)(KK)
  case object Y extends Con  // AA where A =^= B(SI)(SII)

  case class Var(name: String) extends Atom {
    override def toString = name
  }

  type Combination = *
  case class *(left: Term, right: Term) extends Term {
    override def toString = this match {
      case p * (q * r) => s"$p(${q * r})"
      case _ => s"$left$right"
    }

    /**
      * Effects the reduction rules of the various combinators. A reducible
      * expression (a "redex") is a combinator followed by enough arguments for
      * that combinator's reduction rule to be applied.
      */
    def reduce: Term = this match {
      case I * p => p
      case K * p * q => p
      case B * p * q * r => p * (q * r)
      case C * p * q * r => p * r * q
      case S * p * q * r => p * r * (q * r)
      case Y * f => f * (Y * f)
      case ((left: Combination) * right) => left.reduce * right
      case nonRedex: Combination => nonRedex
    }
  }

  @tailrec // Evaluate a term by reducing its head repeatedly.
  def eval(t: Term, stack: List[Term] = Nil): Term = t match {
    case ((comb: Combination) * p * q * r) => eval(comb * p * q, r::stack)
    case ((c: Con)  * p * q * r) => eval((c * p * q * r).reduce, stack)
    case ((a: Atom) * p * q * r) => t.appendTerms(stack)
    case term: Term if stack.nonEmpty => eval(term * stack.head, stack.tail)
    case comb: Combination => {
      val reduced = comb.reduce
      if (reduced == comb) comb else eval(reduced)
    }
    case a: Atom => a
  }

  // Encode a function over Terms as a static Term
  def bracketAbstraction(f: Term => Term): Term = {
    val x = Var("variable")
    f(x).extract(x)
  }

  def bracketAbstraction(f: (Term, Term) => Term): Term = {
    val x = Var("variable-x")
    val y = Var("variable-y")
    f(x, y).extract(y).extract(x)
  }
}

object Demonstrations extends App {
  import comblogic._

  val p: Var = Var("p")
  val q: Var = Var("q")
  val r: Var = Var("r")
  val s: Var = Var("s")

  val leftParens = ((p * q) * r) * s
  val rightParens = p * (q * (r * s))
  val nested = p * p * (p * p * (q * r) * s * s) * s * s

  println
  println("toString:")
  println(List(leftParens, rightParens, nested).mkString("\n"))
  println

  println("Basic evaluation:")
  println(K*p*q + " evaluates to " + eval(K*p*q))
  println(S*p*q*r + " evaluates to " + eval(S*p*q*r))
  val long = S*(K*S)*K * (S*(K*S)*K * S) * (S*(K*S)*K) * K * (S*K*K) * S * s
  println(long + " evaluates to " + eval(long))
  assert(eval(long) == s)
  println

  println("Boolean operators in Combinatory Logic:")
  val TRUE: Term = K
  val FALSE: Term = K*I

  def not(p: Term) = p * FALSE * TRUE
  def and(p: Term, q: Term) = p * q * FALSE
  def or(p: Term, q: Term) = p * TRUE * q
  def xor(p: Term, q: Term) =
    not(
      or(and(p,q),
        and(not(p), not(q))))

  assert(eval(xor(TRUE, TRUE)) == FALSE)
  assert(eval(xor(TRUE, FALSE)) == TRUE)
  assert(eval(xor(FALSE, TRUE)) == TRUE)
  assert(eval(xor(FALSE, FALSE)) == FALSE)

  val NOT: Term = bracketAbstraction(not _)
  val AND: Term = bracketAbstraction(and _)
  val OR: Term = bracketAbstraction(or _)
  val XOR: Term = bracketAbstraction(xor _)

  assert(eval(XOR * TRUE * TRUE) == FALSE)
  assert(eval(XOR * TRUE * FALSE) == TRUE)
  assert(eval(XOR * FALSE * TRUE) == TRUE)
  assert(eval(XOR * FALSE * FALSE) == FALSE)

  println("NOT: " + NOT)
  println("AND: " + AND)
  println("OR:  " + OR)
  println("XOR: " + XOR)
  println

  println("Pay attention to the difference here.")
  println("`XOR` is a static term that can be applied to arbitrary terms.")
  println("`xor` returns a dynamically calculated term.")
  println("The former contains no variables. Observe the latter:")
  val x = Var("<variable-x>")
  val y = Var("<variable-y>")
  println("xor: " + xor(x, y))
  println
}