7
$\begingroup$

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?

Improve this question
$\endgroup$
1
  • $\begingroup$ 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). $\endgroup$
    – wvxvw
    Commented May 3, 2016 at 21:06

2 Answers 2

Reset to default
7
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ Could you please give some directions towards types that capture complexity classes (papers or maybe books)? $\endgroup$
    – Anton Trunov
    Commented May 3, 2016 at 20:09
  • 3
    $\begingroup$ @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. $\endgroup$
    – Martin Berger
    Commented May 3, 2016 at 20:18
5
$\begingroup$

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!

Improve this answer
$\endgroup$
1
  • $\begingroup$ 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. $\endgroup$
    – sfultong
    Commented May 25, 2016 at 18:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.