What Sequent Calculus Teaches Us About Computation | HackerNoon

Table of Links

1. Introduction

2. 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

3. Evaluation Within a Context

   3.1 Evaluation Contexts for Fun

   3.2 Focusing on Evaluation in Core

4. Typing Rules

   4.1 Typing Rules for Fun

   4.2 Typing Rules for Core

   4.3 Type Soundness

5. 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

6. Related Work

7. Conclusion, Data Availability Statement, and Acknowledgments

A. The Relationship to the Sequent Calculus

B. Typing Rules for Fun

C. Operational Semantics of label/goto

References

A The Relationship to the Sequent Calculus

In the main part of the paper we introduced the 𝜆𝜇𝜇˜-calculus without any references to the sequent calculus, because we think it is not essential to understand the latter in order to understand the former. In this appendix, we provide the details which help make the connection between the logical calculus and the term system clear. We only discuss a very simple sequent calculus which contains two logical connectives: the two conjunctions 𝐴 ⊗ 𝐵 and 𝐴 & 𝐵 which correspond to the strict and lazy pairs that we have seen in Core. We use 𝑋 for propositional variables.

𝐴, 𝐵 F 𝑋 | 𝐴 ⊗ 𝐵 | 𝐴 & 𝐵

In the (classical) sequent calculus both the premisses and the conclusion of a derivation rule consist of sequents Γ ⊢ Δ. Both Γ and Δ are multisets of formulas; that is, it is important how often a formula occurs on the left or the right, but not in which order the formulas occur. In the sequent calculus, we only have introduction rules. This means that the logically complex formula 𝐴 ⊗ 𝐵 or 𝐴 & 𝐵 only occurs in the conclusion of the rules that define it, and not in one of the premises. Every connective comes with a set of rules which introduce the connective on the left and the right of the turnstile. In our case, the rules look like this:

The rule Cut is the only rule which destroys the so-called subformula property. This property says that every formula which occurs anywhere in a derivation is a subformula of a formula occurring in the conclusion of the derivation. Proof theorists therefore try to show that we can eliminate the cuts; if every sequent which can be derived using the Cut rule can also be derived without using it, we say that the calculus enjoys the cut-elimination property. The Curry-Howard correspondence for the sequent calculus relates this cut-elimination procedure to the computations that we have seen in the paper.

The first step from the sequent calculus towards the 𝜆𝜇𝜇˜-calculus consists in marking at most one of the formulas in each of the sequents as active. We mark a formula as active by enclosing it in a pair of brackets. This yields two versions of the rule Axiom, one where we mark the formula on the left and one where we mark the formula on the right. If we want to translate every derivation using the original rules to a derivation in the new variant we also have to add special rules which activate and deactivate formulas both on the left and on the right. This yields the following new set of rules:

B Typing Rules for Fun

Given a term 𝑡, an environment Γ and a program 𝑃, if 𝑡 has type 𝜏 in environment Γ and program 𝑃, we write Γ ⊢𝑃 𝑡 : 𝜏. As 𝑃 is only used for typing calls to top-level definitions (rule Call), we usually leave it implicit in the typing rules. To make sure programs 𝑃 are well-formed, we have additional checking rules for programs ∅-ok and P-Ok. If a program is well-formed, we write ⊢ 𝑃 Ok.

C Operational Semantics of label/goto

The full operational semantics for the label/goto construct is in essence the same as for let/cc. To make it precise, we promote evaluation contexts to runtime values

We first repeat Definition 3.1 of evaluation contexts with one change: label 𝛼 {𝐸} is not an evaluation context. We reduce a label as soon as it comes into evaluation position.

Now we add them as another form of value

𝔱 F . . . | 𝐸

Note that these values only exist at runtime, that is, they cannot appear in expressions before evaluation has started. They are typed as consumers, which means that they are the only values with a consumer type. This makes sure that we can substitute them for covariables. Their typing can be captured by the following rule.

Now we can give the evaluation rules for label and goto:

𝐸[label 𝛼 {𝑡 }] ⊲ 𝐸[𝑡[𝐸/𝛼]] 𝐸 ′ [goto(𝔱; 𝐸)] ⊲ 𝐸[𝔱]

The rule for goto also is the reason why the theorem of strong preservation does not immediately hold (see the discussion in Section 4.3). The problem is that from this rule and the given typing rules for Fun it is not immediate that the evaluation contexts 𝐸 ′ and 𝐸 yield a term of the same type when filling their holes, so that the overall type of the term may not be preserved. But this cannot actually happen, because all other reduction rules preserve the overall type and hence all evaluation contexts that are reified by the rule for label must yield a term of that same overall type when their holes are filled. Therefore, also the rule for goto is type-preserving. This can be made precise by explicitly tracking the overall type in the type system (see, e.g., Section 6 in [Wright and Felleisen 1994]).

References

Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. 2013. Copatterns: Programming Infinite Structures by Observations. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Rome, Italy) (POPL ’13). Association for Computing Machinery, New York, NY, USA, 27–38. https://doi.org/ 10.1145/2480359.2429075

Jean-Marc Andreoli. 1992. Logic Programming with Focusing Proofs in Linear Logic. Journal of Logic and Computation 2 (1992), 297–347. Issue 3. https://doi.org/10.1093/logcom/2.3.297

Jonathan Immanuel Brachthäuser, Philipp Schuster, and Klaus Ostermann. 2020. Effects as capabilities: effect handlers and lightweight effect polymorphism. Proc. ACM Program. Lang. 4, OOPSLA, Article 126 (nov 2020), 30 pages. https: //doi.org/10.1145/3428194

William R. Cook. 2009. On Understanding Data Abstraction, Revisited. In Proceedings of the Conference on Object-Oriented Programming, Systems, Languages and Applications: Onward! Essays (Orlando). Association for Computing Machinery, New York, NY, USA, 557–572. https://doi.org/10.1145/1640089.1640133

Pierre-Louis Curien and Hugo Herbelin. 2000. The Duality of Computation. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP ’00). Association for Computing Machinery, New York, NY, USA, 233–243. https://doi.org/10.1145/357766.351262

Pierre-Louis Curien and Guillaume Munch-Maccagnoni. 2010. The Duality of Computation under Focus. In Theoretical Computer Science, Cristian S. Calude and Vladimiro Sassone (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 165–181.

Paul Downen and Zena M. Ariola. 2014. The Duality of Construction. In Proceedings of the 23rd European Symposium on Programming Languages and Systems – Volume 8410 (ESOP ’14). Springer, Berlin, Heidelberg, 249–269. https: //doi.org/10.1007/978-3-642-54833-8_14

Paul Downen and Zena M. Ariola. 2018a. Beyond Polarity: Towards a Multi-Discipline Intermediate Language with Sharing. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 119), Dan Ghica and Achim Jung (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 21:1–21:23. https://doi.org/10.4230/LIPIcs.CSL.2018.21

Paul Downen and Zena M. Ariola. 2018b. A tutorial on computational classical logic and the sequent calculus. Journal of Functional Programming 28 (2018). https://doi.org/10.1017/S0956796818000023

Paul Downen and Zena M. Ariola. 2020. Compiling With Classical Connectives. Logical Methods in Computer Science Volume 16, Issue 3 (Aug. 2020). https://doi.org/10.23638/LMCS-16(3:13)2020

Paul Downen, Philip Johnson-Freyd, and Zena M. Ariola. 2015. Structures for structural recursion. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (Vancouver, BC, Canada) (ICFP 2015). Association for Computing Machinery, New York, NY, USA, 127–139. https://doi.org/10.1145/2784731.2784762

Paul Downen, Luke Maurer, Zena M Ariola, and Simon Peyton Jones. 2016. Sequent calculus as a compiler intermediate language. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming. 74–88.

Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones. 2019. Codata in Action. In European Symposium on Programming (ESOP ’19). Springer, 119–146. https://doi.org/10.1007/978-3-030-17184-1_5

Matthias Felleisen. 1987. Reflections on Landin’s J-operator: A Partly Historical Note. Computer Languages 12, 3 (1987), 197–207. https://doi.org/10.1016/0096-0551(87)90022-1

Matthias Felleisen, Daniel P. Friedman, Eugene Kohlbecker, and Bruce Duba. 1987. A syntactic theory of sequential control. Theoretical Computer Science 52, 3 (1987), 205–237. https://doi.org/10.1016/0304-3975(87)90109-5

Andrzej Filinski. 1989. Declarative Continuations: an Investigation of Duality in Programming Language Semantics. In Category Theory and Computer Science. Springer-Verlag, Berlin, Heidelberg, 224–249.

Gerhard Gentzen. 1935a. Untersuchungen über das logische Schließen. I. Mathematische Zeitschrift 35 (1935), 176–210.

Gerhard Gentzen. 1935b. Untersuchungen über das logische Schließen. II. Mathematische Zeitschrift 39 (1935), 405–431.

Gerhard Gentzen. 1969. The collected papers of Gerhard Gentzen. North-Holland Publishing Co., Amsterdam.

Jean-Yves Girard. 1987. Linear Logic. Theoretical Computer Science 50, 1 (1987), 1–101. https://doi.org/10.1016/0304- 3975(87)90045-4

Brian Goetz et al. 2014. JSR 335: Lambda Expressions for the Java Programming Language. https://jcp.org/en/jsr/detail?id=335

Timothy G. Griffin. 1989. A Formulae-as-Type Notion of Control. In Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (San Francisco, California, USA) (POPL ’90). Association for Computing Machinery, New York, NY, USA, 47–58. https://doi.org/10.1145/96709.96714

Tatsuya Hagino. 1989. Codatatypes in ML. Journal of Symbolic Computation 8, 6 (1989), 629–650. https://doi.org/10.1016/ S0747-7171(89)80065-3

Peter John Landin. 1965. Correspondence between ALGOL 60 and Church’s Lambda-notation: part I. Commun. ACM 8, 2 (feb 1965), 89–101. https://doi.org/10.1145/363744.363749

Paul Blain Levy. 1999. Call-by-Push-Value: A Subsuming Paradigm. In Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications (TLCA ’99). Springer-Verlag, Berlin, Heidelberg, 228–242.

Luke Maurer, Paul Downen, Zena M. Ariola, and Simon Peyton Jones. 2017. Compiling without Continuations. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (Barcelona, Spain) (PLDI 2017). Association for Computing Machinery, New York, NY, USA, 482–494. https://doi.org/10.1145/3062341.3062380

Étienne Miquey. 2019. A Classical Sequent Calculus with Dependent Types. ACM Trans. Program. Lang. Syst. 41, 2, Article 8 (mar 2019), 47 pages. https://doi.org/10.1145/3230625

Guillaume Munch-Maccagnoni. 2009. Focalisation and Classical Realisability. In Computer Science Logic: 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL (Coimbra, Portugal) (CSL ’09), Erich Grädel and Reinhard Kahle (Eds.). Springer, Berlin, Heidelberg, 409–423. https://doi.org/10.1007/978-3-642-04027-6_30

Guillaume Munch-Maccagnoni. 2013. Syntax and Models of a non-Associative Composition of Programs and Proofs. Ph. D. Dissertation. Univ. Paris Diderot.

Sara Negri and Jan Von Plato. 2001. Structural Proof Theory. Cambridge University Press. https://doi.org/10.1017/ CBO9780511527340

Klaus Ostermann, David Binder, Ingo Skupin, Tim Süberkrüb, and Paul Downen. 2022. Introduction and Elimination, Left and Right. Proc. ACM Program. Lang. 6, ICFP, Article 106 (2022), 28 pages. https://doi.org/10.1145/3547637

Michel Parigot. 1992. 𝜆𝜇-Calculus: An algorithmic interpretation of classical natural deduction. In Logic Programming and Automated Reasoning, Andrei Voronkov (Ed.). Springer, Berlin, Heidelberg, 190–201.

John Charles Reynolds. 1972. Definitional Interpreters for Higher-Order Programming Languages. In ACMConf (Boston). Association for Computing Machinery, New York, NY, USA, 717–740. https://doi.org/10.1145/800194.805852

Arnaud Spiwack. 2014. A Dissection of L. (2014). Unpublished draft.

Morten Heine Sørensen and Paweł Urzyczyn. 2006. Lectures on the Curry-Howard Isomorphism. Studies in Logic and the Foundations of Mathematics, Vol. 149. Elsevier.

Hayo Thielecke. 1998. An Introduction to Landin‘s “A Generalization of Jumps and Labels”. Higher Order Symbol. Comput. 11, 2 (sep 1998), 117–123. https://doi.org/10.1023/A:1010060315625

Anne Sjerp Troelstra and Helmut Schwichtenberg. 2000. Basic Proof Theory, Second Edition. Cambridge University Press.

Philip Wadler. 1990. Linear Types Can Change the World!. In Programming Concepts and Methods. North-Holland.

Philip Wadler. 2003. Call-by-value is dual to call-by-name. In Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming (Uppsala, Sweden) (ICFP ’03). Association for Computing Machinery, New York, NY, USA, 189–201. https://doi.org/10.1145/944705.944723

Philip Wadler. 2005. Call-by-Value Is Dual to Call-by-Name – Reloaded. In Term Rewriting and Applications, 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings (Lecture Notes in Computer Science, Vol. 3467), Jürgen Giesl (Ed.). Springer, 185–203. https://doi.org/10.1007/978-3-540-32033-3_15

Andrew K. Wright and Matthias Felleisen. 1994. A Syntactic Approach to Type Soundness. Information and Computation 115, 1 (11 1994), 38–94. https://doi.org/10.1006/inco.1994.1093

Noam Zeilberger. 2008. On the Unity of Duality. Annals of Pure and Applied Logic 153, 1-3 (2008), 66–96. https://doi.org/10. 1016/j.apal.2008.01.001

Noam Zeilberger. 2009. The Logical Basis of Evaluation Order and Pattern-Matching. Ph. D. Dissertation. Carnegie Mellon University, USA. Advisor(s) Pfenning, Frank and Lee, Peter.

Yizhou Zhang, Guido Salvaneschi, Quinn Beightol, Barbara Liskov, and Andrew C. Myers. 2016. Accepting Blame for Safe Tunneled Exceptions. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (Santa Barbara, CA, USA) (PLDI ’16). Association for Computing Machinery, New York, NY, USA, 281–295. https://doi.org/10.1145/2908080.2908086