Skip to content

Instantly share code, notes, and snippets.

@bakenezumi
Last active September 25, 2019 00:46
Show Gist options
  • Save bakenezumi/195ae3bcae81c1006cb48bb683c8b115 to your computer and use it in GitHub Desktop.
Save bakenezumi/195ae3bcae81c1006cb48bb683c8b115 to your computer and use it in GitHub Desktop.
sealed trait Term
case class TmVar(value: Any) extends Term {
override def toString: String = s"$value"
}
case class TmAbs(x: Term, t: Term) extends Term {
override def toString: String = s"λ($x.$t)"
}
case class TmApply(t1: Term, t2: Term) extends Term {
override def toString: String = s"($t1 $t2)"
}
def lambda(xs: Term*) =
xs.init.init.foldRight(TmAbs(xs.init.last, xs.last))(TmAbs(_, _))
def apply(xs: Term*) =
xs.tail.tail.foldLeft(TmApply(xs.head, xs.tail.head))(TmApply(_, _))
implicit class RichTerm(self: Term) {
def apply(that: => Term): Term = {
TmApply(self, that)
}
def eval(): Term = {
evalFunction(self)
}
}
// substitution [x |-> s]t defined in TaPL p. 54 - 5.3.4
def substitution(x: Term, t: Term, s: Term): Term = {
println(s" [$x |-> $s]$t")
val ret = t match {
case y if x == y => s
case TmAbs(y, t1) if x != y => TmAbs(y, substitution(x, t1, s))
case y @ TmApply(t1, t2) if x != y /* && y ∉ FV(s) 捕獲回避代入が必要だが未実装のため問題によってはバグる(6章参照)*/ =>
TmApply(substitution(x, t1, s), substitution(x, t2, s))
case TmVar(y: String) if x.isInstanceOf[TmVar] && s.isInstanceOf[TmVar] =>
// for realnat
TmVar(
y.replaceAll(x.asInstanceOf[TmVar].value.toString,
s.asInstanceOf[TmVar].value.toString))
case y => y
}
println(s" $ret")
ret
}
def evalOne(t: Term): Term = {
println(t)
t match {
case TmApply(t1, t2) if evalOne(t1) != t1 =>
println("E-APP1")
TmApply(evalOne(t1), t2) // E-APP1
case TmApply(v1: TmAbs, t2) if evalOne(t2) != t2 =>
println("E-APP2")
TmApply(v1, evalOne(t2)) // E-APP2
case TmApply(lambda: TmAbs, v: Term) =>
println("E-APPABS")
substitution(lambda.x, lambda.t, v) // E-APPABS
case _ => t
}
}
def eval(t: Term): Term = {
val t_ = evalOne(t)
if (t_ == t) t else eval(t_)
}
val evalFunction = eval _
// variables used in companion object
val x = TmVar("x")
val y = TmVar("y")
val z = TmVar("z")
val a = TmVar("a")
val b = TmVar("b")
val c = TmVar("c")
val d = TmVar("d")
val p = TmVar("p")
val f = TmVar("f")
val m = TmVar("m")
val n = TmVar("n")
val t = TmVar("t")
// if-else
val tru = lambda(x, y, x)
val fls = lambda(x, y, y)
val test = lambda(b, m, n, b(m)(n))
// pair
val pair = lambda(a, b, x, test(x)(a)(b))
val fst = lambda(p, p(tru))
val snd = lambda(p, p(fls))
// charch number
val s = TmVar("s")
val c0 = lambda(s, z, z)
val c1 = lambda(s, z, s(z))
val c2 = lambda(s, z, s(s(z)))
val c3 = lambda(s, z, s(s(s(z))))
def realnat(charch: Term) = {
val expr = eval(charch(lambda(x, TmVar("x + 1")))(TmVar("0")))
println(s"expr: $expr")
val scriptManager = new javax.script.ScriptEngineManager
val engine = scriptManager.getEngineByName("js")
engine.eval(expr.toString)
}
val succ = lambda(n, s, z, s(n(s)(z)))
val plus = lambda(n, m, s, z, n(s)(m(s)(z)))
val times = lambda(n, m, n(plus(m))(c0))
//λn.λs.λz.n (λx.λy. y (x s)) (λx.z) (λx.x)
val pred =
lambda(n,
s,
z,
n(lambda(x, lambda(y, y(x(s)))))(lambda(x, z))(lambda(x, x)))
// Y = λf.(λx.f (x x)) (λx.f (x x))
val Y = lambda(f, lambda(x, f(x)(x))(lambda(x, f(x)(x))))
// Z = λf.(λx.f (λy.x x y)) (λx.f (λy.x x y))
val Z = lambda(
f,
lambda(x, f(lambda(y, x(x)(y))))(lambda(x, f(lambda(y, x(x)(y))))))
val iszero = lambda(x, x(lambda(y, fls))(tru))
val fct = Z(
lambda(f, lambda(x, test(iszero(pred(x)))(c1)(times(x)(f(pred(x)))))))
//
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment