Lambda World 2017 – Lambda Core, hardcore

Despite the title which is a bit obscure, this talk has been very clear and entertaining. The speaker Jarek Ratajski (@jarek000000) who defines himself as a functional programmer, wizard, and anarchitect, definitively knows his art and how to make an engaging speech.

Btw, an anarchitect is a person that breaks the rules so that something can be eventually done.

As usual, mistakes, errors, and inaccuracies are all my faults. A last note: you need Scala 2.12 to compile the code presented here, older versions are likely to fail.

I really recommend watching the presentation video on youtube.

---

Let’s start with a question for the attendees – you are on a desert island and you can take just one thing from the civilized world. What would you like to have to survive?

[someone from the audience shouts “wifi”]

Well, you need Math. Math is the base for everything, but it is huge! So, maybe we can find a small subset, a core, that allows us to recreate the whole Math.

Lambda is a building block of math. Using lambda calculus we can build – one step at a time – the whole Math. Historically Math has been built using sets, unfortunately, sets had some problems in terms of paradoxes, so mathematicians resorted to this simpler mechanism.

So lambda (λ) is a function that takes some lambda as a parameter and produces another lambda. A lambda is written as:

λ x. some expression

A λ x is applied to λ y with the following notation –

x(y)

to a scala developer:

trait Lambda {
    def apply(x: Lambda) : Lambda
}

Now suppose we are on a deserted island with just our Scala compiler. Just the compiler – no jars, no collections, no scala utils, no Boolean, Int, Float, Double, String… anything at all.

The only exception to this nothingness is the badlam package in order to simplify and help the presentation of concepts.

Let’s define the identity, which is a function that returns the function accepted as an argument:

λ x. x

In Scala it turns out to be:

val identity : Lambda = (x) => x

val id2 = identity(identity)

Now we can define a function that accepts multiple arguments (via the curry mechanism) and always returns the first one:

val funny: Lambda = (x) => (y) => x

Note that names are not important, but the structure is. The “funny” function structure can be used to implement true and false concepts:

val aTrue = funny
val aFalse : Lambda = (x) => (y) => y

Note that aFalse is complementary with respect to aTrue. Now that we have true and false symbols we can define boolean operators:

val and : Lambda = (p) => (q) => p(q)(p)

You can read this like: and is a function that via currying accepts two arguments p and q. Consider p: it can be either true or false. If it is true its lambda evaluates to its first argument, otherwise to the second. So, when p is true, the and expression evaluates to q, so and is true when both arguments are true. If p is false, then p is returned – no need to consider q.

Let’s check with Scala:

val result1 : Lambda = and (aFalse)(aTrue)

This evaluates to aFalse, while

val result2:Lambda = and (aTrue)(aTrue)

This evaluates to aTrue.

Or function is based on the same scheme used by and:

val or:Lambda = (p) => (q) => p(p)(q)

To define not is a matter of reversing the true/false definition:

val not: Lambda = (p) => (a) => (b) => p(b)(a)

So long, so far, we have defined all the tools we need for boolean calculus. Let’s see if we can express numbers. One approach could be:

val zero: Lambda = (f) => (x) => x
val one: Lambda = (f) => (x) => f(x)
val two: Lambda = (f) => (x) => f(f(x))
val three: Lambda = (f) => (x) => f(f(f(x)))

So numbers are functions (of course) that accept a function and an argument and return zero or more applications of the function to the argument.

Zero is the identity. One is the single application of lambda f to the identity. Two is the single application of lambda f to one, that is that application of lambda f to the application of lambda f to the identity, and so on…

This may work, but it is boring to encode all numbers in this way. A function that computes the successor of a given number could be a good tool to lessen the burden:

val succ:Lambda = (n) => (f) => (x) => f(n(f)(x))

[NdM – well this is mind-boggling and I have a hard time decoding. Conceptually is simple – just remember that an integer n is represented by a lambda that accepts a function f and an argument x and returns a function composing n nested applications of f over x. So replace x with f(x) and you are done.]

Now we can define addition and multiplication

val plus: Lambda = (m) => (n) => (f) => (x) => m(f)(n(f)(x))
val mult:Lambda = (m) => (n) => (f) => m(n(f))

[NdM -It takes a while for these two as well. Sum is intuitively easy, take 3+2=5, in lambda is: x => f(f(f(x))) + x => f(f(x)) = x => f(f(f(f(f(x))))). You may read plus as: (m,n,f) => (x) => m(f)(n(f)(x)) , that is a function that takes two operands and one function. Remember that m represents an integer by applying a function m times to an operand. So swap in f as an operand and you have m times the application of f, now applies this function to an argument that is n times the application of f to x.]

Multiplication is similar, x is omitted to keep the code terse, but you can read it as:

val mult:Lambda = (m) => (n) => (f) => (x) => m(n(f))(x)

Keeping the sum approach in mind, this is similar – applies m times a function that is composed by n application of f to x. I needed quite a neuron effort to figure this out.]

Predecessor can be defined as:

val pred: Lambda = (n) => (f) => (x) => n((g) => (h) => h(g(f)))((u) => x)((u) => u)

[NdM. I tried hard to understand this, but simply I couldn’t wrap my mind around it. I don’t have even the slightest idea of how this is expected to work. If you figure it out, let me know, please… well indeed, I think that the last part (u) => u, being an identity, is used to skip an application in the application list, therefore reducing by 1 the application list…]

[NdM. I found this thorough explanation of the predecessor on stackoverflow]

Now we can do something even more interesting – conditionals:

val ifLambda: Lambda = (c) => (t) => (f) => c(t)(f)((x) => x)
val isZero: Lambda = (n) => n((x) => aFalse)(aTrue)

Recursion would be a nice addition to the computing arsenal of lambda calculus since it allows the expression of iterative algorithms. But how are we supposed to call a function when lambda functions are anonymous?

First, let’s define a function that makes its argument call itself:

val autocall:Lambda = (x) => x(x)

Then we need a helper function that makes something call itself

val Y: Lambda = (f) => autocall((y) => f((v) => y(y)(v)))

And finally, we define a function containing the body of the recursive function:

val G:Lambda = (r) => (b) =>
  (ifLambda(isZero(n))
    ((x) => one )
    ((x) => mult(n)(r(pred(n))))
  )

Now we have everything to recursively compute a factorial:

val fact = Y(G) // this makes G recursive

[NdM: Once more I have a hard time trying to understand this part. It makes sense intuitively, but I’m lost in details such as function Y. The overall idea is pretty well laid out]

Turing Equivalent?
Lambda calculus has been proved to be Turing- equivalent, meaning that every algorithm that can be implemented on a Turing Machine, can also be implemented using Lambda Calculus. Therefore, you have no excuse, everything can be done purely functional!

Equivalence

In mathematics there are a lot of problems, an interesting one is about theorems.

For a mathematician, a theorem is something like

if ( condition(args)) then statement(args)

That is, if something holds, then something else is true. It would be nice to build a machine that automatically checks this. This is what about a century ago, mathematicians were looking for – a machine that renders us useless by proving theorems by itself.

In the same way, we used lambda calculus to represent numbers, booleans, and statements, we could rewrite the theorem as a lambda calculus expression and then execute it to let it show true or false to determine whether the theorem holds or not.

This could be such a machine:

def main( args: Array[String]) : Unit = {
    val autocall: Lambda = x => x(x)
    println( SmartDisplay.web.display(autocall))
    val OMEGA = autocall(autocall)
}

[NdM: also after having watched the youtube video of the conference, I can’t tell where this function comes from. I believe Jarek, but I have no explanation of why this function should prove theorems.]

That would be awesome, regrettably, it doesn’t work. In fact, autocall function is invoked over autocall itself causing a stack overflow. This is generally what happens when you try to analyze a lambda function for equivalence.

This fact has been proved in 1936 by Alonzo Church: “No computable function can decide the equivalence of two different lambda functions”.

Despite this, there are two guys on stack overflow that are trying to do exactly this in C#.

Lambda calculus is convenient, but it undergoes the incompleteness theorem by Kurt Gödel – For any consistent, effectively generated formal theory that proves certain basic arithmetic truths, there is an arithmetical statement that is true, but not provable in the theory.

In other words, it doesn’t matter how cool your formalism is, you still can’t fully automate through an algorithm to prove the properties of another algorithm.

So this is what nearly a century ago a group of mathematicians, led by Alonzo Church, devised in search of more elegant mathematics.

What I presented today is called Untyped Lambda Calculus. Take plus and try to add true and factorial together. It doesn’t make sense. So, by using this notation you can also write correct expressions that don’t make sense.

Since not every expression you can write makes sense, it is a programmer’s duty to write and use only those that make sense.

Typed lambda calculus checks correctness for you. Untyped lambda is very much like javascript in which you can write everything and is not checked for type correctness.

I haven’t talked about Lazy/Eager evaluations in lambda calculus. This is a very complicated issue, even if very fun. If you do lambda calculus on paper you will notice that sometimes you need to evaluate lazy and other times you need to evaluate eager.

Usually, when you read about lambda calculus in Scala, you don’t find what I have shown you, you find something else – lambda calculus done on the type system of Scala:

sealed trait True extends Bool {
    type If[ T <: Up, F <: Up, Up ] = T
}

sealed trait False extends Bool {
    type If[T <: Up, F <: Up, Up] = F
}

This is not performed at run-time but at compile time. This is awesome because the compiler does all the calculations and produces such fine errors you can’t even figure out where they end.

Sources

• wikipedia
• blog: (C# Version) Dixin’s blog – this is the post where I took inspiration for this talk.
• Book: Roger Penrose: The Emperor’s New Mind – this is not about only lambda calculus, but about computation. Reading this book will help you better grasp the subject.
• Lambda Visualization – Badlam this is nothing special just a package to help the presentation. It is known to work only in presentation and not elsewhere.
• This same presentation in Java – is the original work. This presentation has been done first in Java (for fun and drinking beer of course).

---

NdM: that’s the end of the presentation. Here I add my fragment of code I used to check the code. If you prefer you can use Badlam, the code below is in Scala.

Function to convert from lambda numbers to decimal –

def dec( y : Lambda ) : Int = {
    case class Counter( counter: Int) extends Lambda {
        def apply( x: Lambda ) : Lambda = {
            this
        }
    }
    case class Fun() extends Lambda {
        def apply( x: Lambda ) : Lambda = {
            Counter( x.asInstanceOf[Counter].counter+1 )
        }
    }

    y( Fun() )(Counter(0)).asInstanceOf[Counter].counter
}

The trick is to give function f of lambda the semantic of incrementing its argument by 1. If the argument has type int and starts counting from zero the conversion is done.

The following code is just a pretty printer for lambdas that are not integers:

def del( x : Lambda ) : Unit = {
    x match {
        case `aTrue` => println( "true" )
        case `aFalse` => println( "false" )
        case `and` => println("<and>")
        case `or` => println("<or>")
        case `not` => println("<not>")
        case _ => println("?")
    }
}

(where aTrue, aFalse, and all the other symbols are defined as in Jarek’s presentation.