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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe