# Given a program specification, S, what can be said about the size and efficiency of programs that exactly satsify S, with respect to the size of S?

Suppose we are given a program specification, $$S$$, and we want to reason about programs $$P$$ that satisfy $$S$$. One might like to think that if the specification is 'simple', the the program should be 'simple'. I'm curious about the following informal statement, or a similar statement in the case that I am slightly mis-stating it:

In general, we cannot claim that for arbitrary $$S$$, a program $$P$$ exists that satisfies $$S$$ and is both 'small' and 'fast'.

I'm looking for three things:

1. The proper way to state the above formally.
2. An idea of how to prove such a thing.
3. Citations to papers or texts that address this problem. The more accessible to non-computability/complexity theory experts, e.g. motivated undergrad CS student, the better.

My motivation for this problem comes from a related statement about the sizes of proofs. I'm posting my thought process here so you know where I'm coming from on this and what I have tried.

We'd like to think that if a statement of mathematics is concise enough to easily state, then it ought to have a short, elegant proof. However, it is almost a folk theorem, to state it informally, that there are statements of mathematics that are provably true but whose shortest proof is exceptionally long compared to the length of the original statement. Our desire for short proofs is a double edged sword; we are always on the lookout for shorter, cleaner, better proofs, but we are left feeling somehow dissatisfied with long computer generated proofs, like that of the four color theorem, when it is conceivable that this is indeed the shortest possible proof.

To make the 'folk theorem' about proof lengths just slightly more formal, we can say that there does not exist a computable function $$f$$, such that for all mathematical statements $$T$$, if $$T$$ is provable, the length of the shortest proof $$P$$ of $$T$$ is no greater than $$f(|T|)$$, where $$|T|$$ is the length of $$T$$. To make it concrete, this tells us that if $$a$$ is, for instance, the Ackermann function, then there is some theorem $$T$$ whose shortest proof has length at least $$a(|T|)$$.

This is not terribly difficult to prove. Suppose the claim were false and let $$f$$ be such that every theorem of length $$n$$ had a proof of length no greater than $$f(n)$$. Let $$T$$ be a statement from any undecidable theory $$\mathcal{T}$$ with $$n = |T|$$. Now enumerate all proofs of length at most $$f(n)$$. Then $$T$$ is a theorem if and only if at least one those enumerated proofs is a proof of $$T$$. As $$T$$ was assumed to come from a theory sufficiently 'interesting' so as to be undecidable, we have a contradiction, as the process we just described is a decision procedure for $$\mathcal{T}$$.

The following references are relevant.

Joel Spencer. Short Theorems with Long Proofs. The American Mathematical Monthly, 1983.

http://www.jstor.org/stable/2975571

F. H. Norwood. Long Proofs. The American Mathematical Monthly, 1982.

http://www.jstor.org/stable/2320927

One can map this idea to Turing machines: there does not exist a computable function $$f$$, such that for all Turing machines $$M$$, if $$M$$ halts, then it halts within $$f(n)$$ steps where $$n$$ is the size of $$M$$ under some Turing machine encoding scheme. One can make a similar argument as above, essentially giving a procedure to decide the halting problem.

I had hoped to make a similar claim about the size of a program that satisfies a specification:

There does not exist a computable function $$f$$, such that for all program specifications $$S$$, if $$S$$ is satisfied by some program, then the length of the shortest program $$P$$ that satisfies $$S$$ is no greater than $$f(|S|)$$, where $$|S|$$ is the length of $$S$$.

Turns out this is not true. Why not? Well, maybe some version of it is true, but not the way that I had formulated it.

One thing to notice is that this immediately calls to mind the notion of Kolmogorov complexity. Roughly speaking, the Kolmogorov complexity of a string, $$w$$ is the length of the smallest program that outputs $$w$$ when taking no input. As it turns out, the Kolmogorov complexity of a string is often smaller than $$|w|$$, and never larger than $$|w|$$ by more than a programming-language-dependent constant. So this isn't really what we want.

Why not? Specifying a program by providing a single string that must be the output of the program is not a very powerful or flexible way to specify programs. In some sense, the specification language is very weak compared to the implementation programming language (which is presumably Turing complete). At the other extreme, a Turing-complete specification language and an implementation language that can do nothing except print a single string constant is useless. What we would like to be able to do is state something like on input $$n$$, the program outputs the $$n$$th Fibonacci number'', and then consider the size of the smallest program in a Turing-complete model of computation that behaves this way.

Specification. We first need to define what we mean by a specification. Here is an attempt. Let $$S(u,v)$$ be a computable binary predicate on binary strings. We interpret the first argument $$u$$ as the initial configuration of a Turing machine tape and $$v$$ as the configuration of the Turing machine tape when (and if) it halts. The specification indicates that for any pair of binary strings $$(u,v)$$ the desired TM when initialized with $$u$$ on the tape halts with $$v$$ on the tape if and only if $$S(u,v)$$. \

Specification Size. Since $$S$$ is a computable binary predicate, there exists a TM, say $$M_S$$ such that when provided $$(u,v)$$ as input on the tape, indicates whether $$S(u,v)$$ holds (say by printing 0 or 1 as the case may be). We then take the size of the specification to be the size of the (smallest?) $$M_S$$ that computes $$S(u,v)$$. We take the size of a Turing machine to be, say, the length of the description of the state transition relation.

Constructing a program that satisfies a spec with only constant overhead. With the specification phrased this way, one can construct a TM, $$M$$ that takes the spec $$S$$ as input and computes a function $$g$$ such that $$g(u) = v$$ if and only if $$S(u,v)$$ holds.

Outline of the operation of $$M$$, that takes $$u$$ as input on the tape:

1. Let $$\mathcal{M} = \{M_1, M_2, \ldots \}$$ be an enumeration of all possible Turing machines.
2. Using a dovetailed computation, run every $$M_i$$ for $$j$$ steps on $$u$$. If $$M_i$$ halts with final tape configuration $$v$$, simulate $$M_S$$ on input $$(u,v)$$.
3. If $$M_S(u,v)$$ halts in an accept state, then output $$v$$ and halt.

The above will be a fixed size machine that satisfies an arbitrary computable specification by outputting $$v$$ for input $$u$$ if and only if $$S(u,v)$$.

So now where are we? The above discussion seems to provide a counter example, and it does, but at a high price. The machine $$M$$ as described will take A LOT of steps. So now we are in a position to restate our earlier claim as a new conjecture:

Informally, there are specifications where the program that satisfies the specification cannot be both small and fast.

This is where I am stuck.

I've found one seemingly relevant paper, and I am slowly digesting it:

Manuel Bloom. On the Size of Machines. Information and Control, 1967.

https://www.sciencedirect.com/science/article/pii/S0019995867905463

I've also tried to see how Rice's Theorem applies here, but I don't quite see that either. It seems like this problem combines both semantic and syntactic properties.

Any pointers would be greatly appreciated.

• A program specification may ask for a program that prints a proof of a particular statement. So the results about theorems without short proofs should carry over. May 26 '20 at 14:15
• That seesm to get at half of the problem. A program that satisfies such a specification could be an automated theorem prover, which would have constant size with respect to the size of the spec. Then the running time of the program is at least as long as the output (the length of the resulting proof). So again we have a situation where the program is 'small' but the running time is large. How can we extend this to say that there must be some specification where the resulting program and the running time are arbitrarily large with respect to the size of the spec? May 26 '20 at 15:46