λ-Calculus with Kotlin

The Lambda Calculus is a symbol manipulation framework developed by the mathematician Alonzo Church in the 1930s. It was intended to be an extremely tiny syntax which could nevertheless suffice to calculate anything computable. The mathematical advantage of such a syntax is that with such extreme simplicity, it becomes easier to write formal proofs about computational logic – demonstrated when Church solved David Hilbert's famous Decision Problem using LC.

Another famous mathematician, Alan Turing, formulated a different model of universal computation – the eponymous Turing Machine(..) He proved that the Turing Machine and Lambda Calculus are equivalent. Everything that one can calculate, the other can. Not only this, but Turing and Church posited (in the "Church-Turing Thesis") that these systems universally capture the definition of computability.

However, mathematicians and computer scientists have long known that the entirely abstract lambda calculus, being equivalent to a TM, meant that computations could be expressed in a style independent from machine instructions. Instead, a language consisting of first-class function expressions – aka lambda abstractions – could be subsequently compiled into machine code. Such a language would benefit from decades of mathematical research. And just as real computers extend Turing Machines with extra power and convenience, these functional languages would extend the lambda calculus with additional features and under-the-hood shortcuts (such as hardware-based arithmetic).

-- Lambda Calculus Talk by Gabriel Lebec