Computer Science Logic and 8th Kurt Gödel Colloquium Lars Kristiansen, Paul J. Voda: The Surprising Power of Restricted Programs and G"odel's Functionals

Welcome and News Host Institutions Calls and Deadlines Program Social Program Registration Location and Venue Accommodation Committees Contact Colocated Events Authors' instructions

Print this page We introduce a typed imperative programming language operating on natural numbers. The language has only one primitive instruction, increment modulo a base, and only two control structures, the while-loop and the composition. This extremely restricted, but still very natural language, yields an amazing computational power. We prove that the levels of a hierarchy induced by the language, exactly match the levels in the Ritchie hierarchy. (The hierarchy starts with Grzegorczyk's ${\cal E}^2$ (LINSPACE), and the union of the classes in the hierarchy equals the class of Kalmar elementary functions.) Further, we introduce a formal system $T_\ell$ for defining and computing G\"odel functionals. The system $T_\ell$ is a restriction of G\"odel T. We have removed the successor function, and the only initial function available in $T_\ell$ is the constant function 1 (instead of T's 0). It turns out that exactly the functions in the Ritchie hierarchy can be defined in $T_\ell$. We investigate the relationship between a hierarchy induced by $T_\ell$ and the Ritchie hierarchy. © 2002-2003 Kurt Gödel Society, Norbert Preining. 2003-06-04