# What are the most expressive, terminating languages?

I'm less interested in languages where you can write almost anything, but then are required to write an accompanying proof that what you wrote terminates.

I'm more interested in the design space of languages inherently confined to certain complexity classes by construction.

Is there any sort of theory hierarchy for sub-turing-complete languages?

• There are some shader languages (languages used to program graphical processor), where you cannot write a non-terminating program. Not sure how interesting they are in theoretical terms, but if you needed a practical example, here you go (look for GLSL for example). – wvxvw May 3 '16 at 21:06

There are plenty of classes of programming languages where all programs terminate. The most common form of enforcing termination is by way of types. The most well-developed theory of typing systems for terminating computation might be that of Barendregt's Lambda cube, which decomposes typing into three orthogonal axes:

Starting from a terminating languages such as the simply typed $\lambda$-calculus, one can add any combination of those three axes and retain termination.

This has close connections with logic, via the Curry-Howard correspondence.

There are many extensions and refinements, including types that capture complexity classes.

• Could you please give some directions towards types that capture complexity classes (papers or maybe books)? – Anton Trunov May 3 '16 at 20:09
• @AntonTrunov The general field is "implicit computational complexity". It's a young field, so I don't think there are any books yet. One of the pioneering works are J.-Y. Girard, Light Linear Logic, and his Bounded Linear Logic, the latter co-authored by A. Scedrov and P. Scott. – Martin Berger May 3 '16 at 20:18

Following Bellantoni & Cook's foundational work in A New Recursion-Theoretic Characterization of Polytime Functions, there's been a lot of work on simple characterizations of complexity classes by means of total languages, with strong connections to linear logic as Martin Berger notes in the comments.

Building on this work, other complexity classes have been characterized: Leivant and Marion have given characterizations of PSPACE and ELEM (that last one is particularly nice).

There's also been work on LOGSPACE, again with Leivant and Ramyaa.

It's a pretty exciting field, with a yearly conference!

• This is actually more of the answer I was looking for, but I already accepted the other one. I'm pretty excited about the field as well. – sfultong May 25 '16 at 18:55