# Equivalent formulation of complexity theory in Lambda Calculus?

In complexity theory the definition of time and space complexity both reference a universal Turing machine: resp. the number of steps before halting, and the number of cells on the tape touched.

Given the Church-Turing thesis, it should be possible to define complexity in terms of lambda calculus as well.

My intuitive notion is that time complexity can be expressed as the number of β-reductions (we can define away α-conversion by using De Brujin indexes, and η is barely a reduction anyway), while space complexity can be defined as the number of symbols (λ's, DB-indexes, “apply”-symbols) in the largest reduction.

Is this correct? If so, where can I get a reference? If not, how am I mistaken?

As you point out, the λ-calculus has a seemingly simple notion of time-complexity: just count the number of β-reduction steps. Unfortunately, things are not simple. We should ask:

 Is counting β-reduction steps 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 λ-calculus terms to Turing machines, such that for each term $$M$$ of size $$|M|$$: $$M$$ reduces to a value in $$poly(|M|)$$ exactly when $$tr(M)$$ reduces to a value in $$poly(|tr(M)|)$$.

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. See (1). Even writing down the normal forms takes exponential time.

• The chosen reduction strategy plays an important role, too. For example there exists a family of terms which reduces in a polynomial number of parallel β-steps (in the sense of optimal λ-reduction (2), but whose complexity is non-elementary (3, 4).

The paper (1) clarifies the issue by showing a reasonable encoding that preserves the complexity class PTIME assuming leftmost-outermost Call-By-Name reductions. The key insight appears to be that the exponential blow-up can only happen for uninteresting reasons which can be defeated by proper sharing of sub-terms.

Note that papers like (1) show that coarse complexity classes like PTIME coincide, whether you count β-steps, or Turing-machine steps. That does not mean lower complexity classes like O(log n) also coincide. Of course such complexity classes are also not stable under variation of Turing machine model (e.g. 1-tape vs multi-tape).

D. Mazza's work (5) proves the Cook-Levin theorem (𝖭𝖯-completeness of SAT) using a functional language (a variant of the λ-calculus) instead of Turing machines. The key insight is this:

$$\frac{\text{Boolean circuits}}{\text{Turing machines}}=\frac{\text{affine \lambda-terms}}{\text{\lambda-terms}}$$

I don't know if the situation regarding space complexity is understood.

1. B. Accattoli, U. Dal Lago, Beta Reduction is Invariant, Indeed.

2. J.-J. Levy, Reductions correctes et optimales dans le lambda-calcul.

3. J. L. Lawall, H. G. Mairson, Optimality and inefficiency: what isn't a cost model of the lambda calculus?

4. A. Asperti, H. Mairson, Parallel beta reduction is not elementary recursive.

5. D. Mazza, Church Meets Cook and Levin.

Counting $$\beta$$-reductions is one kind of complexity measure for $$\lambda$$-calculus, but a more flexible and reasonable one is cost semantics, where the operational semantics is augmented by various notions of cost. One good starting point are the OPLSS 2018 lectures on cost semantics by Jan Hoffmann (videos and lecture materials available at the link).

A note about space complexity. While, as pointed out by Martin in his answer, the naive way to count time complexity turns out to work well, the definition of space complexity you suggest is easily seen to be inadequate. Indeed, in the case of space you really want to be able to speak of sublinear complexity, e.g. you want to be able to recover the class $$\mathsf L$$ (deterministic logspace, which is to space a bit what $$\mathsf P$$ is to time), and your definition obviously does not allow you to do that: in any reduction $$M\to^\ast N$$, your are counting at least the size of $$M$$, which is linear in the input size.

The moral of the story is that rewriting is not suitable for counting space. Ulrich Schöpp and Ugo Dal Lago were the first to advocate the use of the so-called geometry of interaction (GoI) for dealing with sublinear space complexity (cf. their ESOP 2010 paper "Functional Programming in Sublinear Space"). As far as I know, the GoI is used in one way or another in all lambda-calculus-based characterizations of sublinear space classes. I do not want to get into what the GoI is here; let's say that it is a way of executing a lambda-term without reducing it (i.e., without firing $$\beta$$-redexes) but by "traveling" through its syntactic tree with a certain auxiliary information.