r/mathematics • u/NationalStill6968 • 4d ago
Calculus what is lambda Calculus?
hey can anyone explain me the lambda calculus and its use cases in turing machine and how it helps the programming languages in a very simple way !!!
Thanks and really excited to read you explanations .
16
u/omegafixedpoint 4d ago
lambda calculus is a term rewriting system based on functions. you define a function in lambda-calculus by writing (λ x.M)
The lambda means "this is a function". What comes after the lambda and before the dot is the name of what the function takes in. What comes after the dot is what the function's output is. For example, in normal math notation you might write f(x) = x + 1. In lambda calculus, that would be (λ x.x + 1).
You use a function by juxtaposing an input next to it. Then, to run the program, you swap out the "x" (or whatever the variable is called) in M. The rule is:
(λx.M) y = M[x := y].
For example: in math, if I define f(x) = x + 1, I know f(1) = 2. In lambda calculus, this would be: (λx.x + 1) 1 = (x + 1)[x := 1] = 1 + 1 = 2.
The key thing is that functions are treated as objects that exist in a spot. They don't have names.
Lambda calculus is "useful" in turing machines in that turing machines can compute any algorithm, and λ-calculus can simulate a turing machine. It is "turing-complete," and thus as expressive as imperative programming based on sequences of instructions and a state. If you are not familiar with turing machines, they are based on an infinite tape of instructions and a set of possible states. Each step of the program, the tape is read at the head, and a state is selected from the possible states. You can see how this resembles programming in a language like C++ or Python, where programs are structured as a list of statements or commands (imperative programming). Lambda calculus behaves more like a series of transformations. The program runs by transforming the expression by the rules I explained.
Lambda calculus is useful for programming and mathematics.
In programming, lambda calculus is useful for:
- Ergonomic reasons: it is often faster to write a function once than write a whole new function definition with a label at the top level of the program. e.g., to make a function to add one to every number in a list, I would write (list.map (λ x => x + 1)) whereas in languages without first class functions, I would have to define a new function "def add_one_list(list): [x + 1 for x in list]"
- Safety & maintainability reasons: you may have noticed that in λ calculus, the functions don't have names. This is because programs are written in terms of expressions rather than statements. If you are familiar with rust, this is like how you can say (let x = if something then 1 else 2;) whereas in a normal imperative language, you are writing a sequence of steps of what the computer should do: if something then: x = 1 else: x = 2. In lambda calculus, there is no "state" of the program. All of the state is contained inside the function. It is dictated by the definition of the function (what it does to its input variable) and nothing more. This makes code easier to maintain, since a function can only affect itself. It cannot modify some magic number variable somewhere, and thus have downstream consequences on other pieces of code. This makes code more modular and portable.
In mathematics, λ calculus is useful because of the "Curry-Howard isomorphism." Just like in imperative programming, we often like to assign types to objects in a program to prevent undefined behavior. We don't want a function to make a string uppercase work on numbers because its behavior is undefined. What would it output? Who knows. Thus, we restrict the possible programs that can exist to improve safety. However, in λ-calculus, the types of functions actually coincide exactly with mathematical statements in logic. A typed function in λ-calculus looks like this:
λ x : A.M
This means just like before. This function takes in an x, and when you feed something into it, you replace all the x's inside M with what was fed in. Except our function can only accept x's that are A's (that have type A). For example, a function to add one to numbers: λ x : ℕ.x + 1. This function only accepts natural numbers. And its type is ℕ → ℕ. What comes on the right side of the arrow is determined by M (the output of the function). The key insight is that a lambda function with type A → B is a proof of that same implication in logic. The statement if A, then B is proven by the programmer or mathematician writing a lambda function to give back a B if you input an A. For example, we know that ℕ ⊆ ℝ (all natural numbers are real numbers). We can prove that the natural numbers are a subset of the real numbers in lambda calculus by supplying a lambda function that takes in an x : ℕ and outputs an ℝ.
This field of study is called type theory. It is about how we can restrict which programs are possible, and what the types tell us about what a program does, and what it lets us prove.
The final boss of type theory is "dependent type theory." In dependent type theory, the type of a lambda function λ x : A.M is not just an arrow (an implication), but actually another lambda (called Π). The rule is:
M[x] : B[x]
---------------------------------
λ x : A.M : Π x : A.B
This rule says that the kind of object returned by the function is determined by the specific input to the function. For example, I could have a function that produces a proof that a number is odd or even. This function's type would be written as: Π x : ℕ.(Odd x) ∨ (Even x). Notice that the codomain (the output type) of the function is even more lambda calculus. With just this extension, we can express first order logic. Theorems are types and proofs are programs. This means every proof is constructive, and it has wide ranging implications for theorem proving, since now the computer can tell you for a fact whether your proof is correct or incorrect, just by following its rules of what constitutes a valid program.
I won't overwhelm you any more. Let me know if you have any questions I hope this is somewhat comprehensible.
3
1
u/UnderTheCurrents 4d ago
Lambda calculus was intended as a way to express functions as rules because some founding fathers found that having them represented as ordered sets says nothing about the internal relationships. 2 + 2 = 4 and 3 + 1 = 4 might refer to the same individual but they are intensionally different.
Because of its broad scope and self-application it can be used to define all sorts of concepts, including inferences and recursively enumerable functions. On the flipside you somtimes have to restrict it with types because it can express logics up to nth orders and fails to be complete.
1
u/hijibijbij 3d ago
Other answers are quite good but maybe I can help you with some low-level basics.
So the plan here is to have some form of mechanism that is so basic that you can mechanically follow some simple rules without any judgement/understanding but it is still capable for doing computation.
We start with some uninterpreted symbols. Imagine you have an infinite supply of symbols, but they do not have any meanings. The only thing you can do with them basically is to check if two of the symbols you have got in your hands are the same or not. Other than that they have no interesting properties.
Usually people denote these symbols by, say, x, y, z, or maybe even aaa, aaaa [note that aaaa here is not the result of adding another a to aaa, they are unrelated, because they are two different symbols].
Now we introduce two more rules to create new things out of these symbols. The first of them, called "application" [the reason for choosing this name will probably be clearer later, but the name is not too important]. This rule takes two things and creates a thing that will be called an "application". Usually people denote this by "juxtaposition" which is to say they just put the two things one beside another and then put parenthesis around it. So the "application" created from the symbols x and aaa would be denoted by (x aaa). But you can take the result of an application and create another application out of it. So, (x ((y z) w)) is an application [made from x and ((y z) w) which is itself an application and so on].
The other rule is called an "abstraction". Again, the name is not super-important. It is another rule to create another kind of object out of two existing ones. But this time, the abstraction specifically takes a symbol as the first thing. The second thing can be anything [a symbol, an application, or even another abstraction]. We write an abstraction made from the symbol x and some other stuff [let's say application of y with y, so (y y)] like this: (λ x. (y y)). The λ character is special, its role is to be able to distinguish between an application and an abstraction. so (something something-else) is an application, but (λ something. something-else) is an abstraction. The period after the symbol x helps us separate the symbol from the other thing. Also, we now allow an abstraction to be either of the two things that make up an application from now on.
Now, sometimes people are lazy and write (a b c) for ((a b) c) and (λ x y. z) for (λ x. (λ y. z)) but these are sort of inessential for the main purpose.
Now the main purpose is, that with some complicated thing [something like (x ((λ y. z) (c a)))], you are allowed to do the following [kind of complicated] procedure. If in any place there is an abstraction as the first thing in an application, so somewhere there is something that looks like ((λ x. E) V) [here E and V are not symbols, they represent some expression like, say, z or (c a)], then you are allowed to replace this whole thing [abstraction inside application] with E, but you are going to replace every x in E with V.
Example: in ((λ x. (λ y. x)) b), you could say, E is (λ y. x) and V is b. The rule then says you can replace this whole thing with (λ y. b) [which is the result of changing every x in E to b].
Seems like a tiny little toy "language" with one weird rule to kind of evolve it step-by-step. Funny thing is that this is all you need to encode any computation whatsoever [that you can do with, say, a Turing machine]. You can define numbers, booleans, addition, xor-ing, factorial, finding the GCD of two numbers, lists, sorting function of lists, anything, any pure computation.
I am skipping over some details [like "alpha-conversion" most notably] but I don't think they are the crux of the issue. It is just a rewrite rule for strings made up of symbols. It was a complete surprise how powerful this one re-write rule is.
Hope this helps.
1
u/GatePorters 3d ago
It basically reduces all of computation into 3 pieces and one computation.
3 pieces are variables, functions, and calling functions.
The one computation is beta reduction, which is just substitution until you can’t anymore.
With those 3 pieces and one computation, you can represent anything that can be represented.
1
u/Double_Sherbert3326 3d ago
It’s the idea that a function is an object, essentially. It’s the idea that you can provide a function itself as the argument for another function, so it is a formal system that allows for object composition aka nesting of functions. This is useful because computers are discrete but some functions are continuous, so it allows us to better approximate continuous expressions in our formal language. The proof of the fundamental theorem of calculus relies on object composition, so it allows us to Get at these kinds of things in our formalization of language.
15
u/dskippy 4d ago
The Lambda Calculus is a programming language. Among the simplest. It was created as a way to study computation in the simplest most fundamental way. So was the turning machine. Thet are independent. I wouldn't say that the lambda calculus has use cases in turning machines. They are two independently developed foundations of computation.
Their development in the 1930s around the same time gave rise to the widely believed though technically not proven Church turning thesis. It states that any computable function can be computed with either one of them.
The lambda calculus is very simple. There are three grammar rules.
e ::= λx.e | e e | x
An expression is either a function with a variable and a body, an application of a function to am expression as an argument, or a reference to a variable. All values are functions.
The usefulness is largely in studying both computation and programming languages. Since it's so simple you can study the entire thing and understand what is capable of doing when you add a new feature and prove important theorems about new language features in the context of a very simple language so proofs about behavior of new features is straightforward. Those can then be added to more complex languages with the understanding that they are sound.