de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
  New lower bounds for the expressiveness and the higher-order Matching problem in the simply typed lambda calculus

Vorobyov, S.(1999). New lower bounds for the expressiveness and the higher-order Matching problem in the simply typed lambda calculus (MPI-I-1999-3-001). Saarbrücken: Max-Planck-Institut für Informatik.

Item is

Basic

show hide
Item Permalink: http://hdl.handle.net/11858/00-001M-0000-0014-6F4C-1 Version Permalink: http://hdl.handle.net/11858/00-001M-0000-0014-7A67-0
Genre: Report

Files

show Files
hide Files
:
1999-3-001 (Any fulltext), 11KB
Description:
-
Visibility:
Public
MIME-Type / Checksum:
text/html / [MD5]
Technical Metadata:
Copyright Date:
-
Copyright Info:
-
License:
-

Locators

show

Creators

show
hide
 Creators:
Vorobyov, Sergei1, Author              
Affiliations:
1Reaktive und Hybride Systeme, escidoc:40045              

Content

show
hide
Free keywords: -
 Abstract: 1. We analyze expressiveness of the simply typed lambda calculus (STLC) over a single base type, and show how k-DEXPTIME computations can be simulated in the order k+6 STLC. This gives a double order improvement over the lower bound of [Hillebrand \& Kanellakis LICS'96], reducing k-DEXPTIME to the order 2k+3 STLC. 2. We show that k-DEXPTIME is linearly reducible to the higher-order matching problem (in STLC) of order k+7. Thus, order k+7 matching requires (lower bound) k-level exponential time. This refines over the best previously known lower bound (a stack of twos growing almost linearly, O(n / log(n)) in the length of matched terms) from [Vorobyov LICS'97], which holds in assumption that orders of types are UNBOUNDED, but does not imply any nontrivial lower bounds when the order of variables is FIXED. 3. These results are based on the new simplified and streamlined proof of Statman's famous theorem. Previous proofs in [Statman TCS'79, Mairson TCS'92, Vorobyov LICS'97] were based on a two-step reduction: proving a non-elementary lower bound for Henkin's higher-order theory Omega of propositional types and then encoding it in the STLC. We give a direct generic reduction from k-DEXPTIME to the STLC, which is conceptually much simpler, and gives stronger and more informative lower bounds for the fixed-order STLC, in contrast with the previous proofs.

Details

show
hide
Language(s): eng - English
 Dates: 1999
 Publication Status: Published in print
 Pages: 20 p.
 Publishing info: Saarbrücken : Max-Planck-Institut für Informatik
 Table of Contents: -
 Rev. Method: -
 Identifiers: URI: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1999-3-001
Report Nr.: MPI-I-1999-3-001
BibTex Citekey: Vorobyov99
 Degree: -

Event

show

Legal Case

show

Project information

show

Source 1

show
hide
Title: Research Report / Max-Planck-Institut für Informatik
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: - Identifier: -