Linear two-sorted constructive arithmetic

Speaker:  Helmut Schwichtenberg - Universität München
  Tuesday, March 15, 2016 at 4:00 PM rinfresco 15.45, inizio seminario 16.00
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.

Ca' Vignal 3 - Piramide, Floor 0, Hall Verde

Contact person
Peter Michael Schuster

Publication date
February 1, 2016