L. Roversi
Flexible Affine Light Logic
Submitted to a journal - a preliminary version has been presented at
the workshop ``LL-Linear Logic'', affiliated to FLoC'02, Copenhagen, 2002
At least two approaches to machine-independent
characterizations of polynomially costing computations exist.
One is purely proof-theoretic. It has been developed by
introducing Light linear logic, and it is based on a careful
control of the expressiveness of the logical rule contraction.
The other approach is recursion-theoretic. It exists in various
forms. Every of them is based essentially on some restrictions
of both a recursion and a composition scheme, with of without
the
help of some typing discipline. Flexible Affine Light Logic
(FALL)
allows to bridge the two approaches. FALL derives from Light
linear
logic. It admits a polynomially costing normalization strategy.
Moreover, there is an inductive embedding of the full system BC
into
FALL, BC being a recursive-theoretic characterization of
poly-time,
by Bellantoni and Cook. So, FALL is expressive enough to
represent
all the feasible computations. The distinguishing feature of
FALL is
that it is a proof-theoretic system that both embodies the quite
restrictive structural constraints a` la Linear logic to control
the
reduction complexity, and keeps such constraints flexible enough
to encode, and simulate, the more programming-oriented terms of
BC.
The paper fully formalizes the structure, and the properties of
FALL.
It also shows the details of the relation with BC, so opening
the
possibility for various comparisons of one approach to feasible
computations vs. the other.
[ bib ]
Back
This file has been generated by
bibtex2html 1.43