Lambda Calculus doesn’t seem to be a suitable topic for mainstream conferences, where it must compete against numerous talks about the latest and greatest technologies, new programming languages or the coolest container solution.
But Codemotion is different – you can always find an unexpected talk about unexpected topics, such as functional programming and lambda calculus. The upcoming Codemotion Online Tech Conference will take place on October 2020, and such topics are part of the agenda. If you are interested, don’t miss the opportunity to attend: free tickets are available through the website!
Functional programming and lambda calculus have been also discussed in past Codemotion conference. Jarek Ratajski, a self-appointed anarchitect, isn’t someone who goes unnoticed; in a monk’s habit, with long hair and beard, he seems to come from another dimension, where Functional Programming is the everyday standard, and nobody is frightened of Monads.
In his talk at Codemotion Rome 2019, Jarek demonstrates how it is possible to derive natural numbers, Boolean logic, and even conditional statements (i.e. the ‘if’ statement) from the definition of the identify function alone, in contrast with the conventional approach based on Set Theory.
How Lambda Calculus works
To understand how this works, please bear with me: the typical notation for the identify function is λx.x, were λx represents the head of a function with a single input parameter x, followed by the body of the function after the dot (.) – in this case just the bounded variable x.
The more general notation is λx.(expression), with one input parameter x and a generic expression as function body.
Then, if we consider the lambda λx.(λy.y), it represents a function that returns the identity function, which can be rewritten as λx.λy.y or just λxy.y. By definition, this lambda represents the number 0 and all the subsequent numbers can be defined as:
0 ≡ λx.λy.y = λxy.y
1 ≡ λx.λy.x y = λxy.x y
2 ≡ λx.λy.x x y = λxy.x x y
…
n ≡ λx.λy.(x … x y) = λxy.(x … x y) with x repeated n-times
In Lambda Calculus notation, the space (‘ ‘) character represents the application of a function, so if we want to apply 3 times function f to variable a we can write:
3 f a = (λxy.(x x x y)) f a = f f f a or f(f(f(a))))
In general, we can define the successor function as follows:
succ ≡ λn.λf.λx.f (n f x)
then we can calculate the successor of 0:
succ 0 = (λnfx.f (n f x)) 0 = λfx.f (0 f x) = λfx.f x ≡ 1
or we can calculate the successor of 1:
succ 1 = (λnfx.f (n f x)) 1 = λfx.f (1 f x) = λfx.f f x ≡ 2
and so on.
We can continue using this notation to define the predecessor function, so we can now determine the sum and the difference.
It’s also easy to incorporate Boolean logic by introducing the ‘true’ and ‘false’ functions:
T ≡ λxy.y
F ≡ λxy.x
and then the ‘and’ and ‘or’:
and ≡ λpq.p q p
or ≡ λpq.p p q
Starting with these simple building blocks, we are gently introduced to the basis of Lambda Calculus, defined by Alonzo Church in the 1930s as the theoretical foundation of function recursion and, to an even greater extent, of Functional Programming, as opposed to the Imperative Programming founded on Turing’s Machine.
Thinking as a Functional Programmer
If you want to understand Lambda Calculus, you should stop thinking about functions as we’ve been always taught – as something that associates an element of a Set to an element of another Set
This strange universe where nothing exists except Lambdas might look unpleasant and scary. However, Lambda Calculus is Turing Complete, so anything we can write in an imperative style, with programming languages such as Java or C#, can also be written in functional way in languages such as Scala or Haskell.
One could, of course, argue that we have known that since the ‘30s, but Functional Programming now seems to be hot again, being more suitable for modern multi-threaded or distributed applications.
Adopting this programming approach can be somewhat intimidating but, as Jarek Ratajski said in his talk, if you go back to basics this path can be both fun and profitable… and it doesn’t require a PhD in Mathematics!
It might seem that this means that the solution to our (technical) problems is at hand, that this is the silver bullet that will make our code error-free and our architecture solid as a rock… unfortunately, this is not the case and these strong, theoretical fundamentals can actually betray us!
You know when you create your beautiful architecture, but your customer changes requirements every day and your architecture…. goes bananas!
Conclusions
During his talk at Codemotion Rome 2019, Jarek Ratajski reminded us of one of the most important results derived from Lambda Calculus: Church‘s proof that there are unsolvable problems – Hilbert’s Entscheidungsproblem – such as computable procedures which can decide whether two given terms convert to one another, as in Gödel’s first incompleteness theorem.
The barber is the “one who shaves all those, and those only, who do not shave themselves.” The question is, does the barber shave himself?
This means that our code can never be perfect and, worse still, that there is no code that can prove that. Despite that, we should keep coding and, above all, have fun with it.
The source code for Jarek’s library can be found on GitHub if you are willing to give it a try. Be careful though! Because of the undecidability theorem, there is a strong possibility that his software does not work!
Finally, if you are interested in functional programming and lambda calculus, don’t miss the opportunity to attend our upcoming Codemotion Online Tech Conference: there are also free tickets!
If you want to know more about how modern technologies and tools can support you for – and during – the organisation of a virtual event, don’t miss this article showcasing the best tools we used to host our online conferences since the COVID-19 outbreak.
