要旨
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.
