An example where smallest normal lambda term is not fastest 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.
Blum’s 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)