eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2016-08-29
40:1
40:18
10.4230/LIPIcs.CSL.2016.40
article
Free-Cut Elimination in Linear Logic and an Application to a Feasible Arithmetic
Baillot, Patrick
Das, Anupam
We prove a general form of 'free-cut elimination' for first-order theories in linear logic, yielding normal forms of proofs where cuts are anchored to nonlogical steps. To demonstrate the usefulness of this result, we consider a version of arithmetic in linear logic, based on a previous axiomatisation by Bellantoni and Hofmann. We prove a witnessing theorem for a fragment of this arithmetic via the `witness function method', showing that the provably convergent functions are precisely the polynomial-time functions. The programs extracted are implemented in the framework of 'safe' recursive functions, due to Bellantoni and Cook, where the ! modality of linear logic corresponds to normal inputs of a safe recursive program.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol062-csl2016/LIPIcs.CSL.2016.40/LIPIcs.CSL.2016.40.pdf
proof theory
linear logic
bounded arithmetic
polynomial time computation
implicit computational complexity