scrambled
scrambled
Concept

Call by value

Modified just now
Books JourneyProgramming Language Theory Statusmastered Tags
  • language-feature-design
  • semantics

INFO

(Lambda calculus, Semantics) A Strict/Eager evaluation strategy in which Beta-redex/Reducible expressions inside lambda abstractions must not be reduced.

In pure lambda calculus, this strategy is defined by the following rules:

  • t1→t1′t1 t2→t1′ t2\displaystyle \frac{t_1 \to t_1'}{t_1\ t_2 \to t_1'\ t_2}
  • t2→t2′v1 t2→v1 t2′\displaystyle \frac{t_2 \to t_2'}{v_1\ t_2 \to v_1\ t_2'}
  • (λx. t) v→[x→v]t(\lambda x.\ t)\ v \to [x \to v] t