42 ms·

What is it in the lambda calculus?

by nixpulvis 3y ago

lmm 3y ago
(Lx.xx)(Lx.xx) is the most famous/well-known one.
- tromp 3y ago
  And as it turns out, the smallest one too. For combinatory logic with the usual {S,K} basis, it's S S K (S (S S K).
burnished 3y ago
What does 'lambda calculus' mean? I read that lambda refers to binding to variables - so is 'calculus' really just a way to refer to calculating generally? I suppose I only know the word contextually from the math class that shares the name.
- sam_bristow 3y ago
  "Lambda calculus is a notation for describing mathematical functions and programs. It is a mathematical system for studying the interaction of functional abstraction and functional application. It captures some of the essential, common features of a wide variety of programming languages." - https://www.cs.cornell.edu/courses/cs3110/2008fa/recitations/rec26.html https://www.cs.cornell.edu/courses/cs3110/2008fa/recitations...
  - greiskul 3y ago
    And the name of this very website we are talking on is derived from lambda calculus. The y combinator is a fixed point combinator in lambda calculus.
- simiones 3y ago
  Someone else gave a very good definition, but I'll add that historically, the Lambda Calculus was a system designed by Alonzo Church to get a formal notion of what "computation" means in mathematics. As in, a formally-defined set of rules for how a computation can be represented, and then be mechanically carried out to achieve a result. The need for such a system came about because of mathematicians wanting to define what it means for a function to be computable in a formal sense, and to be able to define and prove other theorems about computation. The other famous model of computation, which was invented at about the same time, was Alan Turing's "Turing machine", which he used to prove that the halting problem was not computable. Just for a short taste, in the lambda calculus the base entity is an abstract function that can be applied to a variable and return a result. You are probably familiar with formulae like `f(x) = x`. In the lambda calculus formalism, this is written as `\lambda x.x`. However, it's important to note that there is no direct equivalent to something like `f(x) = x + 1` - addition or numbers are not a part of the lambda calculus directly. Instead, you can define numbers and then addition in terms of functions and variables. Instead, the lambda calculus has rules for how function application should work to reduce complex formulae to simpler ones. For example, `(\lambda x.x) y` reduces to `y` [equivalent to f(x) = x; f(y) = ? => y]. Or, `(\lambda x.y) z` reduces to `y` [equivalent to f(x) = y; f(z) = ? => y]. And, if we go on to more complex expressions: `(\lambda x.x) (\lambda x.y) z` reduces to y by applying the reductions above successively (first we reduce the initial expression to `(\lambda x.x) y` then we reduce this to just `y`. It can be shown that this model of how to reduce the formulae of lambda calculus is in fact equivalent to the model of the Turing machine that can write a symbol on its tape.

What is it in the lambda calculus?

lmm 3y ago

(Lx.xx)(Lx.xx) is the most famous/well-known one.

tromp 3y ago
And as it turns out, the smallest one too. For combinatory logic with the usual {S,K} basis, it's S S K (S (S S K).

burnished 3y ago

What does 'lambda calculus' mean? I read that lambda refers to binding to variables - so is 'calculus' really just a way to refer to calculating generally? I suppose I only know the word contextually from the math class that shares the name.

sam_bristow 3y ago
"Lambda calculus is a notation for describing mathematical functions and programs. It is a mathematical system for studying the interaction of functional abstraction and functional application. It captures some of the essential, common features of a wide variety of programming languages." - https://www.cs.cornell.edu/courses/cs3110/2008fa/recitations/rec26.html https://www.cs.cornell.edu/courses/cs3110/2008fa/recitations...
- greiskul 3y ago
  And the name of this very website we are talking on is derived from lambda calculus. The y combinator is a fixed point combinator in lambda calculus.
simiones 3y ago
Someone else gave a very good definition, but I'll add that historically, the Lambda Calculus was a system designed by Alonzo Church to get a formal notion of what "computation" means in mathematics. As in, a formally-defined set of rules for how a computation can be represented, and then be mechanically carried out to achieve a result. The need for such a system came about because of mathematicians wanting to define what it means for a function to be computable in a formal sense, and to be able to define and prove other theorems about computation. The other famous model of computation, which was invented at about the same time, was Alan Turing's "Turing machine", which he used to prove that the halting problem was not computable. Just for a short taste, in the lambda calculus the base entity is an abstract function that can be applied to a variable and return a result. You are probably familiar with formulae like `f(x) = x`. In the lambda calculus formalism, this is written as `\lambda x.x`. However, it's important to note that there is no direct equivalent to something like `f(x) = x + 1` - addition or numbers are not a part of the lambda calculus directly. Instead, you can define numbers and then addition in terms of functions and variables. Instead, the lambda calculus has rules for how function application should work to reduce complex formulae to simpler ones. For example, `(\lambda x.x) y` reduces to `y` [equivalent to f(x) = x; f(y) = ? => y]. Or, `(\lambda x.y) z` reduces to `y` [equivalent to f(x) = y; f(z) = ? => y]. And, if we go on to more complex expressions: `(\lambda x.x) (\lambda x.y) z` reduces to y by applying the reductions above successively (first we reduce the initial expression to `(\lambda x.x) y` then we reduce this to just `y`. It can be shown that this model of how to reduce the formulae of lambda calculus is in fact equivalent to the model of the Turing machine that can write a symbol on its tape.