Posted on Jul 24 The Lambda Calculus was developed in the 1930s by the mathematician Alonzo Church, none other than the teacher of Alan Turing, atheist, homosexual, father of the computer science. It was introduced as a way to explore the foundations of mathematics and computation.The title of the post is a quote from the introduction to Thomas Garrity's "Mathematical Maturity" lecture (I recommend you watch it before continuing. It's 40 seconds long and very funny). This quote perfectly encapsulates the essence of the lambda calculus. Keeping it short, the lambda calculus is a model of computation where the only thing you can do is define functions with one argument that returns another Function (You can think of a function as a way to map an input to an output).Even though it's simple, the lambda calculus is Turing complete, which means that if you give it enough time and resources, it can solve any solvable computational problem.But how would we write a real program with only functions? What about branching and recursion? Well, you actually can do those things with just pure lambda calculus. But first, how we can use more than one value inside a function?We can apply β reduction to make things clear:This is a method called currying, named after some random guy called Haskell Curry, who invented it. It allows us to break down a function that takes multiple arguments into a chain of single-argument functions.Okay, but how do we make conditional operations, like ifs and elses ? Let's define our booleans first:Those are called Church booleans, abstractions that receive two arguments and, If True, the first argument is returned. If False, the second argument is returned.With Church booleans in place, we can now simulate a branching behavior using Church booleans and abstractions. Here's how you can define a conditional expression in lambda calculus:The condition is represented as a parameter, one of the church booleans that will determine with of the branches will be returned.You will get it when we reduce it again. Don't worry about the arithmetic operations, I'll talk about them later.The most popular way to represent natural numbers in lambda calculus is using the Church numerals encoding. In summary, the definition of the numeral N, is the application of a given function F N times to a given value.Here is a small list of definitions, from 0-3.Let's use the definition of 3 for example. If you think about it, in most cases, the result of λf.λx.f (f (f x)) will not be the number three, unless the function we are providing is the succ (as defined below) and the 0 numeral as the value. This is simply a way of doing something three times, which means that not the result, but the function itself is the church numeral three.But how do we get the successor of a numeral?The succ function works by applying f to x one more time, returning the definition of the Church numeral that represents the successor of n. If you reached this point, you should be able to apply reduction to succ 3 and confirm this by yourself. It's fun, I promise!Now that we have numbers, we should be able to operate over them.At this point, we are already composing functions. A good way to explain what's happening on the add definition is that we are applying succ to n m times. Let's partially reduce it to make things clear:We applied succ at 1 two times, which evaluates to 3.The multiplication function is as simple as applying addition to m n times. Similar to what we did on the add definition.Opposite to the successor function, we also have the predecessor function. We'll also need it to be able to subtract numbers. Predecessor is defined by the following formula:I won't write the reduction for this case to keep things short, but again, we are just applying pred to m n times. You can take a look at add reduction if you are confused.Recursion is a powerful concept in programming languages. Even lambda calculus being extremely simple, we can still use some tricks to achieve recursion.But what is recursion? Take a look at this factorial example in javascript:What makes fact interesting to us is the fact that it calls itself. That's recursion! Unfortunately, there isn't a direct way of achieving recursion directly.We'll need to use a little trick called the Y combinator (I'm not talking about Silicon Valley's Y Combinator, but the fixed-point one).The Y combinator takes a function as an argument and returns a fixed-point of that function. In other words, it enables self-reference within a function. Don't worry, I'll explain what a fixed-point is and why it works later.Let's write the factorial function in the lambda calculus syntax, so we can see the Y in action:The definition of fact is perfect, but how can we call it? f should be the fact function itself. Can you think of a way to reference it?First, let's see a fixed-point in action:That's why Y is called a fixed-point. Regardless of the value of the function g, Y is still the same.Well, given that, how does this fix the issue with the f parameter on the fact function? Let's plug both things together:Wait, that was it? Yes! That's exactly what we needed as an argument to the f parameter on fact. A reference to itself. We can keep reducing to see if it will work (Don't run away, please! Read it slowly and I promise it will make sense):And that's how you achieve recursion in pure lambda calculus.The lambda calculus, a foundational concept in mathematics and computer science, provides a way of expressing computation using only functions. It shows the elegance and versatility of functional programming, proving its capability to solve complex problems with simplicity. It continues to influence modern programming paradigms, making it a timeless and fundamental concept in the realm of computation.If you made it this far and are still interested, you can see on this repository an actual implementation of the lambda calculus.References:Templates let you quickly answer FAQs or store snippets for re-use. Are you sure you want to hide this comment? It will become hidden in your post, but will still be visible via the comment's permalink. Hide child comments as well Confirm For further actions, you may consider blocking this person and/or reporting abuse Robert Mion - Jul 14 '22 HAFIZ ABDULMANAN - Jul 25 '22 Vedant Chainani - Jul 24 '22 Corbin Crutchley - Jul 21 '22 Once suspended, hnrbs will not be able to comment or publish posts until their suspension is removed. Once unsuspended, hnrbs will be able to comment and publish posts again. Once unpublished, all posts by hnrbs will become hidden and only accessible to themselves. If hnrbs is not suspended, they can still re-publish their posts from their dashboard. Note: Once unpublished, this post will become invisible to the public and only accessible to Henri Borges. They can still re-publish the post if they are not suspended. Thanks for keeping DEV Community safe. Here is what you can do to flag hnrbs: hnrbs consistently posts content that violates DEV Community's code of conduct because it is harassing, offensive or spammy. Unflagging hnrbs will restore default visibility to their posts. DEV Community — A constructive and inclusive social network for software developers. With you every step of your journey. Built on Forem — the open source software that powers DEV and other inclusive communities.Made with love and Ruby on Rails. DEV Community © 2016 - 2023. We're a place where coders share, stay up-to-date and grow their careers.