# MPI-I-1999-3-001

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

### Vorobyov, Sergei

**MPI-I-1999-3-001**. July** **1999, 20 pages. | Status:** **available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:

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.

Acknowledgement:** **

References to related material:

To download this research report, please select the type of document that fits best your needs. | Attachement Size(s): |

| 428 KBytes |

Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView |

**URL to this document: **http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1999-3-001

**BibTeX**
`@TECHREPORT{``Vorobyov99``,`

` AUTHOR = {Vorobyov, Sergei},`

` TITLE = {New lower bounds for the expressiveness and the higher-order Matching problem in the simply typed lambda calculus},`

` TYPE = {Research Report},`

` INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},`

` ADDRESS = {Stuhlsatzenhausweg 85, 66123 Saarbr{\"u}cken, Germany},`

` NUMBER = {MPI-I-1999-3-001},`

` MONTH = {July},`

` YEAR = {1999},`

` ISSN = {0946-011X},`

`}`