Lambda calculus didn't seem abstract. And I can't see the point of it

Problem Detail: 

The underlying question:

What does lambda calculus do for us that we can't do with the basic function properties and notation generally learned in middle school algebra?

First of all, what does abstract mean in the context of lambda calculus? My understanding of the word abstract is something that is divorced from the machinery, the conceptual summary of a concept.

However, lambda functions, by doing away with function names, prevents a certain level of abstraction. For example:

f(x) = x + 2 h(x, y) = x + 5 y 

But even without defining the machinery of these functions, we can easily talk about their composition. For example:

1. h(x, y) . f(x) . f(x) . h(x, y) or  2. h . f . f . h 

We can include the arguments if we want, or we can abstract away completely to give an overview of what's happening. And we can quickly reduce them to a single function. Let's look at composition 2. I can have student layers of detail I can write with depending on my emphasis:

g = h . f . f . h g(x, y) = h(x, y) . f(x) . f(x) . h(x, y) g(x, y) = h . f . f . h = x + 10 y + 4 

Let's perform the above with lambda calculus, or at least define the functions. I'm not sure this is right, but I believe the first and second expressions increment by 2.

(λuv.u(u(uv)))(λwyx.y(wyx))x 

And to multiply by 5y.

(λz.y(5z)) 

Rather than be abstract, this seems to get into the very machinery of what it means to add, multiply, etc. Abstraction, in my mind, means higher level rather than lower level.

Furthermore, I am struggling to see why lambda calculus is even a thing. What is the advantage of

(λuv.u(u(uv)))(λwyx.y(wyx))x 

over

h(x) = x + 5 y 

or a combined notation

Hxy.x+5y 

or even Haskell's notation

h x y = x + 5 * y 

Again, what does lambda calculus do for us that we can't do with the f(x)-style function properties and notation many are familiar with.

Asked By : JDG

Answered By : Hans Hüttel

There are many reasons why the lambda calculus is so important.

A very important reason is the lambda calculus allows us to have a model of computation in which computable functions are first-class citizens.

One cannot express higher-order functions in the language of middle school algebra.

Take as example the lambda expression

$$\lambda f. \lambda g. \lambda x. f(g(x))$$

This simple expression shows us that, within the lambda calculus, function composition is itself a function. In middle school algebra, this is not easily expressed.

In the lambda calculus, it is very easy to express that a function will return a function as its result.

Here is a small example. The expression (where I here assume an applied lambda calculus with addition and integer constants)

$$(\lambda f. \lambda g. \lambda x. f((g(x)))(\lambda x. x+2)$$

will reduce to

$$\lambda g. \lambda x. g(x)+2$$

Notice also that within the lambda calculus, functions are expressions and not definitions of the form $f(x) = e$. This frees us from the need to name functions and to distinguish between a syntactic category of expressions and a syntactic category of definitions.

Also, when it becomes impossible (or just notationally cumbersome) to express higher-order functions, one will also have problems with assigning types to expressions.

Function composition has the polymorphic type

$$\forall \alpha.\forall \beta. \forall \gamma. (\beta \rightarrow \gamma) \rightarrow ((\alpha \rightarrow \beta) \rightarrow \gamma)$$

in the Hindley-Milner type system.

A very strong selling point for the lambda calculus is precise the notion of typed lambda calculus. The various type systems for functional programming languages such as Haskell and the ML family are based on type systems for lambda calculi, and these type systems provide strong guarantees in the form of mathematical theorems:

If a program $e$ is well-typed and $e$ reduces to the residual $e'$, then $e'$ will also be well-typed.

And if $e$ is well-typed, then $e$ will not exhibit certain errors.

The proofs as programs correspondence is particularly noteworthy. The Curry-Howard isomorphism (see e.g. https://www.rocq.inria.fr/semdoc/Presentations/20150217_PierreMariePedrot.pdf) shows that there is a very precise correspondence between the simply typed lambda calculus and intuitionistic propositional logic: To every type $T$ corresponds a logical formula $\phi_T$. A proof of $\phi_T$ corresponds to a lambda term with type $T$, and a beta-reduction of this term corresponds to performing a cut elimination in the proof.

I urge those who feel that middle school algebra is a good alternative to the lambda calculus to develop an account of higher-order, polymorphically typed middle school algebra together with an appropriate notion of Curry-Howard isomorphism. If you can even work out an interactive proof assistant based on middle school algebra that would allow us to prove the many theorems that have been formalized using lambda calculus-based proof assistants such as Coq and Isabelle, that would be even better. I would then start using middle school algebra, and so, I am sure, would many others with me.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/66849