0
$\begingroup$

It is well known that all computable functions can be expressed as terms of the lambda calculus and computed according to its rules. It is also more or less obvious that many classical formal languages (i.e. languages with formalized semantics) can be translated into the lambda calculus (e.g. using a Church encoding). I am, however, pretty sure that there are languages where such a translation is not possible, the simplest example would be a language with a builtin primitive that solves the Halteproblem.

That makes me wonder if there is an established terminus for the languages that can be translated.

Is there a name for the class of languages that can be translated (correctly, completely) into the lambda calculus?

Improve this question
$\endgroup$
5
  • 1
    $\begingroup$ turing-complete? $\endgroup$
    – Euge
    Commented Feb 25, 2017 at 14:46
  • 1
    $\begingroup$ @Euge No, since languages that are weaker than Turing complete can also be translated into lambda calculus. $\endgroup$
    – David Richerby
    Commented Feb 25, 2017 at 17:19
  • 1
    $\begingroup$ @Euge Oh, but the question title asks about equivalence with the lambda calculus, and those languages are the Turing-complete. $\endgroup$
    – David Richerby
    Commented Feb 25, 2017 at 18:22
  • $\begingroup$ What does "translate into lambda calculus" mean? $\endgroup$
    – Andrej Bauer
    Commented Feb 25, 2017 at 19:51
  • $\begingroup$ @Andrej: translation into lambda calculus means to define a function that takes as input terms of the language and yields lambda terms. This translation should be equivalent in a suitable sense (the precise definition of "equivalent" depends on the source language). Usually, one asks for some form of observational equivalence. $\endgroup$
    – choeger
    Commented Feb 26, 2017 at 13:33

1 Answer 1

Reset to default
5
$\begingroup$

The lambda calculus is exactly equivalent in expressive power to Turing machines, so the languages that can be translated into it are exactly those that are no more powerful than Turing machines.

Models of computation that are more powerful than Turing machines are known as "hypercomputation". However, except for computability theorists, most people don't ever consider languages that can express hypercomputation, so most people don't need a word that "not capable of hypercomputation." It's a bit like there being no word for "food that isn't poisonous" because not being poisonous is the default state for food so people don't really need a word for that.

Your question title asks about languages that are equivalent to the lambda calculus, i.e., those where we can translate in both directions. Because the lambda calculus has the same power as Turing machines, these are exactly the Turing-complete languages.

Improve this answer
$\endgroup$
1
  • $\begingroup$ By the way, what would be a precise definition of "language" and "equivalent" and "translate" in this context? I am aware of several possibilities, not all of which will yield the expected result. $\endgroup$
    – Andrej Bauer
    Commented Feb 25, 2017 at 19:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.