1

While trying to summarize my knowledge about lambda calculus, I understood that I'm quite familiar with call-by-value but I've never seen сall-by-need reduction semantics. I know the definition, but it would be great to see precise meaning.

This is what I have for call-by-need and call-by-value (not very detailed description):

Call-by-value

Small Step

  • Values

    values

  • β-reduction

    βv

  • Evaluation context

    context

    cbv context

Big Step (with closures and environment)

  • Closures

    closures

  • Environment

    environment

  • Reduction

    cbv var

    cbv lam

    cbv app

Call-by-name

Small Step

  • β-reduction

    Nβv

  • Evaluation context

    cbn context

    cbn eval context

I guess there is also a big step, which must be quite similar to call-by-value, but once again, its better to see it once.

So I will be grateful if someone can extend my list with call-by-need.

vonaka
  • 913
  • 1
  • 11
  • 23

1 Answers1

0

Currently I cannot write this in Tex, but the main thing is: when using pure functions the evaluated value of a function with the same parameter(s) will be always the same, so while you are in the same body, you can use the evaluated reference instead of evaluating it again.

For more information see: http://repository.readscheme.org/ftp/papers/plsemantics/felleisen/jfp96-af.pdf

Ádám Révész
  • 231
  • 2
  • 8