Révision 117
| CSL16/introduction.tex (revision 117) | ||
|---|---|---|
| 22 | 22 |
|
| 23 | 23 |
We show that Buss' witness function method can be employed to extract functions directly for classical systems similar to $\mathcal{A}_2^1$ based in linear logic, by taking advantage of free-cut elimination. The De Morgan normal form available in classical (linear) logic means that the functions we extract remain at ground type, based on the usual safe recursive programs of \cite{BelHof:02}. A similar proof method was used by Cantini in \cite{Cantini02}, who uses combinatory terms as the model of computation as opposed to the equational specifications in this work.\footnote{This turns out to be important due to the handling of right-contraction steps in the witnessing argument.}
|
| 24 | 24 |
|
| 25 |
Our result holds for an apparently weaker theory than $\mathcal{A}_2^1$, with induction restricted to positive existential formulas in a way similar to Leivant's $\mathit{RT}_0$ system in \cite{Leivant94:intrinsic-theories}, but the precise relationship between the two logical settings is unclear.
|
|
| 25 |
Our result holds for an apparently weaker theory than $\mathcal{A}_2^1$, with induction restricted to positive existential formulas in a way similar to Leivant's $\mathit{RT}_0$ system in \cite{Leivant94:intrinsic-theories} (see also \cite{Marion01}), but the precise relationship between the two logical settings is unclear.
|
|
| 26 |
% |
|
| 27 |
% Our result holds for an apparently weaker theory than $\mathcal{A}_2^1$, with induction restricted to positive existential formulas in a way similar to Leivant's $\mathit{RT}_0$ system in \cite{Leivant94:intrinsic-theories}, but the precise relationship between the two logical settings is unclear.
|
|
| 26 | 28 |
% We illustrate in the same time the relationship between $\mathcal{A}_2^1$ and linear logic, which was hinted but not investigated in the original paper \cite{BelHof:02}.
|
| 27 | 29 |
We conclude in Sect.~\ref{sect:conclusions} with a survey of related work and some avenues for further applications of the free-cut elimination result.
|
| 28 | 30 |
|
| CSL16/biblio.bib (revision 117) | ||
|---|---|---|
| 279 | 279 |
|
| 280 | 280 |
|
| 281 | 281 |
|
| 282 |
@inproceedings{Marion01,
|
|
| 283 |
author = {Jean{-}Yves Marion},
|
|
| 284 |
title = {Actual Arithmetic and Feasibility},
|
|
| 285 |
booktitle = {Proceedings of Computer Science Logic (CSL 2001)} ,
|
|
| 286 |
pages = {115--129},
|
|
| 287 |
series = {Lecture Notes in Computer Science},
|
|
| 288 |
volume = {2142},
|
|
| 289 |
publisher = {Springer},
|
|
| 290 |
year = {2001}
|
|
| 291 |
} |
|
| 292 |
|
|
| 293 |
|
|
| 294 |
|
|
| 295 |
|
|
| 282 | 296 |
@preprint{BaiDas,
|
| 283 | 297 |
author = {Patrick Baillot and Anupam Das},
|
| 284 | 298 |
title = {Free-cut elimination in linear logic and an application to a feasible arithmetic},
|
Formats disponibles : Unified diff