Peter Møller Neergaard and Harry G. Mairson
How light is safe recursion?
Translations between logics of polynomial time
Unpublished note, 2003
We investigate the simulation of Bellantoni and
Cook's function algebra BC by Girard's Light Linear
Logic LAL (as amended by Asperti). Both of these
languages characterize exactly the polynomial time
functions. Given a ptime function f
described in BC program phif, how can we
translate phif into LAL? The best known
translation, due to Murawski and Ong, compiles only
the linear fragment bc-, where
safe variables cannot be shared. We show that
this fragment can be evaluated in
logspace. Next, we prove that extensions
of their approach to the full BC algebra, as well as
any translation that interprets integers and
primitive recursion via their standard, System
F-inspired inductive type coding, cannot provide a
correct translation into LAL. Finally, we provide a
correct translation, based on generalizing Turing
machine simulations into an SECD compiler, realized
in LAL. We further elaborate this translation so
that it is compositional on the BC combinators.
[ 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.
