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

Question

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:

"https://uf-ias-2012.wikispaces.com/file/view/turner.pdf/401400700/turner.pdf".

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?

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.