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-byname/valueeed). 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/valueeed), 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.
展开▼
