teaching lambda calculus early

[gusl]

I wonder... if we taught lambda calculus to high schoolers / college freshmen, wouldn't that be an excellent way to give them (1) skills to express themselves precisely, and (2) familiarity with abstract concepts?

As an added benefit, when they become instructors someday, they'll be able to write their textbooks and homeworks in a way that is unambiguous (all mathematical questions can be translated into questions about the output of a single computer program).

I think that most of the confusions experienced by people studying math (regardless of level) are about variable binding, quantifier scope, etc. I have a BS degree in math (and a Master's in logic), and most of my confusions are of this type also, when I'm learning unfamiliar math.

Isn't the meaning of the word "abstraction" fully captured by lambda abstraction?

The idea of first-class functions is all about turning verbs into nouns... Function calls are usually understood as applying a verb to a list of nouns. Dealing with first-class functions involves changing (extending) metaphors: now, functions can be objects too, i.e. verbs can be nouns too. This may be related to the fact that computer scientists like making nouns out of verbs, verbs out of adjectives, etc.

The extended metaphor may be that functions are "machines": they do something but they can also be fed into other machines.

---

Tangentially, Kiczales's class has interesting reading: Lucy Suchman - Human Machine Reconfigurations

Comments

[fancybred.livejournal.com]

Actually, we should teach lambda calculus in kindergarten!

Seriously, though, I think it makes sense to teach lambda calculus somewhere between basic algebra and basic calculus.

[gustavolacerda.livejournal.com]

The author, Bret Victor, seems to have a lot of interesting ideas! How did you find his site?

[fancybred.livejournal.com]

Links to the game were going around about a year ago. I saw it on Lambda the Ultimate and Phil Wadler's blog.

[chrisamaphone]

there's also this

[chrisamaphone]

I think that most of the confusions experienced by people studying math (regardless of level) are about variable binding, quantifier scope, etc.

yesyesyesyesyes

i dispute that everything "abstraction" means is captured in lambda abstraction. for one, there are so many other things one can abstract over. but it's definitely a very good introduction to the idea of abstraction, which i think is sorely sorely missing in high school education and earlier.

[gustavolacerda.livejournal.com]

it's nice to get some affirmation.

[gustavolacerda.livejournal.com]

yeah, right after I wrote that, I thought of the \Pi abstraction (i.e. \forall on the other side of C-H).

[chrisamaphone]

∀ as (old school) logicians normally use it isn't quite LF Π; in most of what i've seen, it quantifies over "objects" from some "domain" that is distinct from proof terms for propositions in the logic.

[simrob.livejournal.com]

I would like to second that yesyesyesyesyes

[bhudson.livejournal.com]

Most?

It's an important concept in discrete math, to be sure, but even there I'm not sure that "most" is quite right. There's plenty of other confusions to go around, and lambda calculus isn't confusion-free on its own.

That said, I think the lambda calculus (and various other bits of computer science) is probably a good thing to teach early, though perhaps less abstractly than in the standard university course. A lot of people (hi!) don't really get off on the pure beauty of it all and need to be engaged in other ways.

[chrisamaphone]

i also wrote out a rambly complaint about your verb/noun analogy but i think it was dumb and i'm actually just bothered because i don't like it when anyone tries to make analogies about math.

[gustavolacerda.livejournal.com]

but math is all about analogies!

[bhudson.livejournal.com]

Analogy is for when you know there's an abstraction but you can't quite explain it (either because you don't know how, or because it's stylistically clumsy), so you just show an example of something else, preferably prima facie quite different, that also meets the abstraction.