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