Computation is something different. Models like call by push value make this very clear. LC does as well, though, but LC tends to be joined up with an equality semantics which intentionally sweeps computation under the rug for simplicity.<p>This is a big hairy problem in untyped LC, though, since untyped LC has non-termination and therefore is not confluent. This is what I mean by taking non-termination seriously is one way to force &quot;time&quot; and &quot;computation&quot; back into models. It means that LC has no beta-equivalence the same way that, say, simply typed LC does.<p>So anyway, you&#x27;re wrong to say that LC has no notion of complexity—people count reduction steps all the time—but right to say that often this is intentionally ignored to provide simpler value semantics. It&#x27;s foolish to think of this as equivalent to LC, though.<p>This paper is interesting. I think what they prove was at least folk belief for a long time, but I&#x27;ve never seen a proof.