15
$\begingroup$

AFAIK, The first evidence of using higher order functions goes back to Schönfinkel's 1924 paper: "On the Building Blocks of Mathematical Logic" - where he allowed one to pass functions as arguments to other functions.

That seems interesting. However, everything that I've been reading about his work (and Curry's by extension) seems to allude to one thing in some form or the other: [higher order functions]...this eliminates the need for bound variables...

What I haven't been able to wrap my head around is - what's the big deal? Why did logicians and mathematicians of that time care about this? And do we as theoreticians, care about this today? Why was it "groundbreaking" to get rid of bound variables and what impact did (or does) it have on computing (theoretically) as we know it?

PS: I'm aware of how his work paved way for $\lambda$-calculus and the impact of "it" on computing and functional programming in general. My question is mostly directed to the time "prior" to the creation of $\lambda$-calculus and "after" Schönfinkel's paper. The fact the Curry independently picked up that line of work, which was later known as "combinatory logic" too alludes to the importance of Schönfinkel's work.

$\endgroup$
  • 2
    $\begingroup$ Schönfinkel's paper can be found here. $\endgroup$ – Martin Berger Feb 14 '15 at 10:39
17
$\begingroup$

TL;DR. The metamathematics of binding are subtle: they seem trivial but aren't — whether you deal with (higher-order) logics or 𝜆-calculus. They're so subtle that binding representations form an open research field, with a competition (the POPLmark challenge) some years ago. There are even jokes by people in the field about the complexity of approaches to binding.

So, if you care about metamathematics (and most mathematicians don't), you need to deal with binding. But many mathematicians can safely treat the formalization of binding as if it were a "foundational" problem.

Another point is that binding was the only "new" problem in languages with higher-order functions, because the theory of languages with binding is just algebra (for constants) + binding. Mitchell's "Foundations of Programming Languages" actually presents things in this order and is rather enlightening.

I'm aware of how his work paved way for λ-calculus and the impact of "it" on computing and functional programming in general. My question is mostly directed to the time "prior" to the creation of λ-calculus and "after" Schönfinkel's paper.

I must be missing something, but this remark seems to make no difference. Binding in higher-order logics and binding in λ-calculus seem as hard, so as long as people cared about higher-order logics, they had to deal with binding. I'm biased by using Curry-Howard-isomorphism-based theorem provers that implement logic by simply implementing a type theory (where types are formulas and programs are proof terms), so that I just deal with binding once.

On the other hand, IIRC, at the time indeed few cared about Schönfinkel's work — partly because of how he (didn't) publish it — the papers were mostly written by colleagues based on the research he did (see here, page 4); Curry then rediscovered the theory independently.

Caveat: I'm not an historian, but a PhD student in PL, so mine is a modern (and hopefully accurate) perspective on the topic.

EDIT:

Why is binding subtle, a bit more concretely

There are two facets to it — first, implementing it is hard. Secondly, metamathematics is the mathematics of proof manipulation: this manipulation is typically automatic, that is, it's an algorithm — so essentially, you face all the difficulties of implementation, plus making proofs about them. Below I give examples. The examples have a modern perspective — they are about actually formalized proofs. However, some of the difficulties would extend to accurate manual proofs — as long as you don't cheat on details.

This shows that Schönfinkel simply gave the first solution to this problem, but this was far from definitive.

Implementing it is subtle because of shadowing

The basic problem in implementation is shadowing. Usually one doesn't reuse the same name for different bound variables. But you can't avoid it in lambda calculus, at least because functions (and their bound variables) are duplicated: $(\lambda f. f~1 + f~2) (\lambda x . x)$ reduces to $(\lambda x . x)~1 + (\lambda x . x)~2$. This isn't a problem yet, but starting from $(\lambda f x. f (f x))\ (\lambda g y . g~y)\ z$ gives you $(\lambda g y . g~y)\ (\lambda g y . g~y)\ z$ and then $(\lambda y . (\lambda g y . g~y)~y)\ \ z$: now you need to deal with shadowing. You can avoid this, at the cost of complicating the beta-reduction rule.

Once you have different variables with the same name, you also need to prevent capture. The simplest example of capture is that applying the function $\lambda x y. x$ (return first argument) to $y$ must not give $\lambda y. y$ (the identity function), but $\lambda y'. y$ (a constant function).

What's worse is that the counterexamples to naive algorithms are hard to construct when you know the problem already, let alone when you don't. Bugs in almost correct algorithms often lie undetected for years. I hear that even good students typically fail to come up (on their own) with the correct definition of capture-avoiding substitution. In fact, PhD students (me included) and professors aren't exempt from these problem.

That's one reason why some (including one of the best textbooks on programming languages, Types and Programming Languages by Benjamin Pierce) recommend nameless representation (not quite combinatory logic, even though it has been used, but rather deBrujin indexes).

Proofs about it are subtle

It turns out that proofs about binding are no simpler than the implementation, as mentioned above. Of course, correct algorithms exist, and proof about them exist — but without advanced machinery, for each language using binding you need to repeat the proofs, and those proofs are simply very big and annoying if you use the definitions for binding on pen and paper.

To exemplify algorithms involved in metamathematics, consider the deduction theorem in logics, that allows composing a proof of $B$ assuming $A$ and a proof of $A$ to get a proof of $B$. To prove that theorem, you actually exhibit an algorithm that works on the syntax of the two proofs involved and produces the syntax for a proof of $B$. This algorithm needs to deal with binding.

Next, I looked up my best example of "what goes wrong if you try formalizing the standard definition". Russell O’Connor (who's on this site) formalized the first Gödel's incompleteness theorem in Coq (a theorem prover of the kind mentioned above) — and that theorem involves a logic (with all the relevant algorithms) in another logic (with the syntax of the first logic coded as numbers). He used the definitions which are used on paper and formalized them directly. Search for "substitution" or "variable" and count how often they appear in reference to problems to get an impression. http://r6.ca/Goedel/goedel1.html

I never use those definitions in my work, but each alternative approach has some downside.

$\endgroup$
  • $\begingroup$ I'm biased by using Curry-Howard-isomorphism-based theorem provers, so that I just deal with binding once - Could you please elaborate what you mean? $\endgroup$ – PhD Feb 14 '15 at 18:24
  • 3
    $\begingroup$ You do say it's subtle but never say what exactly makes it so and why care about it if you're a metamathetician? That's the perspective I'm looking for. $\endgroup$ – PhD Feb 14 '15 at 18:27
  • $\begingroup$ On your first comment: I made explicit the connection to Curry-Howard, but I'll have to refer you to Wikipedia or another question. I agree with your second comment; I'll elaborate for people unfamiliar with lambda calculus. $\endgroup$ – Blaisorblade Feb 14 '15 at 23:00
  • $\begingroup$ @PhD: I hope what I added helps a bit, though it doesn't replace a good lecture on this material (and unfortunately, the material I've cut across is typically distributed among lots of other PPL-related material). $\endgroup$ – Blaisorblade Feb 15 '15 at 9:36
  • 1
    $\begingroup$ Thanks a ton! That was indeed helpful. This link may interest you too: home.uchicago.edu/~wwtx/Varfreelogic_revised.pdf - First order logic without bound variables. $\endgroup$ – PhD Feb 15 '15 at 18:27

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.