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.




B. Accattoli, U. Dal Lago, Beta Reduction is Invariant, Indeed.
J.-J. Levy, Reductions correctes et optimales dans le lambda-calcul.
J. L. Lawall, H. G. Mairson, Optimality and inefficiency: what isn't
a cost model of the lambda calculus? 
A. Asperti, H. Mairson,
Parallel beta reduction is not elementary recursive.
D. Mazza, Church Meets Cook and Levin.