Table of Links Introduction


Translating To Sequent Calculus
2.1 Arithmetic Expressions
2.2 Let Bindings
2.3 Top-level Definitions
2.4 Algebraic Data and Codata Types
2.5 First-Class Functions
2.6 Control Operators


Evaluation Within a Context
3.1 Evaluation Contexts for Fun
3.2 Focusing on Evaluation in Core


Typing Rules
4.1 Typing Rules for Fun
4.2 Typing Rules for Core
4.3 Type Soundness


Insights
5.1 Evaluation Contexts are First Class
5.2 Data is Dual to Codata
5.3 Let-Bindings are Dual to Control Operators
5.4 The Case-of-Case Transformation
5.5 Direct and Indirect Consumers
5.6 Call-By-Value, Call-By-Name and Eta-Laws
5.7 Linear Logic and the Duality of Exceptions


Related Work


Conclusion, Data Availability Statement, and Acknowledgments Introduction Introduction Introduction Introduction Translating To Sequent Calculus
2.1 Arithmetic Expressions
2.2 Let Bindings
2.3 Top-level Definitions
2.4 Algebraic Data and Codata Types
2.5 First-Class Functions
2.6 Control Operators Translating To Sequent Calculus Translating To Sequent Calculus 2.1 Arithmetic Expressions 2.1 Arithmetic Expressions 2.2 Let Bindings 2.2 Let Bindings 2.3 Top-level Definitions 2.3 Top-level Definitions 2.4 Algebraic Data and Codata Types 2.4 Algebraic Data and Codata Types 2.5 First-Class Functions 2.5 First-Class Functions 2.6 Control Operators 2.6 Control Operators Evaluation Within a Context
3.1 Evaluation Contexts for Fun
3.2 Focusing on Evaluation in Core Evaluation Within a Context Evaluation Within a Context 3.1 Evaluation Contexts for Fun 3.1 Evaluation Contexts for Fun 3.2 Focusing on Evaluation in Core 3.2 Focusing on Evaluation in Core Typing Rules
4.1 Typing Rules for Fun
4.2 Typing Rules for Core
4.3 Type Soundness Typing Rules Typing Rules Typing Rules 4.1 Typing Rules for Fun 4.1 Typing Rules for Fun 4.2 Typing Rules for Core 4.2 Typing Rules for Core 4.3 Type Soundness 4.3 Type Soundness Insights
5.1 Evaluation Contexts are First Class
5.2 Data is Dual to Codata
5.3 Let-Bindings are Dual to Control Operators
5.4 The Case-of-Case Transformation
5.5 Direct and Indirect Consumers
5.6 Call-By-Value, Call-By-Name and Eta-Laws
5.7 Linear Logic and the Duality of Exceptions Insights Insights 5.1 Evaluation Contexts are First Class 5.1 Evaluation Contexts are First Class 5.2 Data is Dual to Codata 5.2 Data is Dual to Codata 5.3 Let-Bindings are Dual to Control Operators 5.3 Let-Bindings are Dual to Control Operators 5.4 The Case-of-Case Transformation 5.4 The Case-of-Case Transformation 5.5 Direct and Indirect Consumers 5.5 Direct and Indirect Consumers 5.6 Call-By-Value, Call-By-Name and Eta-Laws 5.6 Call-By-Value, Call-By-Name and Eta-Laws 5.7 Linear Logic and the Duality of Exceptions 5.7 Linear Logic and the Duality of Exceptions Related Work Related Work Related Work Related Work Conclusion, Data Availability Statement, and Acknowledgments Conclusion, Data Availability Statement, and Acknowledgments Conclusion, Data Availability Statement, and Acknowledgments Conclusion, Data Availability Statement, and Acknowledgments A. The Relationship to the Sequent Calculus A. The Relationship to the Sequent Calculus B. Typing Rules for Fun B. Typing Rules for Fun C. Operational Semantics of label/goto C. Operational Semantics of label/goto References References 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(𝔱; 𝛼)]}] ⊲ 𝐸[𝔱] 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. Fun label goto Core 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. Authors: 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. This paper is available on arxiv under CC BY 4.0 license. This paper is available on arxiv under CC BY 4.0 license. available on arxiv available on arxiv

Part of HackerNoon's growing list of open-source research papers, promoting free access to academic material.

How Focusing Resolves Stuck Terms in Core Evaluation

How Functional Languages Simulate Goto with Labels and μ-Bindings

Read My Stories

Too Long; Didn't Read

Make resilience your competitive advantage

An Introduction to Evaluation Contexts in Programming Semantics

About Author

Comments

TOPICS

THIS ARTICLE WAS FEATURED IN

Related Stories

Untitled Story

What Sequent Calculus Teaches Us About Computation

Rules of Thumb for Software Engineering

Building a cupboard

What is Code Review and Why We Need to Keep Doing It

How to Find the Stinky Parts of Your Code: 251 - Empty Collections

What Sequent Calculus Teaches Us About Computation

Rules of Thumb for Software Engineering

Building a cupboard

What is Code Review and Why We Need to Keep Doing It

How to Find the Stinky Parts of Your Code: 251 - Empty Collections

Light-Mode

Classic

Newspaper

Dark-Mode

Neon Noir

Minty

HN StartUps