Semantics of λ

Reading: TAPL 5.3.

Page 72 gives evaluation rules for the call-by-value λ-calculus.

Evaluation contexts

Recall (in the semantics of NB) that we can also write small-step operational semantics using evaluation contexts. For the call-by-value λ-calculus, they are defined as:

E ::= [⋅]
      E1 t2
      v1 E2

Intuitively, the rule E ::= E t means that in an application, we can evaluate inside the function being applied, and the rule E ::= v E means that we can only evaluate inside the argument after we’re finished evaluating the function.

Then we can replace the congruence rules (E-App1 and E-App2) with a single rule, just like in NB:

   t ⟶ t'
――――――――――――――  (E-Context)
E[t] ⟶ E[t']

Big-step semantics

Just as we wrote big-step evaluation rules for NB, we can write big-step evaluation rules for λ. They are given in the solution to Exercise 5.3.8:

            —————————————                 (B-Abs)
            λx. t ⇓ λx. t

t1 ⇓ λx. t12   t2 ⇓ v2   [x↦v2]t12 ⇓ v
———————————————————————————————————————   (B-App)
              t1 t2 ⇓ v