|
Peter Møller Neergaard and Harry G. Mairson
LAL is square: Representation and
expressiveness in light affine logic
In Proc. Workshop on Implicit Computational Complexity, July
2002
We focus on how the choice of input-output
representation has a crucial impact on the
expressiveness of so-called “logics of polynomial
time.'' Our analysis illustrates this dependence in
the context of Light Affine Logic (LAL),
which is both a restricted version of Linear Logic,
and a primitive functional programming language with
restricted sharing of arguments. By slightly
relaxing representation conventions, we derive
doubly-exponential expressiveness bounds for this
“logic of polynomial time.'' We emphasize that
squaring is the unifying idea that relates
upper bounds on cut elimination for LAL with lower
bounds on representation. Representation issues
arise in the simulation of
dtime(22^n), where we construct a
uniform family of proof-nets encoding Turing
Machine; specifically, the dependence on n only
affects the number of enclosing boxes. A
related technical improvement is the simulation of
dtime(nk) in depth O(log k) LAL
proof-nets. The resulting upper bounds on cut
elimination then satisfy the properties of a
first-class polynomial Turing Machine
simulation, where there is a fixed polynomial
slowdown in the simulation of any polynomial
computation.
[ bib |
.ps |
.pdf.gz |
.pdf ]
Back
This file has been generated by
bibtex2html 1.61
Copyright notice: The documents contained
in these pages are included by the contributing authors as a means to
ensure timely dissemination of scholarly and technical work on a
non-commercial basis. Copyright and all rights therein are maintained
by the authors or by other copyright holders, notwithstanding that
they have offered their works here electronically. It is understood that all persons copying this information will
adhere to the terms and constraints invoked by each author's
copyright. These works
may not be reposted without the explicit permission of the copyright
holder.
If you experience problems downloading any of the files above,
it is most likely because your browser does not handle compressed
files correctly.
In particular, Netscape might save the file in the compressed
gz-format with extension .ps or
.pdf (indicating postscript or PDF, resp.). You can work around this by saving the file,
renaming it to .ps.gz or .pdf.gz, and then
uncrompress it.
|
