Retour à la page du séminaire

27/01/99: Helmut Schwichtenberg (Munich) --- Feasible programs from proofs.

abstract

We restrict induction and recursion on notations in all finite types so as to characterize the polynomial time computable functions. The restrictions are obtained by enriching the type structure with a formation of types $\square\sigma \multimap \tau$ and formulas $\square A
\multimap B$ and $\forall \overline{x}^\sigma A$, and by adding linear concepts to the lambda-calculus (for object terms and proof terms). For the arithmetical system we define modified realizability and show that the programs extracted from proofs of $\Pi^0_2$-theorems characterize the polynomial time computable functions.