Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
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)
}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment