License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2012.323
URN: urn:nbn:de:0030-drops-35012
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2012/3501/
Go to the corresponding LIPIcs Volume Portal

Terui, Kazushige

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

pdf-format:
24.pdf (0.6 MB)

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.

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 =	{323--338},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Ashish Tiwari},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2012/3501},
  URN =		{urn:nbn:de:0030-drops-35012},
  doi =		{10.4230/LIPIcs.RTA.2012.323},
  annote =	{Keywords: simply typed lambda calculus, computational complexity, denotational semantics, intersection types}
}

Keywords: simply typed lambda calculus, computational complexity, denotational semantics, intersection types
Collection: 23rd International Conference on Rewriting Techniques and Applications (RTA'12)
Issue Date: 2012
Date of publication: 29.05.2012

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI