Cited By
View all- Binder DTzschentke MMüller MOstermann K(2024)Grokking the Sequent Calculus (Functional Pearl)Proceedings of the ACM on Programming Languages10.1145/36746398:ICFP(395-425)Online publication date: 15-Aug-2024
Introduction and elimination, left and right
Authors: 
Klaus Ostermann, David Binder, Ingo Skupin, Tim Süberkrüb, 
Paul DownenAuthors Info & Claims
Article No.: 106, Pages 438 - 465
Abstract
Functional programming language design has been shaped by the framework of natural deduction, in which language constructs are divided into introduction and elimination rules for producers of values. In sequent calculus-based languages, left introduction rules replace (right) elimination rules and provide a dedicated sublanguage for consumers of values. In this paper, we present and analyze a wider design space of programming languages which encompasses four kinds of rules: Introduction and elimination, both left and right. We analyze the influence of rule choice on program structure and argue that having all kinds of rules enriches a programmer’s modularity arsenal. In particular, we identify four ways of adhering to the principle that ”the structure of the program follows the structure of the data“ and show that they correspond to the four possible choices of rules. We also propose the principle of bi-expressibility to guide and validate the design of rules for a connective. Finally, we deepen the well-known dualities between different connectives by means of the proof/refutation duality.
References
[1]
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 (POPL ’13). Association for Computing Machinery, New York, NY, USA. 27–38. isbn:9781450318327 https://doi.org/10.1145/2480359.2429075
[2]
Jean-Marc Andreoli. 1992. Logic Programming with Focusing Proofs in Linear Logic. Journal of Logic and Computation, 2 (1992), 297–347. https://doi.org/10.1093/logcom/2.3.297
[3]
David Binder, Julian Jabs, Ingo Skupin, and Klaus Ostermann. 2019. Decomposition Diversity with Symmetric Data and Codata. Proc. ACM Program. Lang., 4, POPL (2019), Article 30, Dec., 28 pages. https://doi.org/10.1145/3371098
[4]
Luís Caires and Frank Pfenning. 2010. Session Types as Intuitionistic Linear Propositions. In Proceedings of the 21st International Conference on Concurrency Theory (CONCUR’10). Springer-Verlag, Berlin, Heidelberg. 222–236. isbn:3642153747 https://doi.org/10.1007/978-3-642-15375-4_16
[5]
Alberto Carraro, Thomas Ehrhard, and Antonino Salibra. 2012. The stack calculus. In Proceedings Seventh Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2012, Rio de Janeiro, Brazil, September 29-30, 2012 (EPTCS, Vol. 113). 93–108. https://doi.org/10.48550/arXiv.1303.7331
[6]
Tristan Crolard. 2004. A Formulae-as-Types Interpretation of Subtractive Logic. Journal of Logic and Computation, 14 (2004), 529–570. https://doi.org/10.1093/logcom/14.4.529
[7]
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
[8]
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-Verlag, Berlin, Heidelberg. 249–269. https://doi.org/10.1007/978-3-642-54833-8_14
[9]
Paul Downen and Zena M. Ariola. 2018. A tutorial on computational classical logic and the sequent calculus. Journal of Functional Programming, 28 (2018), https://doi.org/10.1017/S0956796818000023
[10]
Paul Downen and Zena M. Ariola. 2021. Duality in Action. In 6th International Conference on Formal Structures for Computation and Deduction, FSCD, Naoki Kobayashi (Ed.) (LIPIcs, Vol. 195). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1–32. https://doi.org/10.4230/LIPIcs.FSCD.2021.1
[11]
Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones. 2019. Codata in Action. In European Symposium on Programming (ESOP ’19). 119–146. https://doi.org/10.1007/978-3-030-17184-1_5
[12]
Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, and Shriram Krishnamurthi. 2001. How to Design Programs. An Introduction to Computing and Programming. The MIT Press, Cambridge, Massachusetts London, England.
[13]
Gerhard Gentzen. 1935. Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39 (1935), 176–210 and 405–431.
[14]
Jeremy Gibbons. 2021. How to design co-programs. Journal of Functional Programming, 31 (2021), https://doi.org/10.1017/S0956796821000113
[15]
Jean-Yves Girard. 1987. Linear logic. Theoretical Computer Science, 50, 1 (1987), 1–101. issn:0304-3975 https://doi.org/10.1016/0304-3975(87)90045-4
[16]
Philippe de Groote. 1994. On the Relation between the λ μ -Calculus and the Syntactic Theory of Sequential Control. In Proceedings of the 5th International Conference on Logic Programming and Automated Reasoning (LPAR ’94). Springer-Verlag, Berlin, Heidelberg. 31–43. https://doi.org/10.1007/3-540-58216-9_27
[17]
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
[18]
Hugo Herbelin and Silvia Ghilezan. 2008. An Approach to Call-by-Name Delimited Continuations. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’08). Association for Computing Machinery, New York, NY, USA. 383–394. https://doi.org/10.1145/1328438.1328484
[19]
Martin Hofmann and Thomas Streicher. 1997. Continuation models are universal for λ μ -calculus. In Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 – July 2, 1997. IEEE Computer Society, 387–395. https://doi.org/10.1109/LICS.1997.614964
[20]
William Lovas and Karl Crary. 2006. Structural Normalization for Classical Natural Deduction. Draft.
[21]
Guillaume Munch-Maccagnoni. 2009. Focalisation and Classical Realisability. In Computer Science Logic: 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL, Erich Grädel and Reinhard Kahle (Eds.) (CSL ’09). Springer, Berlin, Heidelberg. 409–423. https://doi.org/10.1007/978-3-642-04027-6_30
[22]
Koji Nakazawa and Tomoharu Nagai. 2014. Reduction System for Extensional Lambda-mu Calculus. In Rewriting and Typed Lambda Calculi, Gilles Dowek (Ed.). Springer International Publishing, Cham. 349–363. https://doi.org/10.1007/978-3-319-08918-8_24
[23]
Sara Negri. 2002. Varieties of Linear Calculi. J. Philos. Log., 31, 6 (2002), 569–590. https://doi.org/10.1023/A:1021264102972
[24]
Sara Negri and Jan Von Plato. 2001. Structural Proof Theory. Cambridge University Press. https://doi.org/10.1017/CBO9780511527340
[25]
Klaus Ostermann, David Binder, Ingo Skupin, Tim Süberkrüb, and Paul Downen. 2022. Introduction and Elimination, Left and Right - Coq Formalization. https://doi.org/10.5281/zenodo.6685674
[26]
Klaus Ostermann and Julian Jabs. 2018. Dualizing Generalized Algebraic Data Types by Matrix Transposition. In European Symposium on Programming. 60–85. https://doi.org/10.1007/978-3-319-89884-1_3
[27]
Michel Parigot. 1992. Free deduction: An analysis of “Computations” in classical logic. In Logic Programming, A. Voronkov (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 361–380. https://doi.org/10.1007/3-540-55460-2_27
[28]
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.
[29]
Gordon D. Plotkin. 1975. Call-By-Name, Call-By-Value and the λ -Calculus. Theoretical Computer Science, 1 (1975), 125–159. https://doi.org/10.1016/0304-3975(75)90017-1
[30]
Dag Prawitz. 1965. Natural Deduction: A Proof-Theoretical Study. Almqvist & Wiksell, Stockholm. Reprinted Mineola NY: Dover Publications (2006)
[31]
Cecylia Rauszer. 1974. A formalization of the propositional calculus of H-B logic. Studia Logica, 33 (1974), 23–34.
[32]
Tillmann Rendel, Julia Trieflinger, and Klaus Ostermann. 2015. Automatic Refunctionalization to a Language with Copattern Matching: With Applications to the Expression Problem. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015). Association for Computing Machinery, New York, NY, USA. 269–279. isbn:9781450336697 https://doi.org/10.1145/2784731.2784763
[33]
John C. Reynolds. 1972. Definitional interpreters for higher-order programming languages. In Proceedings of the ACM annual conference. Association for Computing Machinery, New York. 717–740. https://doi.org/10.1145/800194.805852
[34]
Alexis Saurin. 2005. Separation with Streams in the λ μ -calculus. In Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS ’05). IEEE Computer Society, USA. 356–365. https://doi.org/10.1109/LICS.2005.48
[35]
Peter Schroeder-Heister. 2018. Proof-Theoretic Semantics. In The Stanford Encyclopedia of Philosophy (Spring 2018 ed.), Edward N. Zalta (Ed.). Metaphysics Research Lab, Stanford University.
[36]
Olin Shivers and David Fisher. 2004. Multi-Return Function Call. In Proceedings of the Ninth ACM SIGPLAN International Conference on Functional Programming (ICFP ’04). Association for Computing Machinery, New York, NY, USA. 79–89. https://doi.org/10.1145/1016848.1016864
[37]
Arnaud Spiwack. 2014. A Dissection of L. Unpublished draft
[38]
Luca Tranchini. 2012. Natural Deduction for Dual-intuitionistic Logic. Studia Logica, 100, 3 (2012), 631–648. https://doi.org/10.1007/s11225-012-9417-8
[39]
Philip Wadler. 1990. Linear Types Can Change the World!. In Programming Concepts and Methods. North-Holland.
[40]
Philip Wadler. 2003. Call-by-value is dual to call-by-name. In Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming (ICFP ’03). ACM, New York, NY, USA. 189–201. isbn:1-58113-756-7 https://doi.org/10.1145/944705.944723
[41]
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, Jürgen Giesl (Ed.) (Lecture Notes in Computer Science, Vol. 3467). Springer, 185–203. https://doi.org/10.1007/978-3-540-32033-3_15
[42]
Philip Wadler. 2014. Propositions as sessions. J. Funct. Program., 24, 2-3 (2014), 384–418. https://doi.org/10.1145/2398856.2364568
[43]
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
[44]
Noam Zeilberger. 2009. The Logical Basis of Evaluation Order and Pattern-Matching. Ph. D. Dissertation. Carnegie Mellon University. USA. isbn:9781109163018
Index Terms
- Introduction and elimination, left and right
Recommendations
Call-by-value is dual to call-by-name
The rules of classical logic may be formulated in pairs corresponding to De Morgan duals: rules about & are dual to rules about V. A line of work, including that of Filinski (1989), Griffin (1990), Parigot (1992), Danos, Joinet, and Schellinx (1995), ...
Call-by-value is dual to call-by-name
ICFP '03: Proceedings of the eighth ACM SIGPLAN international conference on Functional programmingThe rules of classical logic may be formulated in pairs corresponding to De Morgan duals: rules about & are dual to rules about V. A line of work, including that of Filinski (1989), Griffin (1990), Parigot (1992), Danos, Joinet, and Schellinx (1995), ...
Duality in Some Intuitionistic Paraconsistent Logics
ICAART 2016: Proceedings of the 8th International Conference on Agents and Artificial IntelligenceDuality in constructive (or intuitionistic) logics is an important basic property since the dual counterpart of
a given constructive logic can obtain a refutation or falsification of the information or knowledge which is
described by the given logic. In ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
August 2022
959 pages
Copyright © 2022 Owner/Author.
This work is licensed under a Creative Commons Attribution 4.0 International License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 31 August 2022
Published in PACMPL Volume 6, Issue ICFP
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Funding Sources
- DFG
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 1,053Total Downloads
- Downloads (Last 12 months)482
- Downloads (Last 6 weeks)55
Reflects downloads up to 30 Nov 2024
Other Metrics
Citations
Cited By
View all- Binder DTzschentke MMüller MOstermann K(2024)Grokking the Sequent Calculus (Functional Pearl)Proceedings of the ACM on Programming Languages10.1145/36746398:ICFP(395-425)Online publication date: 15-Aug-2024
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in