<p><a href="https://en.wikipedia.org/wiki/Blum%27s_speedup_theorem">Blum’s speedup theorem</a> is usually stated in the language of partially recursive functions, but up to trivial differences in notation, it works just the same in the language of $\lambda$-calculus.</p>

<p>It says that given any reasonable complexity measure $M$ (for example, the optimal number of reductions as in the question) and a recursive function $f(x,y)$ (for example, $2^y$), we can find a recursive predicate $P(x)$ such that:</p>

<blockquote>
  <p>For every algorithm (i.e., $\lambda$-term in normal form here) $g$ computing $P$, there is another algorithm $h$ for $P$ that has $f$-speedup over $g$:
  $$f(x,M(h,x))\le M(g,x)\text{ for all large enough inputs }x,$$</p>
</blockquote>

<p>where $M(g,x)$ denotes the complexity of the computation of $g$ on input $x$ according to measure $M$.</p>

<p>Consequently:</p>

<ul>
<li><p>$P$ has no asymptotically optimal algorithm in the given measure</p></li>
<li><p>in particular, the shortest algorithm for $P$ is not asymptotically optimal</p></li>
<li><p>for any algorithm for $P$, there is an asymptotically faster algorithm whose normal form is longer (because up to renaming of variables, there are only finitely many normal terms of a given length)</p></li>
</ul>

CC BY-SA 3.0
2015-08-25T13:33:35.590Z
2015-08-25T13:33:35.590Z
Emil Jeřábek
<p>Let the $size$ of $\lambda$-terms be defined as follows:</p>

<ul>
<li>$size(x) = 1$,</li>
<li>$size(λx.t) = size(t) + 1$,</li>
<li>$size(t s) = size(t) + size(s) + 1$.</li>
</ul>

<p>Let the complexity of a $\lambda$-term $t$ be defined as 
the number of parallel beta reductions from $t x$ to its normal form
(using an optimal evaluator in Levy's sense).</p>

<p>I am looking for an example of two <em>normal</em> $\lambda$-terms for the same function where 
the larger term has lower complexity.</p>

<p>...</p>

<h2>Edit for clarity</h2>

<p>since it seems that it is not obvious what I'm asking, I'll try to give a solid example. There is often a belief that the "naive"/"simplest" definition of a function is slow and not optimal. Better performance increase the complexity of the term, since you need added data-structures, formulas, etc. A great example is <code>fibonacci</code>, which can be "naively" defined as:</p>

<pre><code>-- The fixed fibonacci definition
fib_rec fib n =
    if (is_zero x) 
        then 1 
        else fib (n - 1) + f (n - 2)

-- Using church numbers instead of the λ-combinator to get a normal form
fib n = n fib_rec 0 n 
</code></pre>

<p>This is often regarded as the "simplest" definition of fib, and is very slow (exponential). If we expand the dependencies of <code>fib</code> (the <a href="https://en.wikipedia.org/wiki/Church_encoding" rel="noreferrer">usual definitions</a> for church-number addition, pred, is_zero), and normalize it, we get this term:</p>

<pre><code>fib = (λa.(a(λbc.(c(λdef.f)(λde.d)(λde.(de))
      (λde.(b(λfg.(c(λhi.(i(hf)))(λh.g)(λh.h)))
      d(b(λfg.(c(λhi.(i(h(λjk.(k(jf))))))(λhi.g)
      (λh.h)(λh.h)))de)))))(λbc.c)a))
</code></pre>

<p>Improvements such as memoization tables would make this term bigger. Yet, <strong>there exists</strong> a different term that is much smaller...</p>

<pre><code>fib = (λa.(a(λb.(b(λcde.(e(λfg.(cf(dfg)))c))))
      (λb.(b(λcd.(cd))(λcd.d)))(λbc.b)))
</code></pre>

<p>and, curiously, is also asymptotically superior to the naive one, running in <code>O(N)</code>. Of all definitions I'm aware, <strong>this is both the fastest and the simplest</strong>. The same effect happens with sort. "Naive" definitions such as bubble sort and insertion sort often get expanded to huge terms (20+ lines long), but <strong>there exists</strong> a small definition:</p>

<pre><code>-- sorts a church list (represented as the fold) of church numbers
sort = λabc.a(λdefg.f(d(λhij.j(λkl.k(λmn.mhi)l)(h(λkl.l)i))
       (λhi.i(λjk.bd(jhk))(bd(h(λjk.j(λlm.m)k)c))))e)(λde.e)
       (λde.d(λfg.g)e)c
</code></pre>

<p>Which also happens to be faster, asymptotically, than every other definition I know. This observation leads me to believe that, as opposed to common belief, the simplest term, with smallest Kolmogorov complexity, is usually the faster. My question is basically wether there is any evidence of the opposite, although I'd have a hard time in formalizing it. </p>

CC BY-SA 3.0
2015-08-23T04:46:42.503Z
No $n!=n.n-1....2.1$ has sqrt(n) complexity.
Turbo
CC BY-SA 3.0
2015-08-23T22:53:07.037Z
It is not the simplest. Show the corresponding λ-term.
MaiaVictor
CC BY-SA 3.0
2015-08-24T04:25:55.343Z
It almost always will not be much larger than the natural statement, if it happens you are probably doing something wrong.
MaiaVictor
CC BY-SA 3.0
2015-08-24T04:56:03.253Z
As a case of study, I've just wrote several different sorting algorithms for church lists (insertion sort, quicksort, merge sort, and so on) as we know well. The normal form for all of those are huge and the performance is bad. I then wrote a sorting function aiming only a small term size. The resulting normal form fits in a twit and the performance is cosmically superior. Exploring the lambda calculus I find that is not an exception but almost always the rule. I need a solid counterexample it is not.
MaiaVictor
CC BY-SA 3.0
2015-08-24T14:41:20.600Z
I’m pretty sure you can code trial division by a shorter $\lambda$-term than the AKS algorithm.
Emil Jeřábek
CC BY-SA 3.0
2015-08-24T15:33:47.883Z
I agree with @EmilJeřábek and, actually, I don't see how an example is not obtained by looking at sorting algorithms, as you already did: isn't the $\lambda$-term implementing bubble sort shorter than the $\lambda$-term implmenting, say, heap sort?  Or, I don't know, a brute-force search, super short to implement but exponential time, vs. a clever polytime algorithm requiring more lines of code...?  I must be missing something, I am afraid I don't really understand the question.
Damiano Mazza
CC BY-SA 3.0
2015-08-24T16:12:31.013Z
I made no effort to actually write it down, but as a heuristic principle, the relative lengths of two algorithms are usually not affected very much by the choice of the programming language, and I see absolutely no reason $\lambda$-calculus should be an exception. Note in particular that normalization is a red herring here: the most natural way how to express algorithms in $\lambda$-calculus gives normal terms from the get-go, and anyway, IIRC from my experience with Unlambda, you can transform any term into a normal term of similar length giving the same result when applied.
Emil Jeřábek
CC BY-SA 3.0
2015-08-24T16:23:54.580Z
And yes, as Damiano mentions, AKS was just an example. The same should hold in more or less any situation where we have a trivial inefficient algorithm, and an efficient but much more sophisticated solution of the same problem.
Emil Jeřábek
CC BY-SA 3.0
2015-08-24T16:57:53.340Z
Since it seems like there is a lot of controversy, I've included a wall of text that might explain exactly what I'm trying to say. I'm sorry, I'm not good with formalizing intuition.
MaiaVictor
CC BY-SA 3.0
2015-08-24T17:04:11.770Z
It might be uninteresting, then, but of course the normal-form requirement is necessary as, as you said, it is easy to give a counterexample otherwise. With normal form I'm basically saying that all dependencies must be accounted for, which IMO is important to measure how complex it is. I'm specifically asking about normal forms since that is the effect I observed.
MaiaVictor
CC BY-SA 3.0
2015-08-24T17:07:27.783Z
@Kaveh: “Normalization is essentially the computation in lambda calculus”. Right. And normally you write an algorithm in its final form, not as a recipe how to compute the description of the algorithm. Most algorithms are naturally given in normal form, it takes a nontrivial sophistication/obfuscation to make a useful $\lambda$-term algorithm not in normal form.
Emil Jeřábek
CC BY-SA 3.0
2015-08-24T17:17:17.927Z
@Kaveh exactly, and this is one of the reasons I believe the "usual" definitions are often bloated and "there exists" a small definition that is much faster. We use so many dependencies without noticing - even addition is complex! Notice the "sort" function I posted doesn't have any dependency - it doesn't do any addition at all (which would be there if I used a for-loop), it doesn't even include binary comparisons! Yet, it just happens to exist on the space of λ-terms and be simpler and faster.
MaiaVictor
CC BY-SA 3.0
2015-08-24T17:21:32.117Z
Exactly, but I don't see very well where your guys are going. Kaveh said if you inline every addition you will a λ-term with a huge normal form. That is right. My observation is that there almost (always?) exists a term that is shorter and faster - which basically means the original algorithm is slow.
MaiaVictor
CC BY-SA 3.0
2015-08-24T17:26:53.977Z
Anyway Kaveh, I've read your comment several times but I'm not sure I understand it. Could you give an actual term? This term `(a b -> (a (c d e -> (c d (c d e))) b))` takes a church number, a church list, and returns the church list concatenated with itself `N` times. It looks rather small. You mean by fixing a specific `N`?
MaiaVictor
CC BY-SA 3.0
2015-08-24T17:44:22.117Z
@Kaveh I think I see what you are talking about and I don't really disagree with it. That is exactly why the normal form req is important, but I still think the question is interesting with it.
MaiaVictor
CC BY-SA 3.0
2015-08-24T17:47:05.193Z
Damiano, I think you understand what I'm asking, would you suggest that I rephrase it or just disregard the question?
MaiaVictor
CC BY-SA 3.0
2015-08-24T17:54:03.447Z
@Damiano, I think I see your and Emil's point: normalization of a term will take only a constant number of beta reductions. When given an input we can do them first any way as it will be a constant number of steps and does not matter in the asymptotic run time of the algorithm. (cleaned up my previous comments.)
Kaveh
CC BY-SA 3.0
2015-08-24T17:58:46.807Z
Viclib, from what Emil and I were saying, I think it is quite clear that there must exist two normal terms $t,t'$ implementing the same function, s.t. $size(t)>size(t')$ and $t$ is asymptotically faster than $t'$.  However, what you seem to be really asking is whether the shortest (normal) program implementing a fixed function is also always asymptotically optimal. As Kaveh was saying, that may be an interesting question.  To me, it sounds like it should be false for some obvious reason, although I can't quite see which reason...
Damiano Mazza
CC BY-SA 3.0
2015-08-24T18:05:28.100Z
*However, what you seem to be really asking is whether the shortest (normal) program implementing a fixed function is also always asymptotically optimal.*

That is not what I was asking but now that you said it that is what I am asking. :P
MaiaVictor
CC BY-SA 3.0
2015-08-24T18:45:28.627Z
I'd love to see that experiment, I don't think that is true.
MaiaVictor
CC BY-SA 3.0
2015-08-24T20:01:59.373Z
@DamianoMazza It is (I believe) faster because it runs through each "succ" constructor of each number exactly once, and as soon as it reaches the last "zero", it already returns the result. So it is merely a linear scan of the data. Any comparison based sorting obviously involve scanning every number several times, so it can't be faster. At least that is how my intuition go, I'm not claiming for sure and I certainly can't prove it! As with everything else I could be terribly mistake. Of course, this is the case because it is a list of church numbers. It is irrelevant for anything else.
MaiaVictor
CC BY-SA 3.0
2015-08-24T20:04:07.537Z
And yes, I'm using interactions and time as the parameter. Did you try running it, though? I'm not sure that would be replicable since that term is really strange: it seems like my optimal evaluator gives wrong results for some cases, like already sorted lists (the normal evaluator doesn't). I'm not sure if this is a bug of my evaluator or what it is. Anyway, if I split the function in 2, the optimal evaluator always give the right results.
MaiaVictor
CC BY-SA 3.0
2015-08-25T12:25:55.390Z
This comments section is getting a bit unwieldy. Some of these longer discussions should be done in chat.
Lev Reyzin
CC BY-SA 3.0
2017-05-22T00:42:56.997Z
@user13972 that sounds crazy...
MaiaVictor
CC BY-SA 4.0
2020-02-29T11:10:10.380Z
a much shorter fib = λn λf n (λc λa λb c b (λx a (b x))) (λx λy x) f f
John Tromp
CC BY-SA 4.0
2020-02-29T16:40:24.327Z
@JohnTromp nice!
MaiaVictor
<lo.logic><computability><pl.programming-languages><lambda-calculus>
An example where smallest normal lambda term is not fastest
MaiaVictor
# An example where smallest normal lambda term is not fastest

(Asked by: username_0 on 2015-08-23)

Let the $size$ of $\lambda$-terms be defined as follows:

$size(x) = 1$,
$size(λx.t) = size(t) + 1$,
$size(t s) = size(t) + size(s) + 1$.

Let the complexity of a $\lambda$-term $t$ be defined as 
the number of parallel beta reductions from $t x$ to its normal form
(using an optimal evaluator in Levy's sense).
I am looking for an example of two normal $\lambda$-terms for the same function where 
the larger term has lower complexity.
...
Edit for clarity
since it seems that it is not obvious what I'm asking, I'll try to give a solid example. There is often a belief that the "naive"/"simplest" definition of a function is slow and not optimal. Better performance increase the complexity of the term, since you need added data-structures, formulas, etc. A great example is fibonacci, which can be "naively" defined as:
-- The fixed fibonacci definition
fib_rec fib n =
    if (is_zero x) 
        then 1 
        else fib (n - 1) + f (n - 2)

-- Using church numbers instead of the λ-combinator to get a normal form
fib n = n fib_rec 0 n 

This is often regarded as the "simplest" definition of fib, and is very slow (exponential). If we expand the dependencies of fib (the usual definitions for church-number addition, pred, is_zero), and normalize it, we get this term:
fib = (λa.(a(λbc.(c(λdef.f)(λde.d)(λde.(de))
      (λde.(b(λfg.(c(λhi.(i(hf)))(λh.g)(λh.h)))
      d(b(λfg.(c(λhi.(i(h(λjk.(k(jf))))))(λhi.g)
      (λh.h)(λh.h)))de)))))(λbc.c)a))

Improvements such as memoization tables would make this term bigger. Yet, there exists a different term that is much smaller...
fib = (λa.(a(λb.(b(λcde.(e(λfg.(cf(dfg)))c))))
      (λb.(b(λcd.(cd))(λcd.d)))(λbc.b)))

and, curiously, is also asymptotically superior to the naive one, running in O(N). Of all definitions I'm aware, this is both the fastest and the simplest. The same effect happens with sort. "Naive" definitions such as bubble sort and insertion sort often get expanded to huge terms (20+ lines long), but there exists a small definition:
-- sorts a church list (represented as the fold) of church numbers
sort = λabc.a(λdefg.f(d(λhij.j(λkl.k(λmn.mhi)l)(h(λkl.l)i))
       (λhi.i(λjk.bd(jhk))(bd(h(λjk.j(λlm.m)k)c))))e)(λde.e)
       (λde.d(λfg.g)e)c

Which also happens to be faster, asymptotically, than every other definition I know. This observation leads me to believe that, as opposed to common belief, the simplest term, with smallest Kolmogorov complexity, is usually the faster. My question is basically wether there is any evidence of the opposite, although I'd have a hard time in formalizing it.

**Tags:** lo.logic, computability, pl.programming-languages, lambda-calculus
> **Comments:**
> **username_1**: No $n!=n.n-1....2.1$ has sqrt(n) complexity.  
> **username_0**: It is not the simplest. Show the corresponding λ-term.  
> **username_0**: It almost always will not be much larger than the natural statement, if it happens you are probably doing something wrong.  
> **username_0**: As a case of study, I've just wrote several different sorting algorithms for church lists (insertion sort, quicksort, merge sort, and so on) as we know well. The normal form for all of those are huge and the performance is bad. I then wrote a sorting function aiming only a small term size. The resulting normal form fits in a twit and the performance is cosmically superior. Exploring the lambda calculus I find that is not an exception but almost always the rule. I need a solid counterexample it is not.  
> **username_2**: I’m pretty sure you can code trial division by a shorter $\lambda$-term than the AKS algorithm.  
> **username_3**: I agree with @EmilJeřábek and, actually, I don't see how an example is not obtained by looking at sorting algorithms, as you already did: isn't the $\lambda$-term implementing bubble sort shorter than the $\lambda$-term implmenting, say, heap sort?  Or, I don't know, a brute-force search, super short to implement but exponential time, vs. a clever polytime algorithm requiring more lines of code...?  I must be missing something, I am afraid I don't really understand the question.  
> **username_2**: I made no effort to actually write it down, but as a heuristic principle, the relative lengths of two algorithms are usually not affected very much by the choice of the programming language, and I see absolutely no reason $\lambda$-calculus should be an exception. Note in particular that normalization is a red herring here: the most natural way how to express algorithms in $\lambda$-calculus gives normal terms from the get-go, and anyway, IIRC from my experience with Unlambda, you can transform any term into a normal term of similar length giving the same result when applied.  
> **username_2**: And yes, as Damiano mentions, AKS was just an example. The same should hold in more or less any situation where we have a trivial inefficient algorithm, and an efficient but much more sophisticated solution of the same problem.  
> **username_0**: Since it seems like there is a lot of controversy, I've included a wall of text that might explain exactly what I'm trying to say. I'm sorry, I'm not good with formalizing intuition.  
> **username_0**: It might be uninteresting, then, but of course the normal-form requirement is necessary as, as you said, it is easy to give a counterexample otherwise. With normal form I'm basically saying that all dependencies must be accounted for, which IMO is important to measure how complex it is. I'm specifically asking about normal forms since that is the effect I observed.  
> **username_2**: @Kaveh: “Normalization is essentially the computation in lambda calculus”. Right. And normally you write an algorithm in its final form, not as a recipe how to compute the description of the algorithm. Most algorithms are naturally given in normal form, it takes a nontrivial sophistication/obfuscation to make a useful $\lambda$-term algorithm not in normal form.  
> **username_0**: @Kaveh exactly, and this is one of the reasons I believe the "usual" definitions are often bloated and "there exists" a small definition that is much faster. We use so many dependencies without noticing - even addition is complex! Notice the "sort" function I posted doesn't have any dependency - it doesn't do any addition at all (which would be there if I used a for-loop), it doesn't even include binary comparisons! Yet, it just happens to exist on the space of λ-terms and be simpler and faster.  
> **username_0**: Exactly, but I don't see very well where your guys are going. Kaveh said if you inline every addition you will a λ-term with a huge normal form. That is right. My observation is that there almost (always?) exists a term that is shorter and faster - which basically means the original algorithm is slow.  
> **username_0**: Anyway Kaveh, I've read your comment several times but I'm not sure I understand it. Could you give an actual term? This term `(a b -> (a (c d e -> (c d (c d e))) b))` takes a church number, a church list, and returns the church list concatenated with itself `N` times. It looks rather small. You mean by fixing a specific `N`?  
> **username_0**: @Kaveh I think I see what you are talking about and I don't really disagree with it. That is exactly why the normal form req is important, but I still think the question is interesting with it.  
> **username_0**: Damiano, I think you understand what I'm asking, would you suggest that I rephrase it or just disregard the question?  
> **username_4**: @Damiano, I think I see your and Emil's point: normalization of a term will take only a constant number of beta reductions. When given an input we can do them first any way as it will be a constant number of steps and does not matter in the asymptotic run time of the algorithm. (cleaned up my previous comments.)  
> **username_3**: Viclib, from what Emil and I were saying, I think it is quite clear that there must exist two normal terms $t,t'$ implementing the same function, s.t. $size(t)>size(t')$ and $t$ is asymptotically faster than $t'$.  However, what you seem to be really asking is whether the shortest (normal) program implementing a fixed function is also always asymptotically optimal. As Kaveh was saying, that may be an interesting question.  To me, it sounds like it should be false for some obvious reason, although I can't quite see which reason...  
> **username_0**: *However, what you seem to be really asking is whether the shortest (normal) program implementing a fixed function is also always asymptotically optimal.*  That is not what I was asking but now that you said it that is what I am asking. :P  
> **username_0**: I'd love to see that experiment, I don't think that is true.  
> **username_0**: @DamianoMazza It is (I believe) faster because it runs through each "succ" constructor of each number exactly once, and as soon as it reaches the last "zero", it already returns the result. So it is merely a linear scan of the data. Any comparison based sorting obviously involve scanning every number several times, so it can't be faster. At least that is how my intuition go, I'm not claiming for sure and I certainly can't prove it! As with everything else I could be terribly mistake. Of course, this is the case because it is a list of church numbers. It is irrelevant for anything else.  
> **username_0**: And yes, I'm using interactions and time as the parameter. Did you try running it, though? I'm not sure that would be replicable since that term is really strange: it seems like my optimal evaluator gives wrong results for some cases, like already sorted lists (the normal evaluator doesn't). I'm not sure if this is a bug of my evaluator or what it is. Anyway, if I split the function in 2, the optimal evaluator always give the right results.  
> **username_5**: This comments section is getting a bit unwieldy. Some of these longer discussions should be done in chat.  
> **username_0**: @user13972 that sounds crazy...  
> **username_6**: a much shorter fib = λn λf n (λc λa λb c b (λx a (b x))) (λx λy x) f f  
> **username_0**: @JohnTromp nice!  

---

## 1 answers

### Answer by username_2 on 2015-08-25. Score: 11

[Blum’s speedup theorem](https://en.wikipedia.org/wiki/Blum%27s_speedup_theorem) is usually stated in the language of partially recursive functions, but up to trivial differences in notation, it works just the same in the language of $\lambda$-calculus.

It says that given any reasonable complexity measure $M$ (for example, the optimal number of reductions as in the question) and a recursive function $f(x,y)$ (for example, $2^y$), we can find a recursive predicate $P(x)$ such that:

> For every algorithm (i.e., $\lambda$-term in normal form here) $g$ computing $P$, there is another algorithm $h$ for $P$ that has $f$-speedup over $g$:
> $$f(x,M(h,x))\le M(g,x)\text{ for all large enough inputs }x,$$

where $M(g,x)$ denotes the complexity of the computation of $g$ on input $x$ according to measure $M$.

Consequently:

* $P$ has no asymptotically optimal algorithm in the given measure
* in particular, the shortest algorithm for $P$ is not asymptotically optimal
* for any algorithm for $P$, there is an asymptotically faster algorithm whose normal form is longer (because up to renaming of variables, there are only finitely many normal terms of a given length)


---

