Miguel Mitrofanov wrote:
That's an interesting task: Design a non-touring complete, restricted language in which every expression is decidable, without making the language unusable for usual programming problems.
Well, I did something like that a few years ago - it was a sort of assembler language, allowing the programmer to, say, sort an array, but not to calculate Akkerman function.
P. Wadler, in his famous paper "Theorems for free!", writes on page 2: "Indeed, every recursive function that can be proved total in second order Peano arithmetic can be written as a term in the Girard/Reynolds calculus [...]. This includes, for instancs, Ackerman's function [...], but excludes interpreters for most languages (including the Girard/Reynolds calculus itself)." BTW, another name for the Girard/Reynolds calculus is "(pure) polymorphic lambda calculus"; and yes, it is strongly normalizing. (Wadler cites some papers to support the above claim.) It seems there is quite a lot of interesting stuff that can be done in a language where every expression is guaranteed to terminate. Cheers Ben