If you assume that the $\lambda$-calculus is a good model of functional programming languages, then one may think: the $\lambda$-calculus has a
seemingly simple notion of
time-complexity: just count
the number of $\beta$-reduction
steps $(\lambda x.M)N \rightarrow M[N/x]$.
But is this a good complexity measure?
To answer this
question, we should clarify what we mean by complexity measure in the
first place. One good answer is given by the Slot and van Emde
Boas thesis: any good complexity measure should have
a polynomial
relationship to the canonical notion of time-complexity defined using
Turing machines. In other words, there should be a 'reasonable'
encoding $tr(.)$ from $\lambda$-calculus terms to Turing machines, such for some polynomial $p$, it is the case that for
each term $M$ of size $|M|$: $M$ reduces to a value in $p(|M|)$ $\beta$-reduction steps exactly
when $tr(M)$ reduces to a value in $p(|tr(M)|)$ steps of a Turing machine.
For a long time, it was unclear if this can be achieved in the λ-calculus. The main problems are the following.
- There are terms that produce normal forms (in a polynomial number of steps) that are of exponential size. Even writing down the normal forms takes exponential time.
- The chosen reduction strategy plays an important role. For example there exists a family of terms which reduces in a polynomial number of parallel β-steps (in the sense of optimal λ-reduction), but whose complexity is non-elementary (meaning worse then exponential).
The paper "Beta Reduction is Invariant, Indeed" by B. Accattoli and U. Dal Lago clarifies the issue by showing a 'reasonable' encoding that preserves the complexity class P of polynomial time functions, assuming leftmost-outermost call-by-name reductions. The key insight is the exponential blow-up can only happen for 'uninteresting' reasons which can be defeated by proper sharing. In other words, the class P is the same whether you define it counting Turing machine steps or (leftmost-outermost) $\beta$-reductions.
I'm not sure what the situation is for other evaluation strategies.
I'm not aware that a similar programme has been carried out for space complexity.
ST
monads). $\endgroup$