Bialgebraic Reasoning on Higher-order Program Equivalence
Article No.: 39, Pages 1 - 15
Abstract
Logical relations constitute a key method for reasoning about contextual equivalence of programs in higher-order languages. They are usually developed on a per-case basis, with a new theory required for each variation of the language or of the desired notion of equivalence. In the present paper we introduce a general construction of (step-indexed) logical relations at the level of Higher-Order Mathematical Operational Semantics, a highly parametric categorical framework for modeling the operational semantics of higherorder languages. Our main result states that for languages whose weak operational model forms a lax bialgebra, the logical relation is automatically sound for contextual equivalence. Our abstract theory is shown to instantiate to combinatory logics and λ-calculi with recursive types, and to different flavours of contextual equivalence.
References
[1]
Carmine Abate, Matteo Busi, and Stelios Tsampas. 2021. Fully Abstract and Robust Compilation: And How to Reconcile the Two, Abstractly. In 19th Asian Symposium on Programming Languages and Systems, APLAS'21 (LNCS, Vol. 13008), Hakjoo Oh (Ed.). Springer, 83--101.
[2]
S. Abramsky. 1990. The lazy λ-calculus. In Research topics in Functional Programming. Addison Wesley, 65--117.
[3]
Jiří Adámek, Horst Herrlich, and George E. Strecker. 1990. Abstract and Concrete Categories. John Wiley and Sons. Free online version: http://www.tac.mta.ca/tac/reprints/articles/17/tr17abs.html.
[4]
Jiří Adámek, Stefan Milius, and Lawrence S. Moss. 2021. Initial Algebras Without Iteration. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 211), Fabio Gadducci and Alexandra Silva (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 5:1--5:20.
[5]
Alejandro Aguirre and Lars Birkedal. 2023. Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice. Proc. ACM Program. Lang. 7, POPL (2023), 33--60.
[6]
Amal Ahmed. 2006. Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types. In 15th European Symposium on Programming (ESOP 2006) (LNCS, Vol. 3924). Springer, 69--83.
[7]
Amal Ahmed, Derek Dreyer, and Andreas Rossberg. 2009. State-dependent representation independence. In 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (POPL 2009), Zhong Shao and Benjamin C. Pierce (Eds.). ACM, 340--353.
[8]
Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler. 2017. Theorems for free for free: parametricity, with and without types. Proc. ACM Program. Lang. 1, ICFP (2017), 39:1--39:28.
[9]
Thorsten Altenkirch and Ambrus Kaposi. 2016. Normalisation by Evaluation for Dependent Types. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) (LIPIcs, Vol. 52). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 6:1--6:16.
[10]
Abhishek Anand and Greg Morrisett. 2017. Revisiting Parametricity: Inductives and Uniformity of Propositions. CoRR abs/1705.01163 (2017). arXiv:1705.01163 http://arxiv.org/abs/1705.01163
[11]
Andrew W. Appel and David A. McAllester. 2001. An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst. 23, 5 (2001), 657--683.
[12]
Nick Benton and Chung-Kil Hur. 2009. Biorthogonality, Step-Indexing and Compiler Correctness. In 14th ACM SIGPLAN International Conference on Functional Programming (ICFP 2009) (Edinburgh, Scotland). ACM, 97--108.
[13]
Jean-Philippe Bernardy, Patrik Jansson, and Ross Paterson. 2012. Proofs for free - Parametricity for dependent types. J. Funct. Program. 22, 2 (2012), 107--152.
[14]
Lars Birkedal, Kristian Støvring, and Jacob Thamsborg. 2010. The Category-Theoretic Solution of Recursive Metric-Space Equations. Theoretical Computer Science 411, 47 (2010), 4102--4122.
[15]
Ales Bizjak and Lars Birkedal. 2015. Step-Indexed Logical Relations for Probability. In 18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2015), Vol. 9034. Springer, 279--294.
[16]
Aleš Bizjak and Lars Birkedal. 2015. Step-Indexed Logical Relations for Probability. In 18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2015) (LNCS, Vol. 9034), Andrew Pitts (Ed.). Springer, 279--294.
[17]
Bard Bloom. 1995. Structural Operational Semantics for Weak Bisimulations. Theor. Comput. Sci. 146, 1&2 (1995), 25--68.
[18]
Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot. 2015. Lax Bialgebras and Up-To Techniques for Weak Bisimulations. In 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015 (LIPIcs, Vol. 42), Luca Aceto and David de Frutos-Escrig (Eds.). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 240--253.
[19]
Francis Borceux. 1994. Handbook of Categorical Algebra: Volume 1: Basic Category Theory. Encyclopedia of Mathematics and Its Applications, Vol. 1. Cambridge University Press.
[20]
Aurelio Carboni, Stephen Lack, and R. F. C. Walters. 1993. Introduction to Extensive and Distributive Categories. Journal of Pure and Applied Algebra 84, 2 (Feb. 1993), 145--158.
[21]
Francesco Dagnino and Francesco Gavazzo. 2022. A Fibrational Tale of Operational Logical Relations. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022) (LIPIcs, Vol. 228). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 3:1--3:21.
[22]
Francesco Dagnino and Francesco Gavazzo. 2023. A Fibrational Tale of Operational Logical Relations: Pure, Effectful and Differential. CoRR (2023). arXiv:2303.03271 [cs]
[23]
Ugo Dal Lago and Francesco Gavazzo. 2021. Differential Logical Relations, Part II Increments and Derivatives. Theor. Comput. Sci. 895, C (2021), 34--47.
[24]
Dominique Devriese, Marco Patrignani, and Frank Piessens. 2016. Fully-abstract compilation by approximate back-translation. In 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016. 164--177.
[25]
Derek Dreyer, Amal Ahmed, and Lars Birkedal. 2009. Logical Step-Indexed Logical Relations. In 24th Annual IEEE Symposium on Logic In Computer Science (LICS 2009). IEEE Computer Society, 71--80.
[26]
Derek Dreyer, Amal Ahmed, and Lars Birkedal. 2011. Logical Step-Indexed Logical Relations. Log. Methods Comput. Sci. 7, 2 (2011).
[27]
Derek Dreyer, Georg Neis, and Lars Birkedal. 2012. The impact of higher-order state and control effects on local relational reasoning. J. Funct. Program. 22, 4-5 (2012), 477--528.
[28]
Marcelo Fiore. 2022. Semantic analysis of normalisation by evaluation for typed lambda calculus. Math. Struct. Comput. Sci. 32, 8 (2022), 1028--1065.
[29]
Marcelo P. Fiore and Gordon D. Plotkin. 1994. An Axiomatization of Computationally Adequate Domain Theoretic Models of FPC. In 9th Annual Symposium on Logic in Computer Science (LICS '94). IEEE Computer Society, 92--102.
[30]
Marcelo P. Fiore, Gordon D. Plotkin, and Daniele Turi. 1999. Abstract Syntax and Variable Binding. In 14th Annual IEEE Symposium on Logic in Computer Science (LICS 1999). IEEE Computer Society, 193--202.
[31]
Marcelo P. Fiore and Sam Staton. 2010. Positive structural operational semantics and monotone distributive law. In CMCS'10 Short Contributions : 10th International Workshop on Coalgebraic Methods in Computer Science.
[32]
Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, and Lars Birkedal. 2023. Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code. J. ACM (2023).
[33]
Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, and Robbert Krebbers. 2020. Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris. In 25th ACM SIGPLAN International Conference on Functional Programming (ICFP 2020) (Proc. ACM Program. Lang., Vol. 4). ACM, Article 114, 29 pages.
[34]
Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat. 2023. Towards a Higher-Order Mathematical Operational Semantics. In 50th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2023) (Proc. ACM Program. Lang., Vol. 7). ACM, Article 22, 27 pages.
[35]
Sergey Goncharov, Stefan Milius, Stelios Tsampas, and Henning Urbat. 2024. Bialgebraic Reasoning on Higher-Order Program Equivalence. arXiv:2402.00625 [cs.PL]
[36]
Sergey Goncharov, Alessio Santamaria, Lutz Schröder, Stelios Tsampas, and Henning Urbat. 2024. Logical Predicates in Higher-Order Mathematical Operational Semantics. (2024).
[37]
Andrew D. Gordon. 1999. Bisimilarity as a Theory of Functional Programming. Theor. Comput. Sci. 228, 1-2 (1999), 5--47.
[38]
A. D. Gordon. 1999. Operational Equivalences for Untyped and Polymorphic Object Calculi. Cambridge University Press, USA, 9--54.
[39]
Jean Goubault-Larrecq, Slawomir Lasota, and David Nowak. 2008. Logical relations for monadic types. Math. Struct. Comput. Sci. 18, 6 (2008), 1169--1217.
[40]
C.A. Gunter. 1992. Semantics of Programming Languages: Structures and Techniques. London.
[41]
Claudio Hermida and Bart Jacobs. 1998. Structural Induction and Coinduction in a Fibrational Setting. Information and Computation 145, 2 (1998), 107--152.
[42]
Claudio Hermida, Uday S. Reddy, and Edmund P. Robinson. 2014. Logical Relations and Parametricity - A Reynolds Programme for Category Theory and Programming Languages. Electron. Notes Theor. Comput. Sci. 303 (2014), 149--180.
[43]
Claudio Alberto Hermida. 1993. Fibrations, logical predicates and indeterminates. Ph. D. Dissertation. University of Edinburgh. https://era.ed.ac.uk/handle/1842/14057
[44]
J. Roger Hindley and Jonathan P. Seldin. 2008. Lambda-Calculus and Combinators: An Introduction (2 ed.). Cambridge University Press.
[45]
Douglas J. Howe. 1989. Equality In Lazy Computation Systems. In 4th Annual Symposium on Logic in Computer Science (LICS 1989). IEEE Computer Society, 198--203.
[46]
Douglas J. Howe. 1996. Proving Congruence of Bisimulation in Functional Programming Languages. Inf. Comput. 124, 2 (1996), 103--112.
[47]
Chung-Kil Hur and Derek Dreyer. 2011. A Kripke logical relation between ML and Assembly. In 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (POPL 2011), Thomas Ball and Mooly Sagiv (Eds.). ACM, 133--146.
[48]
Chung-Kil Hur, Derek Dreyer, Georg Neis, and Viktor Vafeiadis. 2012. The marriage of bisimulations and Kripke logical relations. In 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) 2012) USA, January 22-28, 2012, John Field and Michael Hicks (Eds.). ACM, 59--72.
[49]
Bart Jacobs. 2016. Introduction to Coalgebra: Towards Mathematics of States and Observation. Cambridge Tracts in Theoretical Computer Science, Vol. 59. Cambridge University Press.
[50]
Patricia Johann, Alex Simpson, and Janis Voigtländer. 2010. A Generic Operational Metatheory for Algebraic Effects. In 25th Annual IEEE Symposium on Logic in Computer Science (LICS 2010). IEEE Computer Society, 209--218.
[51]
Shin-ya Katsumata. 2005. A generalisation of pre-logical predicates and its applications. Ph. D. Dissertation. University of Edinburgh. http://hdl.handle.net/1842/850
[52]
Chantal Keller and Marc Lasson. 2012. Parametricity in an Impredicative Sort. In Computer Science Logic - 26th International Workshop/21st Annual Conference of the EACSL, (CSL 2012) (LIPIcs, Vol. 16), Patrick Cégielski and Arnaud Durand (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 381--395.
[53]
Ugo Dal Lago and Francesco Gavazzo. 2022. Effectful program distancing. In 49th Annual ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2022) (Proc. ACM Program. Lang., Vol. 6). 1--30.
[54]
Ugo Dal Lago, Francesco Gavazzo, and Akira Yoshimizu. 2019. Differential Logical Relations, Part I: The Simply-Typed Case. In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019) (LIPIcs, Vol. 132). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 111:1--111:14.
[55]
Søren B. Lassen. 1998. Relational Reasoning about Functions and Nondeterminism. Ph. D. Dissertation. Aarhus University. https://www.brics.dk/DS/98/2/BRICS-DS-98-2.pdf
[56]
Paul Levy, John Power, and Hayo Thielecke. 2003. Modelling environments in call-by-value programming languages. Inf. Comput. 185, 2 (2003), 182--210.
[57]
S. Mac Lane. 1978. Categories for the Working Mathematician (2 ed.). Graduate Texts in Mathematics, Vol. 5. Springer. http://link.springer.com/10.1007/978-1-4757-4721-8
[58]
Robin Milner. 1978. A theory of type polymorphism in programming. J. Comput. System Sci. 17, 3 (1978), 348--375.
[59]
James H. Morris. 1968. Lambda-Calculus Models of Programming Languages. Ph.D. Dissertation. Massachusetts Institute of Technology.
[60]
Max S. New, William J. Bowman, and Amal Ahmed. 2016. Fully abstract compilation via universal embedding. In 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016). ACM, 103--116.
[61]
Peter W. O'Hearn and Jon G. Riecke. 1995. Kripke Logical Relations and PCF. Inf. Comput. 120, 1 (1995), 107--116.
[62]
C-H Luke Ong. 1988. The Lazy Lambda Calculus: An Investigation into the Foundations of Functional Programming. Ph. D. Dissertation. Imperial College London. http://hdl.handle.net/10044/1/47211
[63]
Marco Patrignani, Eric Mark Martin, and Dominique Devriese. 2021. On the Semantic Expressiveness of Recursive Types. In 48th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2021) (Proc. ACM Program. Lang., Vol. 5). ACM, Article 21, 29 pages.
[64]
James T. Perconti and Amal Ahmed. 2014. Verifying an Open Compiler Using Multi-language Semantics. In Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014 (Lecture Notes in Computer Science, Vol. 8410). Springer, 128--148.
[65]
Andrew M. Pitts. 1996. Reasoning about Local Variables with Operationally-Based Logical Relations. In 11th Annual IEEE Symposium on Logic in Computer Science (LICS 1996). IEEE Computer Society, 152--163.
[66]
Andrew M. Pitts. 1996. Relational Properties of Domains. Information and Computation 127, 2 (1996), 66--90.
[67]
Andrew M Pitts. 1997. Operationally-based theories of program equivalence. Semantics and Logics of Computation 14 (1997), 241.
[68]
Andrew M. Pitts. 1998. Existential Types: Logical Relations and Operational Equivalence (Lecture Notes in Computer Science, Vol. 1443). Springer, 309--326.
[69]
Andrew M. Pitts. 2000. Parametric Polymorphism and Operational Equivalence. Mathematical Structures in Computer Science 10, 3 (2000), 321--359.
[70]
Andrew M. Pitts. 2004. Typed operational reasoning. In Advanced Topics in Types and Programming Languages, Benjamin C. Pierce (Ed.). The MIT Press, Chapter 7.
[71]
Andrew M. Pitts and Ian D. B. Stark. 1993. Observable Properties of Higher Order Functions That Dynamically Create Local Names, or: What's New?. In 8th International Symposium on Mathematical Foundations of Computer Science (MFCS 1993) (LNCS, Vol. 711). Springer, 122--141.
[72]
Andrew M. Pitts and Ian D. B. Stark. 1998. Operational Reasoning for Functions with Local State. In Higher Order Operational Techniques in Semantics, Andrew D. Gordon and Andrew M. Pitts (Eds.). Cambridge University Press, New York, NY, USA, 227--274.
[73]
G. D. Plotkin. 1973. Lambda-Definability and Logical Relations. Technical Report. University of Edinburgh.
[74]
John C. Reynolds. 1983. Types, Abstraction and Parametric Polymorphism. In Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, R. E. A. Mason (Ed.). North-Holland/IFIP, 513--523.
[75]
Jan J. M. M. Rutten. 2000. Universal coalgebra: a theory of systems. Theor. Comput. Sci. 249, 1 (2000), 3--80.
[76]
K. Sieber. 1992. Reasoning about sequential functions via logical relations. In Applications of Categories in Computer Science: Proceedings of the London Mathematical Society Symposium, Durham 1991 (London Mathematical Society Lecture Note Series), M. P. Fourman, P. T. Johnstone, and A. M.Editors Pitts (Eds.). Cambridge University Press, 258--269.
[77]
Simon Spies, Neel Krishnaswami, and Derek Dreyer. 2021. Transfinite step-indexing for termination. 5, POPL, Article 13 (jan 2021), 29 pages.
[78]
R. Statman. 1985. Logical relations and the typed lambda-calculus. Information and Control 65, 2 (1985), 85--97.
[79]
William W. Tait. 1967. Intensional Interpretations of Functionals of Finite Type I. J. Symb. Log. 32, 2 (1967), 198--212.
[80]
Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, and Lars Birkedal. 2017. A Logical Relation for Monadic Encapsulation of State: Proving Contextual Equivalences in the Presence of RunST. In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017) (Proc. ACM Program. Lang., Vol. 2). ACM, Article 64, 28 pages.
[81]
Stelios Tsampas, Andreas Nuyts, Dominique Devriese, and Frank Piessens. 2020. A Categorical Approach to Secure Compilation. In 15th IFIP WG 1.3 International Workshop on Coalgebraic Methods in Computer Science, CMCS'20 (LNCS, Vol. 12094), Daniela Petrisan and Jurriaan Rot (Eds.). Springer, 155--179.
[82]
Daniele Turi and Gordon D. Plotkin. 1997. Towards a Mathematical Operational Semantics. In 12th Annual IEEE Symposium on Logic in Computer Science (LICS 1997). 280--291.
[83]
Henning Urbat, Stelios Tsampas, Sergey Goncharov, Stefan Milius, and Lutz Schröder. 2023. Weak Similarity in Higher-Order Mathematical Operational Semantics. In 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2023). IEEE Computer Society Press.
[84]
Henning Urbat, Stelios Tsampas, Sergey Goncharov, Stefan Milius, and Lutz Schröder. 2023. Weak Similarity in Higher-Order Mathematical Operational Semantics. arXiv:2302.08200 [cs.PL]
[85]
Rob J. van Glabbeek. 2011. On cool congruence formats for weak bisimulations. Theor. Comput. Sci. 412, 28 (2011).
[86]
Mitchell Wand, Ryan Culpepper, Theophilos Giannakopoulos, and Andrew Cobb. 2018. Contextual Equivalence for a Probabilistic Language with Continuous Random Variables and Recursion. In 23rd ACM SIGPLAN International Conference on Functional Programming (ICFP 2018) (Proc. ACM Program. Lang., Vol. 2). ACM, Article 87, 30 pages.
[87]
Hiroshi Watanabe. 2002. Well-behaved Translations between Structural Operational Semantics. Electr. Notes Theor. Comput. Sci. 65, 1 (2002), 337--357.
Recommendations
Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances
LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer ScienceThis paper studies quantitative refinements of Abramsky's applicative similarity and bisimilarity in the context of a generalisation of Fuzz, a call-by-value λ-calculus with a linear type system that can express program sensitivity, enriched with ...
Reasoning about higher-order relational specifications
PPDP '13: Proceedings of the 15th Symposium on Principles and Practice of Declarative ProgrammingThe logic of hereditary Harrop formulas (HH) has proven useful for specifying a wide range of formal systems that are commonly presented via syntax-directed rules that make use of contexts and side-conditions. The two-level logic approach, as ...
Comments
Information & Contributors
Information
Published In
July 2024
988 pages
ISBN:9798400706608
DOI:10.1145/3661814
- Conference Chair:
- Pawel Sobocinski,
- Program Chairs:
- Ugo Dal Lago,
- Javier Esparza
Copyright © 2024 Copyright is held by the owner/author(s). Publication rights licensed to ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Sponsors
- SIGLOG: ACM Special Interest Group on Logic and Computation
- IEEE Computer Society
In-Cooperation
- EACSL
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 08 July 2024
Check for updates
Qualifiers
- Research-article
Funding Sources
Conference
LICS '24
Sponsor:
LICS '24: 39th Annual ACM/IEEE Symposium on Logic in Computer Science
July 8 - 11, 2024
Tallinn, Estonia
Acceptance Rates
LICS '24 Paper Acceptance Rate 72 of 236 submissions, 31%;
Overall Acceptance Rate 215 of 622 submissions, 35%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 20Total Downloads
- Downloads (Last 12 months)20
- Downloads (Last 6 weeks)6
Reflects downloads up to 14 Sep 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in