Hacker News new | ask | show | jobs
by leshow 2498 days ago
Stupid question, why is it often written "_the_ lambda calculus" and not just "lambda calculus"
4 comments

A calculus is a system for calculation, so traditionally a specific system for calculation is named as the X calculus: the integral calculus, the pi calculus, the lambda calculus, the situation calculus, etc.

As a loose analogy, think of how specific instances of the general idea of systems are named: the court system, the cooling system, the moderation system, etc. Some uses are a bit archaic though, e.g. people now usually refer to integral calculus as a standalone name, without the definite article. I think we're somewhere in between with (the) lambda calculus; you can find papers that use "the" and others that don't.

there are many lambda calculi.

Here's two:

A) Pure Lambda Calculus is defined by

1. the terms (metavariables t and u): λx.t | x | (t u)

2. the reduction rules, β

3. the two conversion rules, α and η

B) Another of Church's lambda calculus, defined by

1. the terms (metavariables t and u): λx.t | x | (t u)

2. the reduction rule, β

3. the conversion rule, α.

You might go .. wait, these are the same! They are not. Without the η rule, you cannot define extensional equivalence, thus you cannot do things like referential transparency.

There are a number of shortcomings with the pure lambda calculus of course, so over the years people have added things , creating variations of lambda calculi.

A particularly famous one is System F. System F extends the Simply Typed Lambda Calculus (which itself is an extension of the pure lambda calculus) with type generators and eliminators. The trick is to make the language of types into terms of the lambda calculus itself.

System F begets SML, SML(NJ), Ocaml, Haskell and F#.

Then you have the other extensions along Barendregt's Lambda Cube. You get things like Coq and Agda and Idris, which are extensions of System F in the same directions but different ways of constructing them.

On the other side of things people are trying to make sense of the pure lambda calculus itself. There exists a whole subindustry of people explaining substitutions (lambda calculi with explicit substitution), people explaining self interpretation which you can do in lisp but not really in pure lambda calculus (first clean attempt was in 1995!). There are people developing or splitting pure lambda calculus into two subsets - example are people who work with sequent calculus.

All these systems are lambda calculi. When people say _the_ lambda calculus then they usually mean the pure lambda calculus.

Probably for the same reason that some people refer to regular calculus as "the calculus".
You'll always sound smart if you remember that "maths" is plural and one of them is "the calculus".
Maths is the common spelling and pronunciation in standard British English, though.
There are many calculi
Because there's only one.

E.g. If we meet aliens someday their Lambda Calculus will be the same as ours. Just like their integers will be the same as ours.

> Just like their integers will be the same as ours

"The one, the two, the three, the four,...."