28
$\begingroup$

I've been reading for a few weeks about the Lambda Calculus, but I have not yet seen anything that is materially distinct from existing mathematical functions, and I want to know whether it is just a matter of notation, or whether there are any new properties or rules created by the lambda calculus axioms that don't apply to every mathematical function. So, for example, I've read that:

"There can be anonymous functions": Lambda functions aren't anonymous, they're just all called lambda. It is permissible in mathematical notation to use the same variable for different functions if the name is not important. For example, the two functions in a Galois Connection are often both called *.

"Functions can accept functions as inputs": Not new you can do this in with ordinary functions.

"Functions are black boxes": Just inputs and outputs are also valid descriptions of mathematical functions...

This may seem like a discussion or opinionated question but I believe that there should be a "correct" answer to this question. I want to know whether lambda calculus is just a notational, or syntactic convention for working with mathematical functions, or whether there are any substantial or semantic differences between lambdas and ordinary functions.

$\endgroup$
  • 2
    $\begingroup$ I don't want to make a full answer out of it, but functions cannot accept functions as inputs. I can write f(g(0)), but I cannot write f(g, 0). The latter is called a "functional," and calls for different rules. $\endgroup$ – Cort Ammon Jun 10 at 21:28
  • $\begingroup$ @CortAmmon functionals are functions. A function is a just a set of pairs (although, strictly speaking, it's a triple (D, R ,G) where D is the domain R is the range and G is the graph (set of pairs), another small issue I have with the accepted answer, but that is neither here nor there). So if D is a set of functions and you take pairs where the first element is a function in D, then you have a function. Check Wikipedia: "A functional is a mapping [function]..." $\endgroup$ – Neil Jun 11 at 10:03
  • $\begingroup$ I.e. All functionals are functions, not all functions are functionals. But all rules that apply to functions apply to functionals $\endgroup$ – Neil Jun 11 at 10:06
63
$\begingroup$

Ironically, the title is on point but not in the way you seem to mean it which is "is the lambda calculus just a notational convention" which is not accurate.

Lambda terms are not functions1. They are pieces of syntax, i.e. collections of symbols on a page. We have rules for manipulating these collections of symbols, most significantly beta reduction. You can have multiple distinct lambda terms that correspond to the same function.2

I'll address your points directly.

First, lambda is not a name that is being reused. Not only would that be extremely confusing, but we don't write $\lambda(x)$ (or $(\lambda\ x)$) which is what we'd do if $\lambda$ was a name for a function, just like we write $f(x)$. In $f(x)$ we could replace $f$ (if it were defined by a lambda term) with the lambda term producing something like $(\lambda y.y)(x)$ meaning $(\lambda y.y)$ is an expression that can represent a function, not a declaration declaring a function (named $\lambda$ or anything else). At any rate, when we overload terminology/notation, it is (one hopes) done in a manner where it can be disambiguated via context, that certainly can't be the case for lambda terms.

Your next point is fine but somewhat irrelevant. This is not a competition where there's Team Lambda Terms and Team Functions, and only one can win. A major application of lambda terms is studying and understanding certain kinds of functions. A polynomial is not a function though we often sloppily identify them. Studying polynomials doesn't mean one thinks that all functions should be polynomials, nor is it the case that polynomials have to "do" something "new" to be worth studying.

Set theoretic functions are not black boxes, though they are entirely defined by their input-output relation. (They literally are their input-output relation.) Lambda terms are also not black boxes and they are not defined by their input-output relation. As I've mentioned before, you can have distinct lambda terms that produce the same input-output relation. This also underscores the fact that lambda terms can't be functions, though they can induce functions.2

In fact, the analogy between polynomials and lambda terms is very close, and I suspect you may not appreciate the distinction between a polynomial and the function it represents, so I'll elaborate a bit.3 Typically when polynomials are introduced, usually with real coefficients, they are treated as real functions of a particular type. Now consider the theory of linear-feedback shift registers (LFSRs). It is largely the theory of (uni-variate) polynomials over $\mathbb F_2$, but if we think of that as a function $\mathbb F_2\to\mathbb F_2$, then there are at most $4$ such functions. There are, however, an infinite number of polynomials over $\mathbb F_2$.4 One way to see this is that we can interpret these polynomials as something other than $\mathbb F_2\to\mathbb F_2$ functions, indeed any $\mathbb F_2$-algebra will do. For LFSRs, we commonly interpret the polynomials as operations on bitstreams, which, if we wanted could be represented as functions $\mathbf{2}^{\mathbb N}\to\mathbf{2}^{\mathbb N}$, though the vast majority of such functions would not be in the image of the interpretation of an LFSR.

This applies to lambda terms as well, we can interpret both of them as things other than functions. They are also both much more tractable objects to work with than the typically uncountably infinite sets of functions. They are both much more computational than arbitrary functions. I can write a program to manipulate polynomials (with coefficients that are computably representable at least) and lambda terms. Indeed, untyped lambda terms are one of the original models of computable functions. This more symbolic/syntactic, calculational/computational perspective is usually more emphasized, especially for the untyped lambda calculus, than the more semantic interpretations of the lambda calculus. Typed lambda terms are far more manageable things and can usually (but not always) easily be interpreted as set theoretic functions, but can also usually be interpreted into an even broader class of things besides functions than the untyped lambda calculus. They also have a rich syntactic theory of their own and a very deep connection to logic.

1 It's possible the issue might go the other way. Maybe you have a misapprehension about what a function is.

2 This is actually not so straightforward. For the untyped lambda calculus, it doesn't really make sense to naively interpret arbitrary lambda terms as set-theoretic functions. You can start to see this when you try to articulate what the domain of the interpretation should be. If I interpret a lambda term as an element of a set $D$, I also want to be able to interpret it as a function on $D$ and into $D$ since I want to interpret application as function application. You end up with $D^D\subseteq D$ (or a weakening of this) which is true only of the singleton set. What we need for the untyped lambda calculus is a reflexive object, and for the category of sets there are no non-trivial reflexive objects. The story is quite a bit different for typed lambda terms, but can still be non-trivial.

3 If you are clear on this distinction, then the analogy should be pretty informative.

4 This issue doesn't occur with fields of characteristic 0, like the complex numbers, reals, rationals, or integers, so the distinction isn't as sharp, though it still exists.

$\endgroup$
  • 8
    $\begingroup$ This is an amazing response I just have to say. Really clears some long misunderstandings for me. Thanks! $\endgroup$ – the0ther Jun 8 at 4:29
  • 4
    $\begingroup$ I wish I could respond to this in detail! Lot's of things I'd like to follow up on. Overall though this was very useful to me, and apparently to a few other people as well, so thank you for the thorough and considered answer. $\endgroup$ – Neil Jun 8 at 9:45
  • 1
    $\begingroup$ There's just one point I'll take issue with here, which is your claim that polynomials don't have to "do" something "new" to be worth studying. Of course they do! Of course, depending on your field, "new" can have different meanings (So eg a pure mathematician will not distinguish between column vectors and row vectors because they are isomorphic, but a statistician may regard the distinction as useful for computation purposes). Any new formalism must justify itself. $\endgroup$ – Neil Jun 8 at 9:45
  • 2
    $\begingroup$ @Neil: Footnote #2 in particular offers some very clear evidence that the lambda calculus "does something new" that "regular" functions "can't do." For a more concrete example of a non-well-founded lambda expression, see fixed-point combinators. The Church numerals also make for fascinating reading, especially the predecessor function. $\endgroup$ – Kevin Jun 8 at 16:06
  • 1
    $\begingroup$ I would add that lambdas as functions don't do anything useful. The only thing you can do with a lambda is to pass it a lambda and it returns a lambda. You have no way to test what the resulting lambda does. You can only pass it another lambda to get another lambda in return. As functions, the set of "lambda functions" behaves exactly like a singleton set containing just the identity function. It is only by considering the input and output of a lambda as expressions that you can differenciate the lambdas. $\endgroup$ – Florian F Jun 9 at 9:40
0
$\begingroup$

Think about the concept of variables. In old languages like basic, you didn't have dynamic allocation and you needed one name for each variable. (This is not perfectly accurate because you had arrays, but the idea is that...) in many problems, you need to be able to allocate as many variable as you want, without being limited by the number of names your program defines.

Lambda functions allows you to get rid of the same limitation about functions names, allowing your program to define as many functions as it needs and "store" them in the sames complex data structures as other variables. This is not something you could do with conventional named functions.

$\endgroup$
  • $\begingroup$ Why can't I do this with conventional named functions? If I write f(x)=let g(y)=x+y in g, every mathematician will instantly know what is meant and agree this is a sensible mathematical object (perhaps up to some quibbles about being clear about the domain of f). They will also be perfectly happy if I then write down the set {f(n) | n ∈ ℕ}, which contains infinitely many functions and in particular isn't limited by only having a finite number of names to use. $\endgroup$ – Daniel Wagner Jun 10 at 19:25
  • $\begingroup$ The question is about lambda calculus. Whilst related, that's not the same thing as lambda functions in programming languages. $\endgroup$ – Andy Dent Jun 11 at 6:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.