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

Author Kazushige Terui

Thumbnail PDF


  • Filesize: 0.58 MB
  • 16 pages

Document Identifiers

Author Details

Kazushige Terui

Cite AsGet BibTex

Kazushige Terui. Semantic Evaluation, Intersection Types and Complexity of Simply Typed Lambda Calculus. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 323-338, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


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.
  • simply typed lambda calculus
  • computational complexity
  • denotational semantics
  • intersection types


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail