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
Social Program
Location and Venue
Colocated Events
Authors' instructions
Print current pagePrint 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 Valid HTML 4.01! Valid CSS! Debian