Implementing Primitives with Lambda

This article is part-02.2 of the series A Quick Taste of Programming Languages in my blog.

The series is tend to discuss some basic concepts in PL theory and their implementation from a beginner’s perspective. I use Scala code for demonstrations since I’m currently learning it.

The full list of code in this article can be found here. It’s released under the MIT license.

(almost) Anything could be lambda #

Programming languages offer various elements and features to enable programmers describing their problems effectively. You may notice that although I claimed lambda calculus as a universal language, it seems to lack many primitives that other programming languages own, such as natural numbers and conditional test. Well, that’s because lambda doesn’t need to.

Believe it or not, with its own terms (names, functions and applications) and evaluation rules, lambda calculus is already capable of expressing almost all elements and features in a modern programming language. In this article, we are going to play with some basic ones.

Multiple arguments #

Lambda functions only take single argument. This doesn’t effect the expressive ability of lambda calculus because it has been proved that functions with multiple arguments are equivalent to nested functions. This is called currying.

For example say, we want to define a function with two arguments like: $$ λxy.(xy) $$

It’s equivalent to a nested function in lambda calculus: $$ λx.(λy.(xy)) $$ From now on we will use abbreviations like $λxy.(xy)$ to represent functions with multiple arguments.

Natural number #

Definition #

The only way to “implement” something in lambda calculus is to define new functions.

We regard natural numbers as a sequence of elements abiding by arithmetical rules. To represent such sequence in lambda calculus, we need to define the first element of the sequence, zero, and a successor function, which takes an element of the sequence as input and returns the next element of the input.

A possible way to do this is to define zero as: $$ 0\ \equiv λs.(λz.z) $$ The successor function can be defined as: $$ S\ \equiv λwyx.y(wyx) $$ Now we have $$ \begin{align*} 1\ &\equiv\ S0\ \equiv\ λs.(λz.s(z)) \newline 2\ &\equiv\ S1\ \equiv\ λs.(λz.s(s(z)) \newline 3\ &\equiv\ S2\ \equiv\ λs.(λz.s(s(s(z))) \newline &… \ … \end{align*} $$

You can easily verify these using the lambda interpreter we implemented in the last chapter:

val ZERO = lambda_Function("s", lambda_Function("z", lambda_Name("z")))
val S = {
  val wy = lambda_Application(lambda_Name("w"), lambda_Name("y"))
  val wyx = lambda_Application(wy, lambda_Name("x"))
  val ywyx = lambda_Application(lambda_Name("y"), wyx)
  lambda_Function("w", lambda_Function("y", lambda_Function("x", ywyx)))
}

def num_gen(number: Int): lambda_Expr = {
  def rec(n:Int, tmp: lambda_Expr): lambda_Expr = {
    if n == 0 then tmp
      else rec(n - 1, lambda_Application(S, tmp))
  }
  cbv_driver(rec(number, ZERO))
}

Thus all natural numbers are defined now.

Addition #

The addition of two numbers $x$ and $y$ can be defined naturally with the successor function:

$$ ADD\ \equiv λxy.xSy $$

It is verbose to verify this function by hand. So we can just make use of our interpreter:

val ADD = {
  val xs = lambda_Application(lambda_Name("x"), S)
  val xsy = lambda_Application(S, lambda_Name("y"))
  lambda_Function("x", lambda_Function("y", xsy))
}

def add(input1: lambda_Expr, input2: lambda_Expr): lambda_Expr = 
  cbv_driver(lambda_Application(lambda_Application(ADD, input1), input2))

Multiplication #

The multiplication of two numbers $x$ and $y$ can be defined like: $$ MUL\ \equiv λxyz.x(yz) $$ In Scala we have:

val MUL = {
  val yz = lambda_Application(lambda_Name("y"), lambda_Name("z"))
  val xyz = lambda_Application(lambda_Name("x"), yz)
  lambda_Function("x", lambda_Function("y", lambda_Function("z", xyz)))
}
def mul(input1: lambda_Expr, input2: lambda_Expr): lambda_Expr = 
  cbv_driver(lambda_Application(lambda_Application(MUL, input1), input2))

Conditional test #

Definition #

Another important primitive is conditionals. The basic elements of conditionals are true and false, they can be defined as follows: $$ \begin{align*} T\ &\equiv λxy.x \newline F\ &\equiv λxy.y \end {align*} $$ Scala code:

val TRUE = lambda_Function("x", lambda_Function("y", lambda_Name("x")))
val FALSE = lambda_Function("x", lambda_Function("y", lambda_Name("y")))

Logical operations #

With the truth values, we can now define some useful logical operations.

Below are the definitions of AND, OR and negation function respectively:

$$ \begin{align*} \land\ &\equiv λxy.xyF \newline \vee\ &\equiv λxy.xTy \newline \neg\ &\equiv λxy.xFT \end {align*} $$

We can easily translate them into Scala:

val AND = {
  val xy = lambda_Application(lambda_Name("x"), lambda_Name("y"))
  val xyf = lambda_Application(xy, FALSE)
  lambda_Function("x", lambda_Function("y", xyf))
}                                                            
def and(input1: lambda_Expr, input2: lambda_Expr): lambda_Expr = 
  cbv_driver(lambda_Application(lambda_Application(AND, input1), input2))

val OR = {
  val xt = lambda_Application(lambda_Name("x"), TRUE)
  val xty = lambda_Application(xt, lambda_Name("y"))
  lambda_Function("x", lambda_Function("y", xty))
}
def or(input1: lambda_Expr, input2: lambda_Expr): lambda_Expr = 
  cbv_driver(lambda_Application(lambda_Application(OR, input1), input2))                                     

val NEG = {
  val xf = lambda_Application(lambda_Name("x"), FALSE)
  val xft = lambda_Application(xf, TRUE)
  lambda_Function("x", xft)
}
def neg(input: lambda_Expr): lambda_Expr = cbv_driver(lambda_Application(NEG, input))

Test #

Here we implement a basic test function that determines if a input number is zero. $$ Z\ \equiv λx.xF\neg F $$ Continuously, we use our interpreter to avoid the leg work:

val Z = {
  val xf = lambda_Application(lambda_Name("x"), FALSE)
  val xfn = lambda_Application(xf, NEG)
  val xfnf = lambda_Application(xfn, FALSE)
  lambda_Function("x", xfnf)
}
def isZero(input: lambda_Expr): lambda_Expr = cbv_driver(lambda_Application(Z, input))

You can verify that: $$ \begin{align*} Z0\ &\equiv T \newline Z1\ &\equiv F \newline Z2\ &\equiv F \newline … &\ … \end {align*} $$

The predecessor function #

With the tools in our hand, now we are able to implement a predecessor function, which takes a number as input and returns the number in front of it in the sequence (thus one less than it).

A possible way to obtain the predecessor of a number $n$ is to construct a pair $(n, n - 1)$ and extract the second element of the pair.

Here is a constructor of pairs in lambda calculus: $$ PAIR\ \equiv λabz.zab $$ When the first two parameters $a$ and $b$ are applied with inputs, a pair is constructed. For example: $$ PAIR21\ \equiv λz.z21 $$ The truth value functions can then be passed to the pair to extract one element from it: $$ \begin{align*} (λz.z21)T\ &\equiv 2 \newline (λz.z21)F\ &\equiv 1 \end {align*} $$ The following function generates the pair $(n + 1, n)$ from the input pair $(n, n - 1)$: $$ \Phi \equiv (λpz.z(S(pT))(pT)) $$ An example will look like: $$ \begin{align*} \Phi(λz.z21) &\equiv (λpz.z(S(pT))(pT))(λz.z21) \newline &\equiv (λz.z(S2)(2)) \newline &\equiv (λz.z32) \end {align*} $$

To find the predecessor of a number $n$, we start from the pair $(λz.z00)$, apply it with the function $\Phi$ $n$ times and then pick the second element of the generated pair. Here is the definition of the predecessor function: $$ P \equiv λn.n\Phi(λz.00)F $$ Example: $$ \begin{align*} P2 &\equiv (λn.n\Phi(λz.00)F)2 \newline &\equiv 2\Phi(λz.00)F \newline &\equiv \Phi(\Phi(λz.00))F \newline &\equiv \Phi(λz.10)F \newline &\equiv (λz.21)F \newline &\equiv 1 \end {align*} $$ The corresponding Scala definitions will be like:

val PAIR = {
  val za = lambda_Application(lambda_Name("z"), lambda_Name("a"))
  val zab = lambda_Application(za, lambda_Name("b"))
  lambda_Function("a", lambda_Function("b", lambda_Function("z", zab)))
}

val P = {
  val pt = lambda_Application(lambda_Name("p"), TRUE)
  val spt = lambda_Application(S, pt)
  val phi = lambda_Function("p", lambda_Application(lambda_Application(PAIR, spt), pt))
  val nphi = lambda_Application(lambda_Name("n"), phi)
  val pzz = lambda_Application(lambda_Application(PAIR, ZERO), ZERO)
  val nphipzz = lambda_Application(nphi, pzz)
  lambda_Function("n", lambda_Application(nphipzz, FALSE))
}

Notice that the predecessor of zero is zero.

Recursion #

Here comes a more interesting part, where we catch a glimpse of infinite.

Y-Combinator #

You may heard that functional programming languages prefer recursions than loops. But when you look into lambda calculus, you may find it difficult to define a recursive function since functions in lambda calculus don’t have symbols that represent them.

To reference a function itself within its body, we need the help of Y-Combinator. Here is a possible approach to define the Y-Combinator: $$ Y \equiv λf.(λx.f(xx))(λx.f(xx)) $$

When we apply $Y$ to a arbitrary function $R$, we have: $$ \begin{align*} YR &\equiv (λx.R(xx))(λx.R(xx)) \newline &\equiv R((λx.R(xx))(λx.R(xx))) \newline &\equiv R(YR) \newline &\equiv R(R(YR)) \newline &\equiv R(R(R(YR))) \newline &\ …\ … \end {align*} $$

This means $YR$ will infinitely reproduce itself and pass itself to a new $R$. When we want to define a recursive function, we use its first argument to reference the function itself and then pass the function to $Y$.

For example, below is a recursive function that adds up the first $n$ natural numbers: $$ R \equiv λrn.Zn0(nS(r(Pn))) $$

The function returns zero when $n$ is zero, otherwise it returns $n$ plus a recursive call with $n - 1$ as input.

Say we want to add up from 0 to 3: $$ \begin{align*} YR3 &\equiv R(YR)3 \newline &\equiv Z30(3S(YR(P3))) \newline &\equiv 3S(YR2) \newline &\equiv 3S2S(YR1) \newline &\equiv 3S2S1S(YR0) \newline &\equiv 3S2S1S0 \newline &\equiv 6 \end {align*} $$

Another interpreter #

Unfortunately, the call-by-value interpreter we used so far is not able to deal with expressions containing $YR$, because the driver always eagerly evaluate the new results and will thus be trapped into the endless expansion of $YR$.

We can tell that the evaluation order of the interpreter matters in this case and we should carefully develop another interpreter to handle this problem.

A feasible solution is to use a call-by-name driver, which doesn’t evaluate the argument when a function is applied. The driver should beta reduce the input expression once a time and go back to the root of the expression tree before restart. In this way, $YR$ will only be expanded when needed.

The implementation of our new interpreter is as follows:

def expansion(e: lambda_Expr): lambda_Expr = e match {
  case lambda_Name(_) => e
  case lambda_Function(head, body) => lambda_Function(head, expansion(body))
  case lambda_Application(e1: lambda_Function, e2) => beta_reduc(e)
  case lambda_Application(e1: lambda_Application, e2) => 
    lambda_Application(expansion(e1), e2)
  case lambda_Application(e1: lambda_Name, e2) => 
    lambda_Application(e1, expansion(e2))
}

// call-by-name
def cbn_driver(e: lambda_Expr): lambda_Expr = {
  if isStucked(e) then e else e match {
    case lambda_Function(head, body) => lambda_Function(head, cbn_driver(body))
    case lambda_Application(_, _) => cbn_driver(expansion(e))
  }
}

You could use the recursive function $R$ to do some test. Or let’s define a more complicated recursive function, the Fibonacci number function, to have some fun: $$ FIB \equiv λrn.Z(Pn)1(r(Pn)S(r(2Pn)) $$ Definition in Scala:

val FIB = {
  val pn = lambda_Application(P, lambda_Name("n"))
  val twopn = lambda_Application(lambda_Application(TWO, P), lambda_Name("n"))
  val rtwopn = lambda_Application(lambda_Name("r"), twopn)
  val rpn = lambda_Application(lambda_Name("r"), pn)
  val rpns = lambda_Application(rpn, S)
  val rpnsrtwopn = lambda_Application(rpns, rtwopn)
  val zpn = lambda_Application(Z, pn)
  val zpnone = lambda_Application(zpn, ONE)
  lambda_Function("r", lambda_Function("n", lambda_Application(zpnone, rpnsrtwopn)))
}

Use sbt console to test it:

scala> val FIVE = num_gen(5)
val FIVE: lambda_Expr = (lambda y.(lambda x.(y(y(y(y(yx)))))))

scala> cbn_driver(lambda_Application(lambda_Application(Y, FIB), FIVE))
val res0: lambda_Expr = (lambda y.(lambda x.(y(y(y(y(y(y(y(yx))))))))))

Cool.

Well, it looks slow… #

Yes but don’t worry about efficiency.

What we have done in this article is a demonstration, showing that many important elements and features in programming languages can be reduced to pure lambda calculus. Of course it will be a disaster to really implement a language in this way (imagine a runtime performs natural number additions with $O(n)$ complexity) and we’re not going to do that.

Reducing complicated parts of a language into a simple and straightforward model is a useful strategy for proof and design. Another reason for doing this is personally I obsess with watching complex things growing from some elegant basic rules. This is a perfect toy for me. Hope you enjoy it, too :)

(almost) Anything could be lambda #

Multiple arguments #

Natural number #

Definition #

Addition #

Multiplication #

Conditional test #

Definition #

Logical operations #

Test #

The predecessor function #

Recursion #

Y-Combinator #

Another interpreter #

Well, it looks slow… #

Recommended reading #