The lambda calculus is a widely accepted computational model of higher-order
functional pro- grams, yet there is not any direct and universally accepted
cost model for it. As a consequence, the computational difficulty of reducing
lambda terms to their normal form is typically studied by reasoning on concrete
implementation algorithms. In this paper, we show that when head reduction is
the underlying dynamics, the unitary cost model is indeed invariant. This
improves on known results, which only deal with weak (call-by-value or
call-by-name) reduction. Invariance is proved by way of a linear calculus of
explicit substitutions, which allows to nicely decompose any head reduction
step in the lambda calculus into more elementary substitution steps, thus
making the combinatorics of head-reduction easier to reason about. The
technique is also a promising tool to attack what we see as the main open
problem, namely understanding for which normalizing strategies derivation
complexity is an invariant cost model, if any.