consider the following [[operational semantics of the pure lambda calculus|call by value]] [[operational semantics]], defined via [[evaluation context]]s, for multi-argument $\lambda$-calculus: ![[Screen Shot 2023-03-02 at 2.25.05 AM.png]] Can define a [[definitional translation]] to pure $\lambda$-calculus: ![[Screen Shot 2023-03-02 at 2.25.27 AM.png]]