Explanation and Implementation of the Lambda Calculus using Scala

lambdacalculus.scala

package lambdacalculus

/**
  * Abstract Syntax (AST) for lambda terms
  *
  * In the simplest form of lambda calculus, terms are built using only the following rules:
  *
  * Variable (x)
  *   A character or string representing a parameter.
  * Abstraction (λx.M)
  *   Function definition (M is a lambda term). The variable x becomes bound in the expression.
  * Application (M N)
  *   Applying a function to an argument. M and N are lambda terms.
  */
sealed trait Term
case class Var(name: Symbol) extends Term
case class Lambda(param: Var, body: Term) extends Term
case class Apply(left: Term, right: Term) extends Term

object Interpreter {

  /**
    * The set of free variables of a lambda expression, M, is denoted as FV(M) and is defined
    * by recursion on the structure of the terms, as follows:
    *
    * FV(x) = {x}, where x is a variable
    * FV(λx.M) = FV(M) \ {x}
    * FV(M N) = FV(M) ∪ FV(N)
    */
  def fv(e: Term): Set[Var] = e match {
    case v: Var => Set(v)
    case Lambda(p, b) => fv(b) diff Set(p)
    case Apply(l, r) => fv(l) union fv(r)
  }

  // combinator to check whether a variable `v` is free in lambda term `e`
  def hasFv(e: Term, v: Var): Boolean = fv(e).contains(v)

  /**
    * Substitution, written E[V := R], is the process of replacing all free
    * occurrences of the variable V in the expression E with expression R.
    *
    * x[x := N]       ≡ N
    * y[x := N]       ≡ y, if x ≠ y
    * (M1 M2)[x := N] ≡ (M1[x := N]) (M2[x := N])
    * (λx.M)[x := N]  ≡ λx.M
    * (λy.M)[x := N]  ≡ λy.(M[x := N]), if x ≠ y, provided y ∉ FV(N)
    */
  def subst(E: Term, V: Var, R: Term): Term = E match {
    case _: Var if E == V => R
    case Lambda(p, b) if !hasFv(R, p) && p != V =>
      Lambda(p, subst(b, V, R))
    case Lambda(p, _) if p != V => subst(alpha(E), V, R)             // uses α-conversion
    case Apply(l, r) => Apply(subst(l, V, R), subst(r, V, R))
    case _ => E
  }

  // variable renaming - naive implementation
  private val rename: Var => Var = {
    var i = 0
    v: Var => {
      i += 1
      Var(Symbol(s"${v.name.name}${i}"))
    }
  }

  /**
    * α-conversion - renaming the bound (formal) variables in the expression. Used to avoid name collisions.
    *
    * (λx.M[x]) → (λy.M[y])
    */
  def alpha(e: Term): Term = {
    e match {
      case Lambda(p, b) =>
        val p1 = rename(p)
        Lambda(p1, subst(b, p, p1))
      case _ => e
    }
  }

  /**
    * β-reduction - replacing the bound variable with the argument expression in the body of the abstraction.
    * ((λx.M) E) → (M[x:=E])
    *
    * η-conversion - two functions are the same if and only if they give the same result for all arguments
    * (λx.Mx) → (M) when M does not contain x free
    */
  def reduce(e: Term): Term = {

    /**
      * check if lambda term `e` is reducible or not
      */
    def reducible(e: Term): Boolean = e match {
      case Apply(_: Var, _) => false                                 // if left is variable, already reduced form
      case _: Var => false                                           // variable is already reduced form
      case _ => true                                                 // everything else is reducible
    }

    e match {
      case Lambda(x1, Apply(m, x2)) if !hasFv(m, x1) && x1 == x2 =>  // uses η-conversion
        reduce(m)
      case Apply(Lambda(p, b), a) =>                                 // function application
        reduce(subst(b, p, reduce(a)))
      case Apply(l, r) if reducible(l) || reducible(r) =>            // if one of them is reducible, reduce both
        reduce(Apply(reduce(l), reduce(r)))                          // and reduce whole lambda term again
      case _ => e                                                    // reduced form
    }
  }
}

object Compiler {

  /**
    * compile lambda term (AST) to lambda notation
    * @param e lambda term
    * @return string as lambda notation
    */
  def notation(e: Term): String = e match {
    case Var(s) => s.name
    case Lambda(p, b) => s"λ${p.name.name}.${notation(b)}"
    case Apply(l, r) => s"(${notation(l)})(${notation(r)})"
    case _ => "unknown lambda terms"
  }

  /**
    * compile lambda term (AST) to scheme code
    * @param e lambda term
    * @return string as scheme code
    */
  def scheme(e: Term): String = e match {
    case Var(s) => s.name
    case Lambda(p, b) => s"(lambda (${p.name.name}) ${scheme(b)})"
    case Apply(l, r) => s"(${scheme(l)} ${scheme(r)})"
    case _ => "unknown lambda terms"
  }

  /**
    * compile lambda term (AST) to javascript code
    * @param e lambda term
    * @return string as javascript code
    */
  def javascript(e: Term): String = e match {
    case Var(s) => s.name
    case Lambda(p, b) => s"function (${p.name.name}) { return ${javascript(b)} }"
    case Apply(l, r) => s"${javascript(l)}(${javascript(r)})"
    case _ => "unknown lambda terms"
  }

  /**
    * compile lambda term (AST) to ruby code
    * @param e lambda term
    * @return string as ruby code
    */
  def ruby(e: Term): String = e match {
    case Var(s) => s.name
    case Lambda(p, b) => s"-> ${p.name.name} { ${ruby(b)} }"
    case Apply(l, r) => s"${ruby(l)}[${ruby(r)}]"
    case _ => "unknown lambda terms"
  }
}

object Expression {
  val x = Var('x)
  val y = Var('y)
  val z = Var('z)
  val m = Var('m)
  val n = Var('n)
  val f = Var('f)

  val id = Lambda(x, x)
  val free = Lambda(x, y)

  val zero = Lambda(f, Lambda(x, x))
  val one = Lambda(f, Lambda(x, Apply(f, x)))

  val inc = Lambda(n, Lambda(f, Lambda(x, Apply(f, Apply(Apply(n, f), x)))))
  val add = Lambda(m, Lambda(n, Apply(Apply(n, inc), m)))

  val e1 = Apply(Apply(one, id), z)
  val e2 = Lambda(x, Apply(f, x))

  val un = Lambda(x, Apply(Lambda(x, Apply(f, x)), x))
}

object Demo extends App {

  import Interpreter._
  import Compiler._
  import Expression._

  val two = Apply(Apply(add, one), one)                              // adding one and one
  val reducedTwo = reduce(two)                                       // reduced form

  assert(notation(two) == "((λm.λn.((n)(λn.λf.λx.(f)(((n)(f))(x))))(m))(λf.λx.(f)(x)))(λf.λx.(f)(x))")
  assert(notation(reducedTwo) == "λf.λx.(f)(((λf.λx.(f)(x))(f))(x))")

  assert(scheme(reducedTwo) == "(lambda (f) (lambda (x) (f (((lambda (f) (lambda (x) (f x))) f) x))))")
  assert(javascript(reducedTwo) ==
    "function (f) { return function (x) { return f(function (f) { return function (x) { return f(x) } }(f)(x)) } }")
  assert(ruby(reducedTwo) == "-> f { -> x { f[-> f { -> x { f[x] } }[f][x]] } }")

  val inc = Var('inc)                                                // assume `inc` is increment function
  val zero = Var('zero)                                              // assume `zero` is decimal number
  val two1 = Apply(Apply(reducedTwo, inc), zero)                     // applying `inc` twice to `zero`
  val reducedTwo1 = reduce(two1)                                     // reduced form

  assert(notation(two1) == "((λf.λx.(f)(((λf.λx.(f)(x))(f))(x)))(inc))(zero)")
  assert(notation(reducedTwo1) == "(inc)((inc)(zero))")

  assert(scheme(reducedTwo1) == "(inc (inc zero))")
  assert(javascript(reducedTwo1) == "inc(inc(zero))")
  assert(ruby(reducedTwo1) == "inc[inc[zero]]")

  assert(notation(free) == "λx.y")
  // λx.y[y := x]
  assert(notation(subst(free, y, x)) == "λx1.x", "it uses α-conversion to perform capture avoiding substitution")
}