Extending the loop language with higher-order procedural variables
Tristan Crolard, Emmanuel Polonowski, Pierre Valarcher · ACM Transactions on Computational Logic · 2009
We extend Meyer and Ritchie's Loop language with higher-order procedures and procedural variables and we show that the resulting programming language (called Loop ω ) is a natural imperative counterpart of Gödel System T. The argument is two-fold: (1) we define a translation of the Loop ω language into System T and we prove that this translation actually provides a lock-step simulation, (2) using a converse translation, we show that Loop ω is expressive enough to encode any term of System T. Moreover, we define the “iteration rank” of a Loop ω program, which corresponds to the classical notion of “recursion rank” in System T, and we show that both translations preserve ranks. Two applications of these results in the area of implicit complexity are described.