This content originally appeared on HackerNoon and was authored by Abstraction: Computer Science Discourse
Table of Links
Translating To Sequent Calculus
Evaluation Within a Context
Insights
5.1 Evaluation Contexts are First Class
5.3 Let-Bindings are Dual to Control Operators
5.4 The Case-of-Case Transformation
5.5 Direct and Indirect Consumers
Conclusion, Data Availability Statement, and Acknowledgments
A. The Relationship to the Sequent Calculus
C. Operational Semantics of label/goto
3 Evaluation Within a Context
At the end of Section 2.1 we ran into the problem that we cannot yet fully evaluate the term (⌜2⌝ ∗ ⌜4⌝) + ⌜5⌝ in Fun or its translation 𝜇𝛼. + (𝜇𝛽. ∗ (⌜2⌝, ⌜4⌝; 𝛽), ⌜5⌝; 𝛼) in Core with the rules that are available to us: we are stuck. In this section, we finally address this problem. We are going to show how we can evaluate subexpressions of Fun in Section 3.1, but since we are ultimately more interested in compiling programs into Core to optimize and reduce those programs, we are spending more time on the problem for Core in Section 3.2.
3.1 Evaluation Contexts for Fun
The problem with evaluating the term (⌜2⌝ ∗ ⌜4⌝) + ⌜5⌝ is that the available rules only allow to reduce direct redexes and not redexes that are nested somewhere within a term. Evaluation contexts solve this problem by specifying the locations within a term which are in evaluation position. In our example, the term (⌜2⌝ ∗ ⌜4⌝) + ⌜5⌝ can be factored into the evaluation context □+ ⌜5⌝ and the redex ⌜2⌝ ∗ ⌜4⌝. We can then use the old rules to reduce this redex to ⌜8⌝ and then plug this result back into the evaluation context, which yields the new term ⌜8⌝ + ⌜5⌝. The syntax of evaluation contexts is given in Definition 3.1.
\
\ These evaluation contexts also allow us to specify formally the second approximate evaluation rule of the label and goto constructs from Section 2.6:
\ 𝐸[label 𝛼 {𝐸 ′ [goto(𝔱; 𝛼)]}] ⊲ 𝐸[𝔱]
\ Here we again assume that 𝛼 does not occur free in 𝔱 and moreover that the inner evaluation context 𝐸 ′ does not contain another label construct. For the full operational semantics of label/goto we also need to handle the cases where 𝛼 can occur free in 𝔱 and where 𝐸 ′ can contain other labels. Otherwise, we could get stuck during evaluation even for closed and well-typed terms, i.e., the progress theorem (see Theorem 4.1 in Section 4.3) would not hold. As the full semantics is in essence that of other classical control operators (i.p., let/cc; also see the discussion in Section 5.3) and requires some more formalism, we do not give it here and instead refer the interested reader to the brief discussion in Appendix C.
\ With evaluation contexts, we finally have a working and precise operational semantics for Fun (apart from the approximate rules for label and goto) which we can use to reason about programs. Unfortunately, it is wildly inefficient to implement an evaluator which uses evaluation contexts in the way described above. The reason for this inefficiency is that we very elegantly specified how a term can be factored into an evaluation context and a redex, but the evaluator which implements this behavior has to search for the next redex after every single evaluation step. We will see in the next section that we have a better solution once our programs are compiled into Core.
\
:::info Authors:
(1) David Binder, University of Tübingen, Germany;
(2) Marco Tzschentke, University of Tübingen, Germany;
(3) Marius Muller, University of Tübingen, Germany;
(4) Klaus Ostermann, University of Tübingen, Germany.
:::
:::info This paper is available on arxiv under CC BY 4.0 license.
:::
\
This content originally appeared on HackerNoon and was authored by Abstraction: Computer Science Discourse
Abstraction: Computer Science Discourse | Sciencx (2025-07-06T23:58:20+00:00) An Introduction to Evaluation Contexts in Programming Semantics. Retrieved from https://www.scien.cx/2025/07/06/an-introduction-to-evaluation-contexts-in-programming-semantics/
Please log in to upload a file.
There are no updates yet.
Click the Upload button above to add an update.