I been reading about $\lambda$-calculus and related stuff, but I got some confusions which i want to clarify.

The call by value reduction is expressed with two rules

$$ \frac{e_1 \rightarrow e_1'}{e_1e_2 \rightarrow e_1'e_2} $$ and $$ \frac{e_2 \rightarrow e_2'}{ve_2 \rightarrow ve_2'}. $$

where $e$ is any lambda term and $v$ is a value (abstraction of the form $\lambda x.M$).

I encountered evaluation context while reading this paper source, on page 10, I did not understand the following expressions.

Evaluation context(left-to right: hole, app fun, app arg, type fun) $$ E ::= [-] \mid E \,t \mid v \,E \mid E \,[T] $$

and E-CTX

$$ \frac{t_1 \rightarrow t_1'}{E[e_1] \rightarrow E[e_1']} $$

and description below said

E-CTX permits reduction under any arbitrary evaluation context $E$.

So I did not understand above statement, and because I have no knowledge about evaluation context. I searched other posts and googled, but could not get useful clear descriptions.

(1) what is that evaluation context, why there is such thing?

(2) what does evaluation context do with call by value reduction? why not just say "call by value is used here, bla bla..."

(3) E-CTX permits ...., what does that mean?

(4) I think someone has to implement call by value together with polymorphic $\lambda$-calculus. But what about evaluation context, should it be be implemented somehow (which I have no idea now ) ?

Could you guys point out useful sources to read or just answer here if possible? I am around this for a while, so it would be big help. Thanks in advance!

  • 1
    $\begingroup$ (1) To express the call-by-value reduction you need one more rule in addition to those 2 rules you have at the beginning of your question. (2) Have a look at these lecture notes -- they show the missing rule and explain the concept of evaluation contexts. $\endgroup$ – Anton Trunov Jul 1 '16 at 7:57
  • $\begingroup$ @AntonTrunov (1) you mean beta-reduction, right? (2) I am reading the source you have pointed, thanks :) $\endgroup$ – alim Jul 1 '16 at 9:14
  • $\begingroup$ Yes, $\beta$-reduction, with one important detail: the operand of an application must be a value, it's rule (1) in the notes. $\endgroup$ – Anton Trunov Jul 1 '16 at 9:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.