3
$\begingroup$

Automata theory is mainly concerned with Turing machines and all its relatives-in-spirit. $\lambda$-calculus is rather rarely mentioned in textbooks on automata theory.

What's the common name of the theory mainly concerned with $\lambda$-calculus and its relatives? (I think, "mathematical logic", "computability theory", "programming language theory" and "recursion theory" are too general, compared to "automata theory". But there should be an "$\lambda$-theory", shouldn't it?)

Improve this question
$\endgroup$
10
  • 1
    $\begingroup$ What's wrong with just calling it "lambda calculus"? $\endgroup$
    – Qiaochu Yuan
    Commented Jan 15, 2010 at 12:25
  • 2
    $\begingroup$ Because it's too specific: I think of "lambda calculus and its relatives". And "lambda" is just an artificial word, other than "automata", "computability", and so on. $\endgroup$
    – Hans-Peter Stricker
    Commented Jan 15, 2010 at 12:29
  • $\begingroup$ Maybe one could call it "function theory" if this name wasn't already in use. $\endgroup$
    – Hans-Peter Stricker
    Commented Jan 15, 2010 at 12:31
  • $\begingroup$ Anything wrong with "functional programming" besides the fact that it's a computer science term? $\endgroup$
    – François G. Dorais
    Commented Jan 15, 2010 at 13:59
  • 2
    $\begingroup$ That would never stick unless there's another good reason. Besides, the schism between cs and math is very recent, I would contend that "functional programming" is actually a math term, historically speaking. More importantly, it would be wrong to use a term different than those who use it most, namely theoretical computer scientists, who are very competent mathematicians by the way. $\endgroup$
    – François G. Dorais
    Commented Jan 15, 2010 at 14:22

5 Answers 5

Reset to default
4
$\begingroup$

"combinatory logic"

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ I should have known this, since I'm a long-time fan of Raymond Smullyan. How could I have overseen this! Thanks. (To say the least: it's an established name.) $\endgroup$
    – Hans-Peter Stricker
    Commented Jan 15, 2010 at 16:10
  • $\begingroup$ No problem. I've been using lambda calculus in various forms for twelve years now and it wasn't until recently that I felt I really understood the connection to combinators. $\endgroup$
    – Adam
    Commented Jan 15, 2010 at 20:57
6
$\begingroup$

In recent years almost anything I have read about lambda calculus has been about typed lambda calculus. Broadly speaking, I think computer scientists would say that these papers were part of the field known as Type Theory.

If that doesn't quite fit what you want I'd suggest reading the PLT article on Wikipedia.

For example, there is a family of lambda calculi that can be arranged in what is known as the lambda cube. The wikipedia article starts "In mathematical logic and type theory..."

Improve this answer
$\endgroup$
1
  • 2
    $\begingroup$ Should qualify: constructive type theory. $\endgroup$
    – Charles Stewart
    Commented Jan 15, 2010 at 20:34
6
$\begingroup$

I don't know of one that seems sufficiently general. The theory's at an intersection:

  1. It (in its untyped guise) is one of the four most important Turing-complete computation systems;
  2. It is algebraically natural, connected fundamentally to Cartesian-closed categories (though with horrid baggage around $\alpha$-equivalence);
  3. It is a foundational theory, possibly the theory that best captures the notion of schematic function; and
  4. It plays an important role in philosophical logic, due to its link to natural deduction, which is among the few treatments of formal logic that is relevant to the actuality of how we reason.

Maybe a name formed out of keywords from several of these domains would give a suitable term? How about Cartesian function-calculus?

Edited

Improve this answer
$\endgroup$
2
$\begingroup$

Untyped Lambda Calculus is part of the Recursion Theory, I would say. Typed Lambda Calculus is Type Theory, and is connected with constructive mathematics.

The Lambda-Calculus is a concept that can be applied to many parts of mathematics, so there are few books especially about Lambda-Calculus (Imho lambda calculus : logic = measure theory : analysis, sort of). And the ones I know (i.e. Barendregt, etc.) are just referring to it as "Lambda Calculus".

Improve this answer
$\endgroup$
0
$\begingroup$

The lambda calculus is considered one of the fundamental topics in Theoretical Computer Science. You can study it from many points of view:

  1. If you study its denotational semantics, then you use algebra and category theory.
  2. If you study its operational semantics, then you mainly use rewriting theory.
  3. If you study logic, then you will be interested in its type system. You may also be interested in the related system of combinatory logic.
  4. If you are a functional programmer, then you are using lambda calculus as a Turing-complete formalism.
  5. If you study the foundations of mathematics, then the lambda calculus is related to many foundational systems: Illative combinatory logic, Map Theory, Type Theory, ...

However the term "lambda-theory" is already reserved for a very specific concept: a lambda-theory is a congruence on the set of lambda-terms that contains alpha-beta conversion.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .