Roversi:2007WALTFULL (Technical report)

Author(s)  Luca Roversi 
Title  « Weak Affine Light Typing: Intensional expressivity, Polytime soundness and completeness » 
Number  103/07 
Institution  Dipartimento di Informatica, Torino 
Year  2007 
Address  C.so Svizzera, n.185  10149 Torino  Italy 
URL  http://arxiv.org/abs/0712.4222v2 
Abstract 
Weak affine light typing (WALT) assigns light affine linear formulae as types to a subset of lambdaterms in 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. In particular, the evaluation can proceed under any strategy of a rewriting relation, obtained as a mix of both callbyname/callbyvalue $\beta $reductions. WALT is polytime complete since it can represent any polytime Turing machine. WALT weakens, namely generalizes, the notion of stratification of deductions common to some Light Systems  we call as such those logical systems, derived from Linear logic, to characterize FP, the set of Polynomial functions  . A weaker stratification allows to define a compositional embedding of the Quasilinear fragment QlSRN of Safe recursion on notation (SRN) into WALT. QlSRN is SRN, which is a recursivetheoretical system characterizing FP, where only the composition scheme is restricted to linear safe variables. So, the expressivity of WALT is stronger, as compared to the known Light Systems. In particular, using the types, the embedding puts in evidence the stratification of normal and safe arguments hidden in QlSRN: the less an argument is impredicative, the deeper, in a formal, prooftheoretical sense, gets its representation in WALT. 
@techreport{Roversi:2007WALTFULL,
number = {103/07},
month = {December},
author = {Roversi, Luca},
url = {http://arxiv.org/abs/0712.4222v2},
title = {{W}eak {A}ffine {L}ight {T}yping: {I}ntensional expressivity,
{P}olytime soundness and completeness},
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 lambdaterms in
\textsf{System F}. \textsf{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. In particular, the evaluation can proceed under any strategy
of a rewriting relation, obtained as a mix of both
callbyname/callbyvalue $\beta$reductions. \textsf{WALT} is
polytime complete since it can represent any polytime Turing
machine. \textsf{WALT} \textit{weakens}, namely
\textit{generalizes}, the notion of stratification of deductions
common to some \textsf{Light Systems}  we call as such those
logical systems, derived from Linear logic, to characterize
\textsf{FP}, the set of Polynomial functions  . A weaker
stratification allows to define a compositional \textit{embedding}
of the \textit{Quasi}linear fragment \textsf{QlSRN} of Safe
recursion on notation (\textsf{SRN}) into \textsf{WALT}.
\textsf{QlSRN} is \textsf{SRN}, which is a recursivetheoretical
system characterizing \textsf{FP}, where only the composition
scheme is restricted to \textit{linear safe variables}. So, the
expressivity of \textsf{WALT} is stronger, as compared to the
known \textsf{Light Systems}. In particular, using the types, the
\textit{embedding} puts in evidence the stratification of normal
and safe arguments hidden in \textsf{QlSRN}: the less an argument
is impredicative, the deeper, in a formal, prooftheoretical
sense, gets its representation in \textsf{WALT}.},
institution = {Dipartimento di Informatica, Torino},
year = {2007},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)