Terui, Kazushige
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 nEXPTIME complete for r=2n+2, and nEXPSPACE 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.
BibTeX  Entry
@InProceedings{terui:LIPIcs:2012:3501,
author = {Kazushige Terui},
title = {{Semantic Evaluation, Intersection Types and Complexity of Simply Typed Lambda Calculus}},
booktitle = {23rd International Conference on Rewriting Techniques and Applications (RTA'12) },
pages = {323338},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897385},
ISSN = {18688969},
year = {2012},
volume = {15},
editor = {Ashish Tiwari},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2012/3501},
URN = {urn:nbn:de:0030drops35012},
doi = {10.4230/LIPIcs.RTA.2012.323},
annote = {Keywords: simply typed lambda calculus, computational complexity, denotational semantics, intersection types}
}
2012
Keywords: 

simply typed lambda calculus, computational complexity, denotational semantics, intersection types 
Seminar: 

23rd International Conference on Rewriting Techniques and Applications (RTA'12)

Issue date: 

2012 
Date of publication: 

2012 