The Negligible and yet subtle cost of pattern matching

The model behind functional programming languages is the closed λ -calculus, that is, the fragment of the λ -calculus where evaluation is weak (i.e. out of abstractions) and terms are closed. It is well-known that the number of β (i.e. evaluation) steps is a reasonable cost model in this setting, for all natural evaluation strategies (call-by-name/value/need). In this paper we try to close the gap between the closed λ -calculus and actual languages, by considering an extension of the λ -calculus with pattern matching. It is straightforward to prove that β plus matching steps provide a reasonable cost model. What we do then is finer: we show that β steps only, without matching steps, provide a reasonable cost model also in this extended setting—morally, pattern matching comes for free, complexity-wise. The result is proven for all evaluation strategies (name/value/need), and, while the proof itself is simple, the problem is shown to be subtle. In particular we show that qualitatively equivalent definitions of call-by-need may behave very differently.