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.