In "Call-by-push-value: A subsuming paradigm." (Levy, Paul Blain. Springer, Dordrecht, 2003. 27-47) terms of the lambda calculus get split in to values and computations, with the slogan "A value is, a computation does".

What I don't understand is: why are abstractions computations and not values? Intuitively a function does not do anything and can be used as data. It will only do something when applied to something.


1 Answer 1


thanks for your interest in call-by-push-value. The fact that functions (all functions, not just lambda-abstractions) are computations is the main difference between call-by-push-value and call-by-value (where functions are values), and it does seem strange at first. But the mystery is (somewhat) resolved when you see the CK-machine, which is a kind of operational semantics that uses a computation and a stack. In terms of that machine, a function of type A -> B is a computation that aims to pop a value of type A and then behave as a computation of type B. For example:

    print "hello".
    lambda x.
    print "hello again".
    return x

is a computation that first prints "hello", then pops x ("lambda" means "pop"), then prints "hello again", then returns x. And actually, the same phenomenon of "lambda" as "pop" is present in call-by-name; that's why call-by-push-value manages to subsume call-by-name.

I hope that helps! I should also say that the origin of call-by-push-value is that it was empirically observed within the models. The slogan was designed to fit the language and not the other way round. But that's just saying probably a less helpful answer, because it's just saying "the language is that way because the models say so".

  • $\begingroup$ What is the advantage of CBPV over FG-CBV? It seems to me that FG-CBV does everything that CBPV does (explicit evaluation order, thunks can be done with abstractions). $\endgroup$
    – Labbekak
    Commented Aug 17, 2018 at 12:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.