On the expressive power of finitely typed and universally polymorphic recursive procedures (Q1185006)

The paper is devoted to the expressive power of functional programs. The language of finitely typed functional programs of level less than or equal to \(k\) is devoted by \(FL_ k\) (the level of a program is the highest order of a function definition used in the program). The first result of the paper is that the hierarchy \(FL_ 0\subset FL_ 1\subset\dots\) does not collapse, namely, that \(FL_ k\) is strictly less expressive than \(FL_{k+2}\), for an arbitrary \(k\). Using the result of Goerdt that the spectral complexity of \(FL_ k\) is exactly \(\text{DTIME}(\exp_ k({\mathcal O}(\log n)))\), the authors strengthen the result by showing that the above hierarchy is strict. The language \(FL=\bigcup_{k=0}^ \infty FL_ k\) of finitely typed functional programs corresponds exactly to the elementary spectral complexity, in other words, the halting problem for the language on finite models is exactly elementary (and in particular, decidable). The programming language \(ML\) is, essentially, \(FL\), augmented with the polymorphic let-in constructor. It is shown that \(ML\), however, computes the same class of functions as \(FL\), and therefore, the presence of the polymorphic let-in constructor in \(ML\) is not essential. Second however is that \(ML\) extended with a polymorphic fixpoint constructor has the halting problem for finite models undecidable. As a matter of fact, the paper shows that this last extension \(EML\) of the language \(ML\) is semi-universal, in the sense of the theory of program schemes. Therefore, \(EML\) is strictly more expressive than \(ML\).