I'm curious of the ways we can construct provably complex languages.

In particular, most constructions (i.e., the one used for proving the Time hierarchy theorem) seem to rely on encodings of Turing Machines and some diagonalization argument.

Do we know of ways to construct complex languages based on other techniques?

For example, I'm thinking in the direction of somehow using randomness to construct a difficult to decide language similar to how we would do to achieve high Kolmogorov complexity.

  • 1
    $\begingroup$ A good place to start is System F, also known as second-order propositional constructive logic. F lacks recursion so is total, and cannot be Turing complete. Unless you know what you are looking for, you'd probably struggle to find a natural total function that is provably not expressible in System F. Barendregt's $\lambda$-cube gives a systematic way of constructure a few more such languages. $\endgroup$ Mar 17 at 16:56
  • 1
    $\begingroup$ This seems essentially the same as cstheory.stackexchange.com/q/6575/129. Is there something @mti has in mind that distinguishes the two? $\endgroup$ Mar 18 at 1:40
  • $\begingroup$ @JoshuaGrochow Thanks for the pointer. Looks definitely related and interesting. Will look into that in more detail later. This question does have a different scope though. Beyond getting an overview of methods for constructing complex languages, my intent also was to initiate a discussion around the idea of constructing complex languages more "manually". E.g., we know that a random string has high Kolmogorov complexity. Is there a similar property in the realm of computation that ensures high computational complexity? $\endgroup$
    – mti
    Mar 18 at 14:46
  • 1
    $\begingroup$ Just as you prove that random strings have high Kolmogorov complexity w/ a counting argument, one can also prove by a counting argument (going back at least to Shannon) that random Boolean functions on n variables cannot be computed by circuits smaller than $\Theta(2^n / n)$. Is that like what you had in mind? $\endgroup$ Mar 18 at 19:08
  • $\begingroup$ Yes, something like that. Would you have a reference for a formalization of that statement? $\endgroup$
    – mti
    Mar 18 at 19:54


Your Answer

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

Browse other questions tagged or ask your own question.