# Given a λ-term, can I decide which machine model I need to express it?

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?

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