Semantic Evaluation, Intersection Types and Complexity of Simply Typed Lambda Calculus

Abstract

Consider the following problem: given a simply typed lambda term of Boolean type and of order r, does it normalize to "true"? A related problem is: given a term M of word type and of order r together with
a finite automaton D, does D accept the word represented by the normal form of M? We prove that these problems are n-EXPTIME complete for r=2n+2, and n-EXPSPACE complete for r=2n+3.

While the hardness part is relatively easy, the membership part is not so obvious; in particular, simply applying beta reduction does not work. Some preceding works employ semantic evaluation in the category of sets and functions, but it is not efficient enough for our purpose.

We present an algorithm for the above type of problem that is a fine blend of beta reduction, Krivine abstract machine and semantic evaluation in a category based on preorders and order ideals, also known as the Scott model of linear logic. The semantic evaluation can also be presented as intersection type checking.