Roversi:2008WALTSRNCOMPL (Technical report)

Author(s)  Luca Roversi 
Title  « Weak Affine Light Typing is complete with respect to Safe Recursion on Notation » 
Number  104/08 
Institution  Dipartimento di Informatica, Torino 
Year  2008 
Address  C.so Svizzera, n.185  10149 Torino  Italy 
URL  http://arxiv.org/abs/0804.0660 
Abstract 
Weak affine light typing (WALT) assigns light affine linear formulae as types to a subset of $\lambda $terms of System F. WALT is polytime sound: if a $\lambda $term $M$ has type in WALT, $M$ can be evaluated with a polynomial cost in the dimension of the derivation that gives it a type. The evaluation proceeds under any strategy of a rewriting relation which is a mix of both callbyname and callbyvalue $\beta $reductions. WALT weakens, namely generalizes, the notion of ``stratification of deductions'', common to some Light Systems  those logical systems, derived from Linear logic, to characterize the set of Polynomial functions  . A weaker stratification allows to define a compositional embedding of Safe recursion on notation (SRN) into WALT. It turns out that the expressivity of WALT is strictly stronger than the one of the known Light Systems. The embedding passes through the representation of a subsystem of SRN. It is obtained by restricting the composition scheme of SRN to one that can only use its safe variables linearly. On one side, this suggests that SRN, in fact, can be redefined in terms of more primitive constructs. On the other, the embedding of SRN into WALT enjoys the two following remarkable aspects. Every datatype, required by the embedding, is represented from scratch, showing the strong structural prooftheoretical roots of WALT. Moreover, the embedding highlights a stratification structure of the normal and safe arguments, normally hidden inside the world of SRNnormal/safe variables: the less an argument is ``polyomially impredicative'', the deeper, in a formal, prooftheoretical sense, it is represented inside WALT. Finally, since WALT is SRNcomplete it is also polynomialtime complete since SRN is. 
@techreport{Roversi:2008WALTSRNCOMPL,
number = {104/08},
month = {April},
author = {Roversi, Luca},
url = {http://arxiv.org/abs/0804.0660},
title = {{W}eak {A}ffine {L}ight {T}yping is complete with respect to {S}afe
{R}ecursion on {N}otation},
address = {C.so Svizzera, n.185  10149 Torino  Italy},
abstract = {Weak affine light typing (\textsf{WALT}) assigns light affine
linear formulae as types to a subset of $\lambda$terms of
\textsf{System F}. \textsf{WALT} is polytime sound: if a
$\lambda$term $M$ has type in \textsf{WALT}, $M$ can be evaluated
with a polynomial cost in the dimension of the derivation that
gives it a type. The evaluation proceeds under any strategy of a
rewriting relation which is a mix of both callbyname and
callbyvalue $\beta$reductions. \textsf{WALT} \textit{weakens},
namely \textit{generalizes}, the notion of
``\textit{stratification of deductions}'', common to some
\textsf{Light Systems}  those logical systems, derived from
Linear logic, to characterize the set of Polynomial functions 
. A weaker stratification allows to define a compositional
\textit{embedding} of Safe recursion on notation (\textsf{SRN})
into \textsf{WALT}. It turns out that the expressivity of
\textsf{WALT} is strictly stronger than the one of the known
\textsf{Light Systems}. The embedding passes through the
representation of a subsystem of \textsf{SRN}. It is obtained by
restricting the composition scheme of \textsf{SRN} to one that can
only use its safe variables \textit{linearly}. On one side, this
suggests that \textsf{SRN}, in fact, can be redefined in terms of
more primitive constructs. On the other, the \textit{embedding} of
\textsf{SRN}\ into \textsf{WALT} enjoys the two following
remarkable aspects. Every datatype, required by the embedding, is
represented from scratch, showing the strong structural
prooftheoretical roots of \textsf{WALT}. Moreover, the embedding
highlights a stratification structure of the normal and safe
arguments, normally hidden inside the world of
\textsf{SRN}normal/safe variables: the less an argument is
``polyomially impredicative'', the deeper, in a formal,
prooftheoretical sense, it is represented inside \textsf{WALT}.
Finally, since \textsf{WALT} is \textsf{SRN}complete it is also
polynomialtime complete since \textsf{SRN} is.},
institution = {Dipartimento di Informatica, Torino},
year = {2008},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)