What types of string properties are verifiable in polynomial time?

Question

When given the string and the property in question as a potential certificate. Is there any classification theorem that says something along the lines of: all properties (of strings) that have this property (as a sub property) are verifiable in polynomial time?

Are there any collections of types of patterns in strings that are verifiable in poly time?

A trivial property is that a collection of strings with these properties belong to a language in NP (belonging to NP being the sub property).

I'm looking for something more concrete.

I'm looking for the common thread between string properties like these that makes these properties verifiable in poly time for any string.

i.e. is there a way to pick properties of strings out of a hat in such a way that the properties you pick are guaranteed to be verifiable in poly time in any string.

Maybe there is a way to do this with implicit complexity--where the only properties you can build (in some restricted language) are the ones that are verifiable in poly time?

Answer 1

Verifying a property of strings over an alphabet $\Sigma$ is precisely the same problem as checking whether a string is part of a language, called the Entscheidungsproblem or decision problem.

Language : $\Sigma^* \mapsto \{0,1\}$

What you are interested in are 'properties of strings' or in other words 'classes of languages'.

The class you are probably looking for is 'P', which contains all languages for which the decision problem can be solved in polynomial time on a deterministic Turing machine. Interestingly this class is the same as the class of languages for which the decision problem can be solved by polynomial circuits.

All C programs which contain constantly bounded loops belong to P for example (they can easily be turned into a polynomial circuit). From there you can extend the language to include other loops that terminate in polynomial time. You have to be careful with nested loops. There are special Hoare-type logics for this purpose.