Révision 126 CSL16/conclusions.tex

conclusions.tex (revision 126)
21 21 
From the point of view of constructing theories for complexity classes, the choice of linear logic and witness function method satisfies two particular desiderata:
22 22 

  		





  23
  23
  
    
\begin{enumerate}


  		





  24
  
  
    
\item\label{item:crit-implicit-complexity} Complexity controlled by `implicit' means, not explicit bounds.


  		





  
  24
  
    
\item\label{item:crit-implicit-complexity} Complexity is controlled by `implicit' means, not explicit bounds.


  		





  25
  25
  
    
%, e.g.\ modalities or ramification, as in \cite{Leivant94:found-delin-ptime}. 


  		





  26
  26
  
    
\item\label{item:crit-ground-type} Extraction of programs relies on functions of only ground type.


  		





  27
  27
  
    
\end{enumerate}


  		





  ......




  34
  34
  
    

  		





  35
  35
  
    

  		





  36
  36
  
    

  		





  37
  
  
    
Most works on the relationships between linear logic and complexity fit in the approach of the proofs-as-programs correspondence and study variants of linear logic with weak exponential modalities \cite{GirardSS92:bounded-ll} \cite{Girard94:lll} \cite{Lafont04}. However, Terui considers a na\"ive set theory \cite{Terui04} that also characterises $\FP$ and is based on light linear logic.\footnote{He also presents a cut-elimination result but, interestingly, it is entirely complementary to that which we present here: he obtains full cut-elimination since he works in a system without full exponentials and with Comprehension as the only nonlogical rule. Since the latter admits a cut-reduction step, the former ensures that cut-elimination eventually terminates by a \emph{height-based} argument, contrary to our argument that analyses the \emph{degrees} of cut-formulae.} His approach relies on functionals at higher type, using light linear logic to type the extracted functionals. Another work using linear logic to characterize  complexity classes by using convergence proofs is \cite{Lasson11} but it is tailored for second-order logic.


  		





  
  37
  
    
Most works on the relationships between linear logic and complexity fit in the approach of the proofs-as-programs correspondence and study variants of linear logic with weak exponential modalities \cite{GirardSS92:bounded-ll} \cite{Girard94:lll} \cite{Lafont04}. However, Terui considers a na\"ive set theory \cite{Terui04} that also characterises $\FP$ and is based on \emph{light linear logic}.\footnote{He also presents a cut-elimination result but, interestingly, it is entirely complementary to that which we present here: he obtains full cut-elimination since he works in a system without full exponentials and with Comprehension as the only nonlogical rule. Since the latter admits a cut-reduction step, the former ensures that cut-elimination eventually terminates by a \emph{height-based} argument, contrary to our argument that analyses the \emph{degrees} of cut-formulae.} His approach relies on functionals at higher type, using the propositional fragment of the logic to type the extracted functionals. Another work using linear logic to characterize  complexity classes by using convergence proofs is \cite{Lasson11} but it is tailored for second-order logic.


  		





  38
  38
  
    
 The status of first-order theories is more developed for other substructural logics, for instance \emph{relevant logic} \cite{FriedmanM92}, although we do not know of any works connecting such logics to computational complexity.


  		





  39
  39
  
    

  		





  40
  40
  
    
%Most works on the relationships between linear logic and complexity concern the construction of \emph{type systems}, e.g.\ bounded linear logic \cite{GirardSS92:bounded-ll}, light linear logic and elementary linear logic \cite{Girard94:lll}, soft linear logic \cite{Lafont04}. However, Terui considers a na\"ive set theory \cite{Terui04} that is also sound and complete for polynomial time and is based on light linear logic. His approach relies on functionals at higher type, using light linear logic to type the extracted functionals.\footnote{He also presents a cut-elimination result but, interestingly, it is entirely complementary to that which we present here: he obtains full cut-elimination since he works in a system without full exponentials and with Comprehension as the only nonlogical axiom. Since the latter admits a cut-reduction step, the former ensures that cut-elimination eventually terminates by a \emph{height-based} argument, contrary to our argument that analyses the \emph{degrees} of cut-formulae.} The status of first-order theories is more developed for other substructural logics, for instance \emph{relevant logic} [cite?], although we do not know of any works connecting such logics to computational complexity.


  		





  41
  41
  
    

  		





  42
  
  
    
Concerning the relationship between linear logic and safe recursion, note that an embedding of a variant of safe recursion into light linear logic has been carried studied in \cite{Murawski04}, but this is in the setting of functional computation and is quite different from the present approach. Observe however that a difficulty in this setting  was the non-linear treatment of safe arguments which here we manage by including in our theory a duplication axiom for $W$. 


  		





  
  42
  
    
Concerning the relationship between linear logic and safe recursion, we note that an embedding of a variant of safe recursion into light linear logic has been carried studied in \cite{Murawski04}, but this is in the setting of functional computation and is quite different from the present approach. Observe, however, that a difficulty in this setting  was the nonlinear treatment of safe arguments which here we manage by including in our theory an explicit contraction axiom for $W$. 


  		





  43
  43
  
    

  		





  44
  44
  
    
We have already mentioned the work of Bellantoni and Hofmann \cite{BelHof:02}, which was somewhat the inspiration behind this work. Our logical setting is very similar to theirs, under a certain identification of symbols, but there is a curious disconnect in our use of the additive disjunction for the $\surj$ axiom. They rely on just one variant of disjunction. As we said, they rely on a double-negation translation and thus functionals at higher-type.


  		





  45
  45
  
    

  		





  ......




  68
  68
  
    
%\todo{finish!}


  		





  69
  69
  
    

  		





  70
  70
  
    
%


  		





  71
  
  
    
In further work we would like to apply the free-cut elimination theorem to theories based on other models of computation, namely the formula model employed in bounded arithmetic \cite{Buss86book}. We believe that the WFM could be used at a much finer level in this setting,\footnote{One reason for this is that atomic formulae are decidable, and so we can have more freedom with the modalities in induction steps.} and extensions of the theory for other complexity classes, for instance the polynomial hierarchy, might be easier to obtain.


  		





  
  71
  
    
In further work we would like to apply the free-cut elimination theorem to theories based on other models of computation, namely the formula model employed in bounded arithmetic \cite{Buss86book}. We believe that the witness function method could be used at a much finer level in this setting,\footnote{One reason for this is that atomic formulae are decidable, and so we can have more freedom with the modalities in induction steps.} and extensions of the theory for other complexity classes, e.g.\ the polynomial hierarchy, might be easier to obtain.


  		





  72
  72
  
    
%


  		





  73
  73
  
    
%Say something about minimisation and the polynomial hierarchy. Could be achieved by controlling contraction/additives, since this requires a notion of tests.


  		





  74
  74
  
    
%


  		












Formats disponibles :
  Unified diff