Is Lambda Calculus purely syntactic?

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.

Answer

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 λ(x) (or (λ x)) which is what we’d do if λ 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 (λy.y)(x) meaning (λy.y) is an expression that can represent a function, not a declaration declaring a function (named λ 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 F2, but if we think of that as a function F2F2, then there are at most 4 such functions. There are, however, an infinite number of polynomials over F2.4 One way to see this is that we can interpret these polynomials as something other than F2F2 functions, indeed any F2-algebra will do. For LFSRs, we commonly interpret the polynomials as operations on bitstreams, which, if we wanted could be represented as functions 2N2N, 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 DDD (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.

Attribution
Source : Link , Question Author : Neil , Answer Author : Derek Elkins left SE

Leave a Comment