<p>Suppose we are given a program specification, <span class="math-container">$S$</span>, and we want to reason about programs <span class="math-container">$P$</span> that satisfy <span class="math-container">$S$</span>. 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:</p>

<blockquote>
  <p>In general, we cannot claim that for arbitrary <span class="math-container">$S$</span>, a program <span class="math-container">$P$</span> exists that satisfies <span class="math-container">$S$</span> and is both 'small' and 'fast'.</p>
</blockquote>

<p>I'm looking for three things:</p>

<ol>
<li>The proper way to state the above formally.</li>
<li>An idea of how to prove such a thing.</li>
<li>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.</li>
</ol>

<p>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.</p>

<p>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. </p>

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

<p>This is not terribly difficult to prove. Suppose the claim were false and let <span class="math-container">$f$</span> be such that  every theorem of length <span class="math-container">$n$</span> had a proof of length no greater than <span class="math-container">$f(n)$</span>. Let <span class="math-container">$T$</span> be a statement from any undecidable theory <span class="math-container">$\mathcal{T}$</span> with <span class="math-container">$n = |T|$</span>. Now enumerate all proofs of length at most <span class="math-container">$f(n)$</span>. Then <span class="math-container">$T$</span>  is a theorem if and only if at least one those enumerated proofs is a proof of <span class="math-container">$T$</span>. As <span class="math-container">$T$</span> 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 <span class="math-container">$\mathcal{T}$</span>. </p>

<p>The following references are relevant.</p>

<p>Joel Spencer. Short Theorems with Long Proofs. The American Mathematical Monthly, 1983.</p>

<p><a href="http://www.jstor.org/stable/2975571" rel="nofollow noreferrer">http://www.jstor.org/stable/2975571</a></p>

<p>F. H. Norwood. Long Proofs. The American Mathematical Monthly, 1982.</p>

<p><a href="http://www.jstor.org/stable/2320927" rel="nofollow noreferrer">http://www.jstor.org/stable/2320927</a></p>

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

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

<blockquote>
  <p>There does not exist a computable function <span class="math-container">$f$</span>, such that for all
  program specifications <span class="math-container">$S$</span>, if <span class="math-container">$S$</span> is satisfied by some program, then
  the length of the shortest program <span class="math-container">$P$</span> that satisfies <span class="math-container">$S$</span> is no
  greater than <span class="math-container">$f(|S|)$</span>, where <span class="math-container">$|S|$</span> is the length of <span class="math-container">$S$</span>.</p>
</blockquote>

<p>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.</p>

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

<p>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 <span class="math-container">$n$</span>, the program outputs the <span class="math-container">$n$</span>th Fibonacci number'', and then consider the size of the smallest program in a Turing-complete model of computation that behaves this way. </p>

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

<p><strong>Specification Size.</strong> Since <span class="math-container">$S$</span> is a computable binary predicate, there exists a TM, say <span class="math-container">$M_S$</span> such that when provided <span class="math-container">$(u,v)$</span> as input on the tape, indicates whether <span class="math-container">$S(u,v)$</span> 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?) <span class="math-container">$M_S$</span> that computes <span class="math-container">$S(u,v)$</span>. We take the size of a Turing machine to be, say, the length of the description of the state transition relation. </p>

<p><strong>Constructing a program that satisfies a spec with only constant overhead.</strong> With the specification phrased this way, one can construct a TM, <span class="math-container">$M$</span> that takes the spec <span class="math-container">$S$</span> as input and computes a function <span class="math-container">$g$</span> such that <span class="math-container">$g(u) = v$</span> if and only if <span class="math-container">$S(u,v)$</span> holds. </p>

<p>Outline of the operation of <span class="math-container">$M$</span>, that takes <span class="math-container">$u$</span> as input on the tape:</p>

<ol>
<li>Let <span class="math-container">$\mathcal{M} = \{M_1, M_2, \ldots \}$</span> be an enumeration of all possible Turing machines.</li>
<li>Using a dovetailed computation, run every <span class="math-container">$M_i$</span> for <span class="math-container">$j$</span> steps on <span class="math-container">$u$</span>. If <span class="math-container">$M_i$</span> halts with final tape configuration <span class="math-container">$v$</span>, simulate <span class="math-container">$M_S$</span> on input <span class="math-container">$(u,v)$</span>.</li>
<li>If <span class="math-container">$M_S(u,v)$</span> halts in an accept state, then output <span class="math-container">$v$</span> and halt.</li>
</ol>

<p>The above will be a fixed size machine that satisfies an arbitrary computable specification by outputting <span class="math-container">$v$</span> for input <span class="math-container">$u$</span> if and only if <span class="math-container">$S(u,v)$</span>.</p>

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

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

<p>This is where I am stuck.</p>

<p>I've found one seemingly relevant paper, and I am slowly digesting it:</p>

<p>Manuel Bloom. On the Size of Machines. Information and Control, 1967.</p>

<p><a href="https://www.sciencedirect.com/science/article/pii/S0019995867905463" rel="nofollow noreferrer">https://www.sciencedirect.com/science/article/pii/S0019995867905463</a></p>

<p>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.</p>

<p>Any pointers would be greatly appreciated. </p>

CC BY-SA 4.0
2020-05-26T14:15:04.207Z
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.
Andrej Bauer
CC BY-SA 4.0
2020-05-26T15:46:20.180Z
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?
user10108
<computability><turing-machines><kolmogorov-complexity><universal-turing-machines>
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?
user10108
# 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?

(Asked by: username_0 on 2020-05-26)

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.

**Tags:** computability, turing-machines, kolmogorov-complexity, universal-turing-machines

> **Comments:**
> **username_1**: 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.  
> **username_0**: 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?  

---

## 0 answers

