TypeLessLambda.sc

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)))))))

//