Optimality and Inefficiency: What Isn't a Cost Model of the Lambda Calculus?

Abstract

We investigate the computational efficiency of the sharing graphs of Lamping [Lam90], Gonthier, Abadi, and Lévy [GAL92], and Asperti [Asp94], designed to effect so-called optimal evaluation, with the goal of reconciling optimality, efficiency, and the clarification of reasonable cost models for the λ-calculus. Do these graphs suggest reasonable cost models for the λ-calculus? If they are optimal, are they efficient?We present a brief survey of these optimal evaluators, identifying their common characteristics, as well as their shared failures. We give a lower bound on the efficiency of sharing graphs by identifying a class of λ-terms that are normalizable in Θ(n) time, and require Θ(n) "fan interactions," but require Ω(2n) bookkeeping steps. For [GAL92], we analyze this anomaly in terms of the dynamic maintenance of deBruijn indices for intermediate terms. We give another lower bound showing that sharing graphs can do Ω(2n) work (via fan interactions) on graphs that have no β-redexes. Finally, we criticize a proposed cost model for λ-calculus given by Frandsen and Sturtivant [FS91], showing by example that the model does not take account of the size of intermediate forms. Our example is a term requiring Θ(2n) steps while having proposed cost Θ(n). We propose some cost models that both reflect this parameter, and simultaneously reconcile key concepts from optimal reduction.