Linear two-sorted constructive arithmetic

Helmut Schwichtenberg - Universit√§t M√ľnchen
Date and time
Tuesday, March 15, 2016 at 4:00 PM - rinfresco 15.45, inizio seminario 16.00
Ca' Vignal - Piramide, Floor 0, Hall Verde
Programme Director
Peter Michael Schuster
External reference
Publication date
February 1, 2016
Computer Science  


We consider a term system in the style of Gödel's system T together
with a computation model that allows to faithfully represent
polynomial-time algorithms.  To this end we follow a tradition initiated
by Simmons (1988) and developed by Bellantoni and Cook (1992), where two
sorts of variables are admitted, here called output and input variables.
The idea is that input variables are the general ones which may be
recursed on and used many times, whereas output variables cannot be
recursed on and can be used only once.  These ideas have been extended
to a higher type setting and hence -- via the Curry-Howard
correspondence -- to a linear two-sorted arithmetical system in the
style of Heyting arithmetic in all finite types.  Here we further extend
this setup with the aim to also include certain nonlinear algorithms
(like treesort), given by constants defined by equations involving
multiple recursive calls.

© 2002 - 2021  Verona University
Via dell'Artigliere 8, 37129 Verona  |  P. I.V.A. 01541040232  |  C. FISCALE 93009870234