There seems to be an interesting model of computation involved in determining whether a term from some programming language has any free variables. It's a tree traversal that seems almost like the process to recognize a context-free language, but it requires a little more information: the set of variables in scope at any point. At the same time, though, recognizing such a language doesn't seem complicated enough to require the full power a Turing machine. I suspect that type-checking and other kinds of reasoning we do about programs could also be phrased in terms of a model like this.

I'd like to come up with a crisp definition for this kind of tree-traversal process. I'm hoping that there's a class of automata that are known to solve just this kind of problem. I'm focusing on finding closed terms of the untyped lambda calculus because that seems like the simplest instance of this problem.

Is there a well-known class of automata below Turing machines that can recognize closed terms of the lambda calculus? And/or is there a well-known class of languages below recursively enumerable that contains "the set of all closed lambda-calculus terms" as a language?

I know that context-sensitive languages are a level in between context-free and recursively enumerable languages, and that there are various classes called "mildly context-sensitive", but I don't know enough about those to say whether they fit the requirements here.

  • $\begingroup$ The chomsky higharchy is exactly Regular -> Context Free -> Context Sensitive -> Recursive(ly Enumerable). Context Sensitive grammers exist and they define context sensitive languages which are recognized by linear bounded automaton: en.wikipedia.org/wiki/Linear_bounded_automaton Basically its those things that can be recognized by a turing machine in O(n) space $\endgroup$
    – Jake
    Nov 27 '20 at 19:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.