I am having a hard time figuring out the specific relationship, of various things in computability. So we have a hierarchy of machines, with a (real life) upper bound of Turing machines, moving on down to things like deterministic finite automata. We also have a hierarchy of grammars that the machines can implement. These grammars range from recursively enumerable down to things like regular grammars. By implement I mean be configured in such a way that they either accept a string or declare it not part of the language.

The lambda calculus has a grammar. This grammar can be expressed on a low class of machine. The lambda calculus itself though is Turing complete. Clearly the syntax of the lambda calculus has no relationship to the power classification.

While the full lambda calculus is Turing complete you can restrict it in certain ways so that the syntax is the same, but the calculus becomes no longer Turing complete. This is talked about in the Turner paper:


You could restrict it more, and make it an even weaker machine, until nothing can be expressed. As the version of lambda calculus you are programming in becomes weaker, and weaker, fewer grammars could be implemented.

Noting that the syntax is the same: Given a string representing a lambda expression X. Depending on the content of X only certain classes of restricted lambda calculus (to un-restricted) may be able to execute it. If the expression X requires a Turing machine to implement then a machine restricted to a weaker lambda calculus would not be able to express it.

Is it possible to determine what class of machine is required to express a given lambda expression? Turner in his paper clearly shows that you can restrict the lambda calculus to not require a Turing machine. But just given the expression, can you determine the class of machine?

  • $\begingroup$ Probably any reasonable rigorous formulation of this question would be undecidable. $\endgroup$ Jan 11, 2016 at 7:32
  • 1
    $\begingroup$ Please give a full reference to "the Turner paper" that is robust against link rot. $\endgroup$
    – Raphael
    Jan 11, 2016 at 7:36

1 Answer 1


Paraphrasing, this seems to be your question:

Given an unrestricted λ-term, can I determine what kind of automaton/machine model I need to express it?

Such properties are inherently undecidable (usually). Starting with a Turing-complete formalism, Rice's theorem immediately tells you that what you are asking is impossible.

The set of TMs/λ-terms corresponding to any non-empty, non-Turing-complete machine model forms a non-trivial index set and is thus is never decidable.

Of course, if you restrict yourself to a less than Turing-complete base set of terms, Rice's theorem does no longer apply. This is still a tough question to ask, though, even at lower levels of the hierarchy. For instance, it is undecidable if an NPDA accepts a DCFL, if a context-free grammar describes a regular language, or even if a context-free grammar is equivalent to a fixed regular grammar.


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.