SKIEquivalence.scala

package skiequivalence

sealed trait SKIExpression {
  def convert:SKIExpression
  def freeVariables:Set[TermVariable]
}

case class TermVariable(variable:String) extends SKIExpression {
  override def convert = this
  override def freeVariables = Set(this)
  override def toString = variable
}
case class Application(fn:SKIExpression, arg:SKIExpression) extends SKIExpression {
  override def convert = Application(fn.convert, arg.convert)
  override def freeVariables = fn.freeVariables ++ arg.freeVariables
  override def toString = s"($fn $arg)"

}
case class Abstraction(variable:TermVariable, expression: SKIExpression) extends SKIExpression {
  override def convert = expression match {
    case bound:TermVariable if bound == variable => I
    case Application(fn, bound:TermVariable) if bound == variable => fn
    case term:SKIExpression if ! ((term freeVariables) contains variable) => Application(K,expression.convert)
    case Application(p,q) => Application(Application(S, Abstraction(variable,p).convert), Abstraction(variable, q).convert)
    case _:Abstraction => Abstraction(variable, expression.convert).convert
  }
  override def freeVariables = expression.freeVariables - variable
  override def toString = s"\\$variable . $expression"
}

case object S extends SKIExpression {
  override def convert = this
  override def freeVariables = Set.empty
  override def toString = "S"
}
case object K extends SKIExpression {
  override def convert = this
  override def freeVariables = Set.empty
  override def toString = "K"
}

case object I extends SKIExpression {
  override def convert = this
  override def freeVariables = Set.empty
  override def toString = "I"
}


object Equivalence {
  def main(args:Array[String]): Unit = {
    println(Abstraction(TermVariable("x"),
              Abstraction(TermVariable("y"),
                Abstraction(TermVariable("z"),Application(TermVariable("z"), TermVariable("x"))))).convert)
  }
}